Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
I.e., comment lines and empty lines are not counted.
References
Aldous, P., Might, M.: Static analysis of non-interference in expressive low-level languages. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 1–17. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48288-9_1
The ArchiMate Enterprise Architecture Modeling Language. https://www.opengroup.org/archimate-forum/archimate-overview [2021]
Barthe, G., et al.: JACK — a tool for validation of security and behaviour of java applications. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol. 4709, pp. 152–174. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74792-5_7
California Code of Regulations (CCR).: 13 CA ADC §1968.2. Malfunction and diagnostic system requirements – 2004 and subsequent model-year passenger cars, light-duty trucks, and medium-duty vehicles and engines (2022)
Clang 19.0.0 git documentation. DataFlowSanitizer design document. https://clang.llvm.org/docs/DataFlowSanitizerDesign.html [2024]
Cousot, P.: Semantic foundations of program analysis. In S. Muchnick and N. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10, pp. 303–342. Prentice-Hall (1981)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of POPL 1977, pp. 238–252. ACM Press (1977)
Delmas, D., Souyris, J.: ASTRÉE: from research to industry. In: Proceedings of the 14th International Static Analysis Symposium (SAS2007), number 4634 in LNCS, pp. 437–451 (2007)
Feiler, P., Gluch, D., Hudak, J.: Technical Note CMU/SEI-2006-TN-011. The Architecture Analysis & Design Language (AADL): An Introduction. Technical report, Software Engineering Institute, Carnegie Mellon University (2006)
Giacobazzi, R., Mastroeni, I.: Abstract non-interference: parameterizing non-interference by abstract interpretation. In: Jones, N.D., Leroy, X., editors, Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, pp. 186–197. ACM (2004)
ISO 26262. Road vehicles – Functional safety (2018)
ISO/IEC JTC1/SC22/WG14 working group. ISO/IEC 9899:2018 information technology – programming languages – c. Technical Report N2310, ISO & IEC (2018)
Kästner, D.: Applying abstract interpretation to demonstrate functional safety. In: Boulanger, J.-L. (ed.) Formal Methods Applied to Industrial Complex Systems. ISTE/Wiley, London, UK (2014)
Kästner, D., Mauborgne, L., Ferdinand, C., Theiling, H.: Detecting spectre vulnerabilities by sound static analysis. In: Anne Coull, R.F., Chan, S., editor, The Fourth International Conference on Cyber-Technologies and Cyber-Systems (CYBER 2019), vol 4 of IARIA Conferences, pp. 29–37. IARIA XPS Press (2019)
Kästner, D., Mauborgne, L., Wilhelm, S., Mallon, C., Ferdinand, C.: Static Data and Control Coupling Analysis. In: 11th Embedded Real Time Systems European Congress (ERTS2022), Toulouse, France (2022)
Kästner, D., et al.: Finding All Potential Runtime Errors and Data Races in Automotive Software. In SAE World Congress 2017. SAE International (2017)
Kästner, D., Pohland, J.: Program analysis on evolving software. In: Roy, M. (ed.) CARS 2015 - Critical Automotive applications: Robustness & Safety. France, Paris (2015)
Kästner, D., Wilhelm, S., Mallon, C., Schank, S., Ferdinand, C., Mauborgne, L.: Automatic sound static analysis for integration verification of AUTOSAR software. In: WCX SAE World Congress Experience, SAE International (2023)
Kästner, D., et al.: Analyze This! Sound Static Analysis for Integration Verification of Large-Scale Automotive Software. In Proceedings of the SAE World Congress 2019 (SAE Technical Paper). SAE International (2019)
Limited, M.: MISRA C++:2008 Guidelines for the use of the C++ language in critical systems (2008)
Logozzo, F., Mohamed, I.: How to make taint analysis precise. In: Arceri, V., Cortesi, A., Ferrara, P., Olliaro, M. (eds) Challenges of Software Verification. Intelligent Systems Reference Library, vol 238. Springer, Singapore (2023). https://doi.org/10.1007/978-981-19-9601-6_3
Miné, A., Delmas, D.: Towards an industrial use of sound static analysis for the verification of concurrent embedded avionics software. In Proceedings of the 15th International Conference on Embedded Software (EMSOFT’15), pp. 65–74. IEEE CS Press (2015)
Miné, A., et al.: Taking static analysis to the next level: proving the absence of run-time errors and data races with astrée. In: 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016), Toulouse, France (2016)
MISRA (Motor Industry Software Reliability Association) Working Group.: MISRA-C:2012 Guidelines for the use of the C language in critical systems. MISRA Limited (2013)
Radio Technical Commission for Aeronautics. RTCA DO-178C. Software Considerations in Airborne Systems and Equipment Certification (2011)
Software Engineering Institute SEI – CERT Division. SEI CERT C Coding Standard – Rules for Developing Safe, Reliable, and Secure Systems. Carnegie Mellon University (2016)
Souyris, J., Le Pavec, E., Himbert, G., Jégu, V., Borios, G., Heckmann, R.: Computing the worst case execution time of an avionics program by abstract interpretation. In: Proceedings of the 5th International Workshop on Worst-Case Execution Time (WCET) Analysis, pp.21–24 (2005)
Spoto, F., et al.: Static identification of injection attacks in java. ACM Trans. Program. Lang. Syst. 41(3), 1–58 (2019)
State of California – Air Resources Board. Public hearing to consider the proposed revisions to the on-board diagnostic system requirements and associated enforcement provisions for passenger cars, light-duty trucks, medium-duty vehicles and engines, and heavy-duty engines. staff report: Initial statement of reasons. https://ww2.arb.ca.gov/sites/default/files/barcu/regact/2021/obd2021/isor.pdf [Retrieved: Jan 2024], 2021
OMG Systems Modeling Language (OMG SysML\(^{\rm TM}\)) Version 1.6. https://www.omg.org/spec/SysML/1.6/PDF [Retrieved: Jan 2021]
Van Gilder, J.F.: Carb mandated obd compliance reporting update. WCX SAE World Congress Experience WCX 2023, https://www.sae-itc.com/binaries/content/assets/itc/content/hrcs/2023-wcx-carbmandatedobdsignalflowanalysisupdate.pdf [retrieved: Jan. 2024], 2023
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Kästner, D. et al. (2024). Sound Non-interference Analysis for C/C++. In: Ceccarelli, A., Trapp, M., Bondavalli, A., Bitsch, F. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2024. Lecture Notes in Computer Science, vol 14988. Springer, Cham. https://doi.org/10.1007/978-3-031-68606-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-031-68606-1_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-68605-4
Online ISBN: 978-3-031-68606-1
eBook Packages: Computer ScienceComputer Science (R0)