Automatic Verification of (Un)intended Data and Control Flows in Embedded Software

Data and control flows are essential to software architecture and are commonly defined during the design phase. Yet, they are rarely verified later during implementation. Instead, most verification activities focus on guideline compliance, functional tests, and robustness. In this paper, we dive deeper into the topic of flow analysis and discuss which methods can be used to reliably detect unintended behavior and prevent functional errors, such as forbidden communication between processes of different criticality, accidental disclosure of sensitive data, and even algorithmic errors. Using concrete examples, we explain the different types of flow dependencies and introduce the method of specification-driven code slicing, which can automatically verify the absence of certain unintended flows. This addresses certification requirements from automotive engineering (“Freedom from Interference”), aerospace (“Data and Control Coupling”), and industrial automation (“Restricted Data Flow”) by asserting the safety and security properties of software applications. The outlined method can significantly reduce the number of issues discovered late in testing campaigns.

This paper was presented at Embedded World Conference 2024.