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 1)
Benjamin M. Brosgol, AdaCore
1/3/2012 8:26 PM EST
The complexities of general-purpose language
Unfortunately, all general-purpose language—including Ada, C, C++, and Java—are too complex to be used, at their full generality, for high-integrity software. They may have features with implementation-dependent or undefined effects, or error-prone syntax or semantics, and in any event the full languages or their run-time libraries are too complex to support the analysis needed to demonstrate the relevant security or safety properties.
One solution is to choose a language subset that avoids problematic features. MISRA C4 and MISRA C++5 take this route, but neither C nor C++ was originally designed with a focus on high-integrity systems. It’s difficult to reorient a language’s underlying philosophy through a subset. In addition, both MISRA C and MISRA C++ include rules that are subject to interpretation, and thus may be enforced differently by different tools.
Java is another possible candidate for subsetting, but its highly dynamic nature, along with its dependence on automatic garbage collection for storage management, complicates the analysis needed to demonstrate time and space predictability. Subsetting can’t effectively solve these problems without largely negating the reasons for considering Java in the first place. Java’s extensive class libraries, moreover, would need to be restricted and/or rewritten, again defeating one of the language’s major benefits.
Ada provides a more appropriate basis for subsetting. Since the language was originally designed for high-integrity software, it has the relevant foundation for reliability, and it does not require the memory management complexity of Java. Array indices are checked to make sure that they are within bounds, strong typing prevents misusing the value of one type as though it were of another type, and integer overflow raises an exception instead of wrapping around. The language also permits the inclusion of range constraints on scalar data; for example, an integer can be declared to be within the range 0 through 100. The ability to specify scalar range constraints increases the accuracy of bounds analysis and helps catch logic errors early.
Subsetting in Ada can actually be controlled by the application. The pragma Restrictions feature, introduced in Ada 95, allows the program to specify features that are not being used and thus do not require run-time support. The simpler run-time libraries are easier to analyze and also reduce the code footprint. The Ravenscar profile6, a subset of concurrency features amenable to safety or security certification, is specified as a set of such restrictions.
Defining a subset is useful and necessary but still does not directly address the issue of deducing security- or safety-related properties from the program text. For that purpose, a notation is needed that allows the developer to specify a program’s contracts: statically verifiable annotations that identify data object dependences, subprogram preconditions and postconditions, loop invariants, and similar properties. The SPARK language7, originally designed by Praxis High-Integrity Systems (now Altran Praxis), takes this approach, using a specialized form of comment for its annotations.
Part two of this article will summarize the basic elements of the SPARK technology and show how it addresses software security issues.
References
1. Common Criteria Portal.
2. MITRE Corp. Common Weakness Enumeration.
3. ISO/IEC JTC 1/SC 22/WG 23 Programming Language Vulnerabilities, Technical Report TR 24772. Guidance to avoiding vulnerabilities in programming languages through language selection and use (October 2010).
4. MISRA. Guidelines for the Use of the C Language in Critical Systems (October 2004).
5. MISRA. Guidelines for the Use of the C++ Language in Critical Systems (June 2008).
6. 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).
7. J. Barnes. High Integrity Software – The SPARK Approach to Safety and Security, Addison-Wesley, (2003).
Related articles
Automating rule sets for safety-critical HDL coding
High-integrity object-oriented programming with Ada
Cut the cost of code development with traceability tools
MILS architecture simplifies design of high-assurance systems
Case study: Threat simulation for multi-port radar and electronic warfare systems
HiRel for space
Addressing obsolescence with hardware abstraction layers
Leakage-resistant protocols protect high-security applications
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 at @MilAeroDL.
Unfortunately, all general-purpose language—including Ada, C, C++, and Java—are too complex to be used, at their full generality, for high-integrity software. They may have features with implementation-dependent or undefined effects, or error-prone syntax or semantics, and in any event the full languages or their run-time libraries are too complex to support the analysis needed to demonstrate the relevant security or safety properties.
One solution is to choose a language subset that avoids problematic features. MISRA C4 and MISRA C++5 take this route, but neither C nor C++ was originally designed with a focus on high-integrity systems. It’s difficult to reorient a language’s underlying philosophy through a subset. In addition, both MISRA C and MISRA C++ include rules that are subject to interpretation, and thus may be enforced differently by different tools.
Java is another possible candidate for subsetting, but its highly dynamic nature, along with its dependence on automatic garbage collection for storage management, complicates the analysis needed to demonstrate time and space predictability. Subsetting can’t effectively solve these problems without largely negating the reasons for considering Java in the first place. Java’s extensive class libraries, moreover, would need to be restricted and/or rewritten, again defeating one of the language’s major benefits.
Ada provides a more appropriate basis for subsetting. Since the language was originally designed for high-integrity software, it has the relevant foundation for reliability, and it does not require the memory management complexity of Java. Array indices are checked to make sure that they are within bounds, strong typing prevents misusing the value of one type as though it were of another type, and integer overflow raises an exception instead of wrapping around. The language also permits the inclusion of range constraints on scalar data; for example, an integer can be declared to be within the range 0 through 100. The ability to specify scalar range constraints increases the accuracy of bounds analysis and helps catch logic errors early.
Subsetting in Ada can actually be controlled by the application. The pragma Restrictions feature, introduced in Ada 95, allows the program to specify features that are not being used and thus do not require run-time support. The simpler run-time libraries are easier to analyze and also reduce the code footprint. The Ravenscar profile6, a subset of concurrency features amenable to safety or security certification, is specified as a set of such restrictions.
Defining a subset is useful and necessary but still does not directly address the issue of deducing security- or safety-related properties from the program text. For that purpose, a notation is needed that allows the developer to specify a program’s contracts: statically verifiable annotations that identify data object dependences, subprogram preconditions and postconditions, loop invariants, and similar properties. The SPARK language7, originally designed by Praxis High-Integrity Systems (now Altran Praxis), takes this approach, using a specialized form of comment for its annotations.
Part two of this article will summarize the basic elements of the SPARK technology and show how it addresses software security issues.
References
1. Common Criteria Portal.
2. MITRE Corp. Common Weakness Enumeration.
3. ISO/IEC JTC 1/SC 22/WG 23 Programming Language Vulnerabilities, Technical Report TR 24772. Guidance to avoiding vulnerabilities in programming languages through language selection and use (October 2010).
4. MISRA. Guidelines for the Use of the C Language in Critical Systems (October 2004).
5. MISRA. Guidelines for the Use of the C++ Language in Critical Systems (June 2008).
6. 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).
7. J. Barnes. High Integrity Software – The SPARK Approach to Safety and Security, Addison-Wesley, (2003).
Related articles
Automating rule sets for safety-critical HDL coding
High-integrity object-oriented programming with Ada
Cut the cost of code development with traceability tools
MILS architecture simplifies design of high-assurance systems
Case study: Threat simulation for multi-port radar and electronic warfare systems
HiRel for space
Addressing obsolescence with hardware abstraction layers
Leakage-resistant protocols protect high-security applications
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 at @MilAeroDL.
|
|
|
|
|
Navigate to related information