PaperlayerView exact revision on arXiv

Source-linked AI summary

Automated Abstraction Refinement for Information Flow Security in Embedded Systems

Jonas Becker-Kupczok, Lukas Ernst, Paula Herber

arXiv:2609.29645v1cs.CRcs.PLcs.SE

TL;DR

Timed and concurrent embedded systems make information flow analysis either imprecise or expensive. This paper uses heuristic-guided abstraction refinement during symbolic-execution-based analysis; experiments on shared bus architectures show automatically derived abstractions can support precise, efficient analysis while reducing manual effort.

  • Problem

    Information flow analysis for time-dependent, concurrent embedded systems can be imprecise or expensive, making it difficult to assess confidentiality and integrity.

    Source: §1 · pp. 1–2

  • Method

    The approach heuristically refines abstraction levels during symbolic-execution-based IFA, reducing explored states and targeting detected potential information leakage.

    Source: §1 · p. 2, §3 · p. 5, §3.3 · p. 9

  • Results

    Experiments on shared bus architectures show automatically derived abstractions enable efficient and precise IFA while reducing manual effort and maintaining scalability.

    Source: §1 · p. 3, §6 · p. 16

  • Takeaways & Limitations

    The case studies demonstrate feasibility of automated abstraction selection for symbolic-execution-based IFA of timed concurrent SystemC models.

    Source: §1 · p. 3, §6 · p. 16

    The authors believe the non-cumulative refinement approach is sound but do not provide formal assurances of that claim.

    Source: Identifying Paths in Different SysCDGs · p. 14

Abstract

from arXiv · show

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.

1 Introduction

Timed and concurrent embedded systems make information flow analysis difficult: timing-blind analyses lose precision, while analyses tracking timing and control dependencies can become expensive. The paper introduces heuristic-driven abstraction refinement and reports case studies in which automatically chosen abstractions support precise, efficient analysis without manual abstraction definitions.

1 Introduction

  • Timing-blind IFA can classify an entire shared-bus system as insecure, while precise timing and control analysis may require unscalable interleaving exploration.These challenges arise in concurrent, time-dependent embedded systems.Source: §1 · pp. 1–2
  • The prior symbolic-execution approach combines abstract interpretation with dependency tracking, but choosing abstractions remains a manual, expertise-intensive task.Retaining variables can constrain branching yet enlarge the state space; retaining less information can increase overapproximation and false positives.Source: §1 · p. 2
  • Heuristics dynamically adapt abstraction levels, refining symbolic state-space exploration and filtering spurious information flows when potential violations are detected.Exploration uses partial descendants and splitters; information-flow refinement uses path resolution.Source: §1 · p. 2
  • Case studies show automatically chosen abstractions enable precise and efficient IFA without manually defined abstractions.The implementation targets SystemC and the evaluation includes shared bus architectures.Source: §1 · pp. 2–3

2 Background

The background introduces information flow analysis, SystemC’s concurrent event-driven simulation model, and the symbolic-execution approach on which this work builds.

2.1 Information Flow Analysis

  • IFA identifies program locations that can influence a target location, supporting non-interference analysis for confidentiality or integrity.Source: §2.1 · p. 3
  • A program dependence graph represents possible influences between program locations and supports backward slicing from an output.Its edges typically encode data and control dependencies.Source: §2.1 · p. 3

2.2 SystemC

  • SystemC models communicating hardware/software processes with an event-driven simulation kernel and supports shared-bus communication, arbitration, contention, and timing.Source: §2.2 · p. 3
  • SystemC’s scheduler executes ready processes in evaluation phases, publishes signal updates in update/notify phases, and advances time when no process is ready.Delta delays separate update/notify phases; threads yield cooperatively at waits.Source: §2.2 · pp. 3–4

2.3 Symbolic Execution for IFA of Embedded Systems

  • The prior approach combines block-wise dependence graphs with symbolic execution and abstract interpretation to construct a SystemC dependence graph for reachability-based IFA.The graph captures data, timing, event, and other control dependencies between blocks.Source: §2.3 · p. 4, Figure 1 · p. 4

3 Heuristic Abstraction Refinement

The section describes heuristic abstraction refinement that uses state dependencies and potential leaks to balance symbolic-execution scalability and information-flow precision. It also explains how path sequences across SysCDGs assess whether potential flows persist across abstractions, with soundness implications differing between cumulative and non-cumulative procedures.

3 Heuristic Abstraction Refinement

  • The overall process alternates symbolic execution and refinement, restarting after indicated changes and stopping when no violating paths remain or no promising refinements can be identified.Exploration refinement reduces the state space used to construct the thread interleaving and SystemC dependence graphs; information-flow refinement tests whether a detected violating path persists under a refined abstraction.Source: §3 · pp. 5–6

3.1 Kinds of Abstractions

  • Abstractions can track selected variable assignments rather than variables globally, so values may be tracked only until their relevant branching decision.This assignment-based view conceptually corresponds to static single assignment form, without explicitly transforming the program.Source: §3.1 · pp. 6–7

3.2 Exploration Refinement using Partial Descendants and Splitters

  • Exploration refinement starts with the highest abstraction and tracks branch-controlling values when partial descendants exceed a threshold or an untracked condition changes the scheduler state.The partial-descendants heuristic monitors the maximum count across abstract states and uses breadth-first exploration to mitigate overestimation; the cheaper, local splitters heuristic checks scheduler-state changes at atomic-block ends.Source: §3.2 · p. 7, Partial Descendants Heuristic · p. 8, Splitters Heuristic · p. 8

3.3 Information Flow Refinement

  • Information-flow refinement iteratively tests violating paths and refines their controlling conditions or dependencies until paths disappear or no promising candidates remain.The path-resolution heuristic first considers data dependencies of controlling nodes, then their other dependencies, and finally dependencies of any path node. Cumulative refinement combines refinements across paths; non-cumulative refinement can keep abstractions smaller, while execution timeouts reject costly candidates.Source: §3.3 · pp. 8–9, Path Resolution Heuristic · p. 10
  • Program locations serve as node signatures, so paths passing the same locations in the same order can be matched across SysCDGs despite different abstract state transitions.The authors argue that if a path is absent because a location is not executed under another abstraction, there likely is no corresponding concrete information flow.Source: Identifying Paths in Different SysCDGs · pp. 12–13
  • Common violating paths are found in a signature product graph whose product nodes combine only nodes with matching signatures across SysCDGs.A common path in the considered SysCDGs is defined as a path in this product graph.Source: Identifying Paths in Different SysCDGs · p. 13
  • Common-path checking can retain a potential flow through a loop after refinement even when the old path itself is absent from the refined graph.For a loop refined from an unknown iteration count to exactly four iterations, the old one-iteration path is absent, but the four-iteration path remains in the old SysCDG and is common to both graphs.Source: Identifying Paths in Different SysCDGs · p. 13
  • For cumulative refinement, signature choice affects precision and performance rather than soundness, but mistaken path matching can retain useless or discard useful refinements and cause false positives.Timeouts caused by useless refinements can also lead to a false positive result of illegal information flow.Source: Identifying Paths in Different SysCDGs · p. 13
  • For non-cumulative refinement, missing a common violating path could incorrectly report secure information flow; the authors believe their approach is sound but provide no formal assurance.Overapproximating common paths is acceptable for soundness, though it may harm performance or cause false positives.Source: Identifying Paths in Different SysCDGs · p. 14

4 Evaluation

Case studies on shared bus architectures evaluate the prototype and its refinement strategies. The examples report reduced state space and analysis time alongside removal of spurious information flow.

4 Evaluation

  • The prototype was implemented in Java for SystemC and evaluated on shared bus case studies.The results are reported in Table 1.Source: §4 · p. 14
  • Both cumulative and non-cumulative information flow refinement eliminate false positives in Priorities and Many Slots, with equal efficiency.Priorities needs no exploration refinement; Many Slots models a multi-slot bus with security levels stored alongside values.Source: §4 · p. 14
  • In Arbiter, exploration refinement is unnecessary, and the splitters heuristic's additional states are also introduced by information flow refinement because they are needed to prove security.The case study models dynamic bus allocation.Source: §4 · p. 14
  • ≈100× lower exploration time resulted from both exploration heuristics in Transmitters, where constructing the SysCDG without exploration refinement exhausted memory.The case has two transmitters with different security levels and dynamic timing behavior.Source: §4 · p. 15
  • Across the examples, the heuristics reduce state space and analysis time and exclude spurious information flow; non-cumulative refinement can also yield fewer states.Partial descendants and splitters give similar results, while cumulative and non-cumulative refinement are similarly efficient.Source: §4 · p. 15

5 Related Work

Related work addresses abstraction refinement, information flow analysis, and concurrent systems through varied techniques and formalisms. The authors position their contribution as applying abstraction refinement to IFA for embedded systems.

5 Related Work

  • Path-condition approaches can exclude spurious paths, but loops, recursion, and concurrency can make them expensive or imprecise; embedded-system applicability is also limited.Timed path conditions are used for embedded-system security hardening and Simulink IFA, but does not derive them and does not target control-flow-oriented languages such as SystemC.Source: §5 · p. 15
  • Automatic path-condition refinement [37] targets Java bytecode rather than embedded-system characteristics, and concrete witness validation means non-termination can prevent a conclusive result.Uppaal timed-automata information-flow control is tailored to that formalism.Source: §5 · pp. 15–16
  • Concurrent IFA approaches often use rely/guarantee reasoning or separation logics, requiring expert manual effort in non-trivial cases; graph-based methods may trade precision for computational cost.The cited approaches may restrict high-dependent branching or synchronization, while the authors' underlying approach targets timing-based synchronization in hardware designs.Source: §5 · pp. 15–16
  • Symbolic-execution IFA approaches do not account for timing and concurrency, while embedded-system symbolic execution has not targeted IFA.Hardware-level tracking, including quantitative timing-sensitive RTL leakage work, is complementary to SystemC abstraction refinement.Source: §5 · p. 16
  • To the authors' knowledge, abstraction refinement had not previously been applied to information flow analyses of embedded systems.Related approaches include shared-state and interference predicates, probabilistic inference for data flow, and safety-oriented path slicing.Source: §5 · pp. 15–16

6 Conclusion

The paper presents automated abstraction refinement for symbolic-execution-based IFA of timed concurrent SystemC models, using exploration and information-flow refinement heuristics. Evaluation on shared bus architectures demonstrates efficient and precise IFA with less manual abstraction selection.

6 Conclusion

  • The approach combines partial descendants and splitters to reduce symbolic state space with path resolution to eliminate spurious flows along paths with potential illegal information flow.It dynamically adapts abstraction levels during IFA of timed concurrent SystemC models.Source: §6 · p. 16
  • Evaluation on several shared bus architectures found that heuristics derive abstractions enabling efficient, precise IFA while reducing manual effort and maintaining scalability.The techniques were implemented and evaluated on those architectures.Source: §6 · p. 16
  • Future work will optimize performance, investigate additional refinement heuristics, and scale the approach to larger, more complex industrial designs.Source: §6 · p. 16
Loading 2609.29645v1…