Organizer: Tim Weißmantel, Modeling and Analysis of Information Systems

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 talk, I present an approach to regain precision in IFA for timed systems that concurrently execute processes using a cooperative scheduler, such as SystemC. 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 timeshared bus architectures.

Speaker Bio

https://www.uni-muenster.de/EmbSys/team/becker/index.shtml