Automated Abstraction Refinement for Information Flow Security in Embedded Systems
Paper proposes heuristic automatic abstraction refinement for information flow analysis in concurrent embedded systems, implemented for SystemC.
The arXiv paper addresses imprecision and cost in information flow analysis (IFA) for concurrent, time-dependent embedded systems by automating abstraction refinement. Heuristics select abstraction levels based on state dependencies and detected potential leakage, replacing prior manual definitions. The approach combines symbolic execution with abstract interpretation to capture data, control, timing, and event dependencies between processes. It is implemented for SystemC and demonstrated on several shared bus architectures, balancing analysis time against precision.
- Automatic abstraction refinement replaces manual level selection in information flow analysis
- Heuristics use state dependencies and detected leakage to pick abstraction levels
- Symbolic execution captures data, control, timing, and event dependencies
- Implemented for SystemC and evaluated on shared bus architectures
Full article185 words · extracted from arxiv.org · click to collapse
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.
Text extracted automatically; images, tables and formatting may be missing. Original: https://arxiv.org/abs/2609.29645