This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Building Security In: The SPARK Approach to Software Development
Technical Paper
2012-01-0734
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
Software products in the automotive industry are by nature widely distributed and costly to update (recall), so high reliability is clearly of utmost importance. Just as clearly, the increasing reliance on remote access to such systems, for diagnostic and other purposes, has made security an essential requirement, and traditional techniques for software development are proving to be inadequate in dealing with these issues.
Correctness by Construction is a software design and development methodology that builds reliability and security into the system from the start. It can be used to demonstrate, with mathematical rigor, a program's correctness properties while reducing the time spent during testing and debugging. This paper will discuss the use of Correctness by Construction, and its accompanying SPARK1 language technology, to improve automotive systems' security and reliability. (The approach can also account for safely issues, although that is not the focus of this paper.) The SPARK language and toolset avoid vulnerabilities found in other languages and can, for instance, guarantee the absence of run-time errors such as divide-by-zero or buffer overflow. Using the SPARK language and toolset, developers can verify secure information flow through the system and, more generally, demonstrate that security-related properties are achieved.
The approach offered by Correctness by Construction and SPARK is in contrast with the use of so-called retrospective static analysis tools that attempt to find errors or vulnerabilities in existing code. Such tools can only demonstrate the presence of errors (which may be correctable) but cannot show how many errors remain in the system. With Correctness by Construction and SPARK, developers can ensure that errors and vulnerabilities are not introduced in the first place.
Correctness by Construction and SPARK have a growing success rate in applications where failure is not tolerated and where demanding safely or security standards must be met. The technology has been adopted in safety-critical domains including avionics, air traffic control, and rail transportation, and likewise in systems that must meet the highest security levels defined in the Common Criteria (Evaluation Assurance Levels (EAL) 4 through 7).
This paper discusses how to apply Correctness by Construction and the SPARK technology to improve the reliability and security of automotive systems while reducing the costs of development, debugging, and maintenance. It includes examples of previous high-security systems that have been developed using this approach and discusses the applicability of the techniques to automotive systems.
Authors
Topic
Citation
Matthews, S. and Gicca, G., "Building Security In: The SPARK Approach to Software Development," SAE Technical Paper 2012-01-0734, 2012, https://doi.org/10.4271/2012-01-0734.Also In
References
- Barnes, J. High Integrity Software, The SPARK Approach to Safety and Security Addison-Wesley 0-321-13616-0 2003
- Black, P.E. et. al. Source Code Security Analysis Tool Functional Specification Version 1.1 NIST Special Publication 500-268
- Common Weakness Enumeration MITRE Corporation cwe.mitre.org/
- MISRA-C:2004 Guidelines for the use of the C language in critical systems October 2004 www.misra-c.com
- Denning, D.E. Denning, P.J. “Certification of Programs for Secure Information Flow” Communications of the ACM 20 7 July 1977 504 513
- Chapman, R. Hall, A. “Correctness by Construction: Building a Commercial Secure System” IEEE Software 16 1 18 25 Jan Feb 2002
- The Tokeneer Project www.adacore.com/tokeneer
- Chapman, R. Botcazou, E. Wallenburg, A. “SPARKSkein: A Formal and Fast Reference Implementation of Skein” Proceedings of the 14 th Brazilian Symposium on Formal Methods Sao Paulo, Brazil Sept. 2011 Springer-Verlag LNCS 7021 16 27