Cif: A Static DLM Analyzer to Assure Correct Information Flow in C

For safety-critical and security-critical Cyber-Physical Systems in the domains of aviation, transportation, automotive, medical applications and industrial control correct software implementation with a domain-specific level of assurance is mandatory. Particularly in the aviation domain, this demonstration demands new technologies to convince authorities of the proper implementation of avionic systems with increasing complexity. Two decades ago, Andrew Myers developed the Decentralized Label Model (DLM) to model and prove correct information flows in applications’ source code. Unfortunately, the proposed DLM targets Java applications and is not applicable for today’s avionic systems. Reasons are issues with the dynamic character of objectoriented programming or the in general uncertain behaviors of features like garbage collectors of the commonly necessary runtime environments. Hence, highly safety-critical avionics are usually implemented in C. Thus, we adjusted the DLM to the programming language C and developed a suitable tool checker, called Cif. Apart from proving the correctness of the information flow statically, Cif is also able to create a dependency graph to represent the implemented information flow graphically. Even though this paper focuses on the avionic domain, our approach can be applied equally well to any other safety-critical or securitycritical system. This paper demonstrates the power of Cif and its capability to graphically illustrate information flows, and discusses its utility on selected C code examples.      «

For safety-critical and security-critical Cyber-Physical Systems in the domains of aviation, transportation, automotive, medical applications and industrial control correct software implementation with a domain-specific level of assurance is mandatory. Particularly in the aviation domain, this demonstration demands new technologies to convince authorities of the proper implementation of avionic systems with increasing complexity. Two decades ago, Andrew Myers developed the Decentralized Label...     »