Automated Abstraction Refinement for Information Flow Security in Embedded Systems
En palabras de los autores
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.
Apareció: viernes, 25 de septiembre. arXiv. Preprint, todavía sin revisión por pares.
Comentario de los autores: 18 pages, 3 figures, 1 table. Accepted at the 24th International Conference on Software Engineering and Formal Methods (SEFM 2026), to be published in Springer's Lecture Notes in Computer Science series. This is the submitted version and ha