发表机构
University of Münster（明斯特大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对嵌入式系统信息流分析不精确或代价高昂的问题，本文提出基于状态依赖和潜在泄露信息的启发式自动抽象精化方法，在SystemC上实现并验证可行性。
AI 中文摘要
信息流分析（IFA）是验证机密性和完整性的强大技术，因此对于安全敏感的嵌入式系统而言非常可取。然而，由于这些系统本质上是并发且时间相关的，现有的针对嵌入式系统的IFA往往要么不精确，要么代价高昂。在本文中，我们提出了一种利用自动化抽象精化来解决该问题的方法。关键思想是基于状态之间依赖关系以及检测到的潜在信息泄露的信息，启发式地选择抽象级别。我们的方法建立在先前工作的基础上，在该工作中，我们利用符号执行来精确捕获IFA中进程之间的数据、控制、时间和事件依赖关系。为了符号化地捕获值，该分析使用抽象解释。虽然现有方法需要手动定义抽象级别，但我们在本文中的新颖贡献是使用精心设计的启发式规则来自动选择这些级别。目标是保持分析时间可接受，同时保留足够的信息以判断非法信息流是否可能发生。我们已经为系统设计语言SystemC实现了我们的方法，并通过在几种共享总线架构上的实验结果证明了其可行性。
英文摘要
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.
Comments18 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 has not undergone peer review or any post-submission improvements or corrections
