Sound Non-interference Analysis for C/C++

Homologation of vehicles in markets that are subject to U.S. regulations requires, as a part of the certification documentation, an analysis of all input and output signals that influence the control or diagnosis of any emissions-related component or system. On-board diagnostic (OBD) systems are required for every component and system that can cause increases in emissions. In this article we present a sound non-interference analysis at the C/C++ code level, that allows to automatically determine which output signals can be influenced by a given input signal, or vice versa, and which can demonstrate the independence between selected input and output signals. The analysis is based on integrating a generic taint analysis framework into a sound static runtime error analyzer that can take the impact of runtime errors on data and control flow into account. Soundness of the underlying analysis is an essential property since it provides full data and control coverage; in particular it can guarantee that all data and function pointer values have been taken into account. Our approach can be applied to signal flow analysis, to demonstrate freedom of interference between software components at the source code level, to show compliance between source code and software architecture, and to satisfy cybersecurity requirements. We will outline the underlying theoretical concepts, present our taint propagation algorithm for non-interference analysis, and report on practical experience on industry-grade example projects.