組み込みシステムの情報流解析を自動で精密化
Automated Abstraction Refinement for Information Flow Security in Embedded Systems
この論文をやさしく読む
ひとことで言うと
組み込みシステムで情報漏えいを調べる際、解析の細かさを自動調整する方法。
何に役立つ？
時間や並行処理を含む設計で、機密情報の不正な流れを現実的な計算時間で検証する助けになる。
この研究の面白いところ
従来は手動だった抽象化水準の選択を、状態間の依存関係と漏えい候補に基づいて自動化した。
どこまで分かった？
実行可能性はSystemCのいくつかの共有バス構成で示された。大規模な製品全般での性能は要旨に示されていない。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
情報流解析は機密性と完全性を検証する強力な方法であり、安全性が重要な組み込みシステムで有用である。しかし、これらのシステムは本質的に並行して動作し、時間にも依存するため、既存の情報流解析は精度が低いか計算費用が高い傾向がある。本論文は、自動的な抽象化の精密化でこの問題に取り組む。状態間の依存関係と、検出された潜在的な情報漏えいに関する情報に基づき、ヒューリスティックに抽象化の水準を選ぶことが中心となる。先行研究では、記号実行を使って、プロセス間のデータ、制御、時間、事象の依存関係を情報流解析の中で精密に捉えた。値を記号的に扱うために抽象解釈を用いる。従来の方法では抽象化水準を手動で定める必要があったが、本論文では慎重に設計したヒューリスティックによって自動的に選べるようにする。目的は、解析時間を許容範囲に保ちながら、違法な情報流が起こりうるか判断するだけの情報を残すことである。SystemC設計言語向けに実装し、いくつかの共有バス構成を使った実験結果で実行可能性を示す。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-24（UTC）
- 最新改訂
- 2026-09-24 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-24 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
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.
著者のコメント
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 has not undergone peer review or any post-submission improvements or corrections
arXiv ID: 2609.29645 ／ 要約の誤りについて