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).

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Symbolic Execution for Precise Information Flow Analysis of Timed Concurrent Systems

  • Jonas Becker-Kupczok,
  • Paula Herber

摘要

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).