Symbolic Execution for Precise Information Flow Analysis of Timed Concurrent Systems

Becker-Kupczok, Jonas; Herber, Paula

Abstract

Information flow analysis (IFA) is a powerful technique for verifying confidentiality and integrity. This is highly desirable for embedded systems, where security violations can lead to significant economic damages or even loss of human life. Unfortunately, if shared bus architectures are used, classical IFA that do not consider timing behavior will always classify the whole system as insecure. In this paper, we present an approach to regain precision in IFA for timed systems that concurrently execute processes using a cooperative scheduler. Our key idea is to extend a classical IFA approach based on program dependence graphs with a symbolic execution together with abstract interpretation to precisely yet abstractly capture data, control, timing, and event dependencies between processes. While this increases the cost of the analysis, the gain in precision leverages IFA even for concurrent systems with time-shared bus architectures as they are widely used, for example, in the automotive industry. We have implemented our approach for the system level description language SystemC, and demonstrate its applicability with a case study that uses a general-purpose input/ouput (GPIO).