Automatic method improves security checks for embedded systems
Automated Abstraction Refinement for Information Flow Security in Embedded Systems
Cryptography and SecurityProgramming LanguagesSoftware Engineering
Summary
Embedded systems are tiny computers in devices that need to keep information safe and private. Checking if these systems leak secret information can be very slow or unclear because they run many tasks at once and depend on precise timing. The authors developed a new way to automatically adjust how these checks work using smart guesses about where problems might happen. This makes the checks faster and still good enough to find if secrets could leak. They tested their method on shared bus computer designs and showed it works.
What this means in practice
- •For embedded system designers: Speed up security verification in embedded designs by automatically tuning analysis precision to detect confidential data leaks effectively.
- •For hardware architects: Assess potential information flow vulnerabilities in shared bus architectures with reduced manual effort through automated refinement heuristics.
Authors
Jonas Becker-Kupczok, Lukas Ernst, Paula Herber
Abstract
Information flow analysis (IFA) is a powerful technique for verifying confidentiality and integrity and is therefore highly desirable for security-sensitive embedded systems. However, as these systems are inherently concurrent and time-dependent, existing IFA for embedded systems tend to be either imprecise or expensive. In this paper, we propose an approach to tackle this problem using automatic abstraction refinement. The key idea is to heuristically choose abstraction levels based on information about dependencies between states and detected potential information leakage. Our approach builds on previous work, where we leverage symbolic execution to precisely capture data, control, timing, and event dependencies between processes within an IFA. To capture values symbolically, this analysis uses abstract interpretation. While the existing approach requires manual definition of abstraction levels, our novel contribution in this paper is using carefully designed heuristics to select these levels automatically. The aim is to keep analysis times acceptable while also retaining enough information to decide whether or not illegal information flow is possible. We have implemented our approach for the system design language SystemC and demonstrate its feasibility with experimental results on several shared bus architectures.