Design Article
Tell us What You Think
We want to know what you thought about this Design. Let us know by adding a comment.
Developing secure code using SPARK (Part 2)
Benjamin M. Brosgol, AdaCore
1/10/2012 8:49 PM EST
Platform considerations
Formally verifying properties of the source program is useful, but it’s the compiled code that actually executes. That raises an important issue; compiler bugs, or platform security vulnerabilities that allow the compiled code to be tampered with, could mean that the running program is not equivalent to its source code. (The hardware, also, could be faulty, but that is a separate subject and outside the scope of this article.)
In theory, compiler issues could be addressed by formally verifying the code generator. That is not a practical solution, however. It is more realistic to take an approach similar to the DO-178B avionics safety standard.7 Requirements-based tests are used to exercise the compiled code with sufficient depth to detect (and work around) faulty generated code, and, for software at the highest level of safety criticality, the developer needs to demonstrate the correctness of any generated code sequences that are not traceable to the source code. This approach has worked well in practice.
Risks related to interference from other applications on the same platform can be mitigated by choosing an architecture that implements time and space partitioning. Examples are ARINC 6538 and MILS9.
Achieving trust
Many factors affect a system’s security. Often the weak link is the human element, and that can negate even the best technology. On the technical side, demonstrating that a system meets its requirements is insufficient if the requirements themselves are incomplete. In addition, important decisions such as the strength of an encryption algorithm are independent of the programming language. Nevertheless, the chosen language(s) and tools can have a significant impact on both the development effort and the degree of confidence that the system’s security properties are met.
In an all-too-common scenario, developers attempt to reinforce their software through extensive testing and by performing static analysis on the existing code. To slightly paraphrase a famous quote by the late computer scientist Edsger Dijkstra, however, these can show the presence of vulnerabilities, but not their absence. From SPARK’s perspective, such a state of affairs is not good enough. A rigorous, mathematically based approach is required, especially at the highest security levels. As noted in a study of source code security analysis tools10, SPARK is an example of a language that is “by design, more suitable for secure programming” than C, C++, and Java, and that will “entirely preclude many common weaknesses or expose others. “
The SPARK language and its accompanying Correctness by Construction methods and supporting toolset have been successfully used on a number of high-security (as well as safety-critical) systems. As these experiences have shown, constructing reliable, safe, and secure software can be accomplished in a cost-effective manner, and without requiring the developers to be experts in formal logic. No programming language can guarantee secure software, but choosing a language that is part of the solution and not part of the problem is a good first step.
References
1. J.G.P. Barnes. High Integrity Software—The SPARK Approach to Safety and Security, Addison-Wesley (2003).
2. A. Burns, B. Dobbing, T. Vardanega. “Guide for the use of the Ada Ravenscar Profile in high integrity systems,” University of York Technical Report YCS-2003-348 (January 2003).
3. J.M. Spivey. The Z Notation: A Reference Manual, 2nd Edition, Prentice-Hall (1985).
4. Y. Moy. SPARK Code Sample: Linear Search.
5. Y.Moy. Ada Gem #68: Let’s SPARK!—Part 1 (June 2009).
6. Y.Moy. Ada Gem #69: Let’s SPARK!—Part 2 (September 2009).
7. RTCA SC-167 / EUROCAE WG-12. RTCA/DO-178B—Software Considerations in Airborne Systems and Equipment Certification (December 1992).
8. ARINC 653 Avionics Application Software Standard Interface, Part 1, Required Services (P1-3) and Part 2 - Extended Services (P2-1).
9. W. Vanfleet, J. Luke, et al., “MILS:Architecture for High-Assurance Embedded Computing,” CrossTalk (August 2005).
10. P.E. Black, M. Kass, M. Koo, E. Fong. Source Code Security Analysis Tool Functional Specification Version 1.1; NIST Special Publication 500-268 v1.1 (February 2011).
About the author
Benjamin Brosgol is a senior member of the technical staff of AdaCore.
He has been involved with programming language design and implementation
for more than thirty years, concentrating on languages and technologies
for high-integrity systems. He was a distinguished reviewer of the
original Ada language specification and a member of the design team for
the Ada 95 revision.
____________________________
Did you find this article of interest? Then visit Military & Aerospace Designline, where we update daily with design, technology, product, and news articles tailored to fit your world. Too busy to go every day? Sign up for our newsletter to get the week's best items delivered to your inbox. Just click here and choose the "Manage Newsletters" tab. You can also follow us on Twitter: @MilAeroDL.
Next: SPARK in practice
Formally verifying properties of the source program is useful, but it’s the compiled code that actually executes. That raises an important issue; compiler bugs, or platform security vulnerabilities that allow the compiled code to be tampered with, could mean that the running program is not equivalent to its source code. (The hardware, also, could be faulty, but that is a separate subject and outside the scope of this article.)
In theory, compiler issues could be addressed by formally verifying the code generator. That is not a practical solution, however. It is more realistic to take an approach similar to the DO-178B avionics safety standard.7 Requirements-based tests are used to exercise the compiled code with sufficient depth to detect (and work around) faulty generated code, and, for software at the highest level of safety criticality, the developer needs to demonstrate the correctness of any generated code sequences that are not traceable to the source code. This approach has worked well in practice.
Risks related to interference from other applications on the same platform can be mitigated by choosing an architecture that implements time and space partitioning. Examples are ARINC 6538 and MILS9.
Achieving trust
Many factors affect a system’s security. Often the weak link is the human element, and that can negate even the best technology. On the technical side, demonstrating that a system meets its requirements is insufficient if the requirements themselves are incomplete. In addition, important decisions such as the strength of an encryption algorithm are independent of the programming language. Nevertheless, the chosen language(s) and tools can have a significant impact on both the development effort and the degree of confidence that the system’s security properties are met.
In an all-too-common scenario, developers attempt to reinforce their software through extensive testing and by performing static analysis on the existing code. To slightly paraphrase a famous quote by the late computer scientist Edsger Dijkstra, however, these can show the presence of vulnerabilities, but not their absence. From SPARK’s perspective, such a state of affairs is not good enough. A rigorous, mathematically based approach is required, especially at the highest security levels. As noted in a study of source code security analysis tools10, SPARK is an example of a language that is “by design, more suitable for secure programming” than C, C++, and Java, and that will “entirely preclude many common weaknesses or expose others. “
The SPARK language and its accompanying Correctness by Construction methods and supporting toolset have been successfully used on a number of high-security (as well as safety-critical) systems. As these experiences have shown, constructing reliable, safe, and secure software can be accomplished in a cost-effective manner, and without requiring the developers to be experts in formal logic. No programming language can guarantee secure software, but choosing a language that is part of the solution and not part of the problem is a good first step.
References
1. J.G.P. Barnes. High Integrity Software—The SPARK Approach to Safety and Security, Addison-Wesley (2003).
2. A. Burns, B. Dobbing, T. Vardanega. “Guide for the use of the Ada Ravenscar Profile in high integrity systems,” University of York Technical Report YCS-2003-348 (January 2003).
3. J.M. Spivey. The Z Notation: A Reference Manual, 2nd Edition, Prentice-Hall (1985).
4. Y. Moy. SPARK Code Sample: Linear Search.
5. Y.Moy. Ada Gem #68: Let’s SPARK!—Part 1 (June 2009).
6. Y.Moy. Ada Gem #69: Let’s SPARK!—Part 2 (September 2009).
7. RTCA SC-167 / EUROCAE WG-12. RTCA/DO-178B—Software Considerations in Airborne Systems and Equipment Certification (December 1992).
8. ARINC 653 Avionics Application Software Standard Interface, Part 1, Required Services (P1-3) and Part 2 - Extended Services (P2-1).
9. W. Vanfleet, J. Luke, et al., “MILS:Architecture for High-Assurance Embedded Computing,” CrossTalk (August 2005).
10. P.E. Black, M. Kass, M. Koo, E. Fong. Source Code Security Analysis Tool Functional Specification Version 1.1; NIST Special Publication 500-268 v1.1 (February 2011).
About the author
Benjamin Brosgol is a senior member of the technical staff of AdaCore.
He has been involved with programming language design and implementation
for more than thirty years, concentrating on languages and technologies
for high-integrity systems. He was a distinguished reviewer of the
original Ada language specification and a member of the design team for
the Ada 95 revision. ____________________________
Did you find this article of interest? Then visit Military & Aerospace Designline, where we update daily with design, technology, product, and news articles tailored to fit your world. Too busy to go every day? Sign up for our newsletter to get the week's best items delivered to your inbox. Just click here and choose the "Manage Newsletters" tab. You can also follow us on Twitter: @MilAeroDL.
Next: SPARK in practice
|
|
|
|
|
Navigate to related information