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
SPARK in practice
SPARK has been successfully used in a number of high-security systems. Here is a brief sample.
Tokeneer
The Tokeneer ID Station project1 was sponsored by the U.S. National Security Agency (NSA) to investigate whether SPARK and the Correctness by Construction methods could be used in practice to develop a system that would meet EAL5 from the Common Criteria. The effort involved requirements analysis, formal specification (in Z), design (formal refinement of the specification), implementation in SPARK, verification through the SPARK toolset, and top-down testing. A team from Praxis High-Integrity Systems, now Altran Praxis, successfully completed the project on schedule and within budget, at a level of effort that was much less than is typically required for high-integrity software.
Since the delivery of the system, only four minor defects in the ten thousand lines of SPARK code have been reported. The proof activity that was used could be applied at EAL7. All of the project material—requirements, specification, source code, tests, etc.—has been made available by NSA and may be downloaded.
SPARKSkein
Skein is a cryptographic hash function, with a reference implementation in C, that has been entered in the U.S. National Institute of Standards and Technology (NIST) competition for the new Secure Hash Algorithm (SHA-3) standard. Such hash functions are used to compute short digests of long messages and are one of the key building blocks of digital communication and cryptographic systems.
SPARKSkein2 is a SPARK implementation of the Skein algorithm. It was developed jointly by Altran Praxis and AdaCore with the goals of readability, portability (across machines of any word size and endianness, with no pre-processing required), performance, and formal demonstration of freedom from run-time errors. These objectives were met, showing that the use of rigorous methods to achieve correctness did not have to compromise portability or efficiency. In fact, developing the SPARK version uncovered an integer overflow problem in the C reference implementation. SPARKSkein is available through the Skein website.
References
1. J. E. Barnes, R. Chapman, R. Johnson, J. Widmaier, D. Cooper, B. Everett. "Engineering the Tokeneer Enclave Protection Software,” 1st IEEE International Symposium on Secure Software Engineering; (March 2006).
2. R. Chapman, E. Botcazou, and A. Wallenburg. “SPARKSkein: A Formal and Fast Reference Implementation of Skein,” in Proc. of the 14th Brazilian Symposium on Formal Methods; Sao Paulo, Brazil (September 2011).
SPARK has been successfully used in a number of high-security systems. Here is a brief sample.
Tokeneer
The Tokeneer ID Station project1 was sponsored by the U.S. National Security Agency (NSA) to investigate whether SPARK and the Correctness by Construction methods could be used in practice to develop a system that would meet EAL5 from the Common Criteria. The effort involved requirements analysis, formal specification (in Z), design (formal refinement of the specification), implementation in SPARK, verification through the SPARK toolset, and top-down testing. A team from Praxis High-Integrity Systems, now Altran Praxis, successfully completed the project on schedule and within budget, at a level of effort that was much less than is typically required for high-integrity software.
Since the delivery of the system, only four minor defects in the ten thousand lines of SPARK code have been reported. The proof activity that was used could be applied at EAL7. All of the project material—requirements, specification, source code, tests, etc.—has been made available by NSA and may be downloaded.
SPARKSkein
Skein is a cryptographic hash function, with a reference implementation in C, that has been entered in the U.S. National Institute of Standards and Technology (NIST) competition for the new Secure Hash Algorithm (SHA-3) standard. Such hash functions are used to compute short digests of long messages and are one of the key building blocks of digital communication and cryptographic systems.
SPARKSkein2 is a SPARK implementation of the Skein algorithm. It was developed jointly by Altran Praxis and AdaCore with the goals of readability, portability (across machines of any word size and endianness, with no pre-processing required), performance, and formal demonstration of freedom from run-time errors. These objectives were met, showing that the use of rigorous methods to achieve correctness did not have to compromise portability or efficiency. In fact, developing the SPARK version uncovered an integer overflow problem in the C reference implementation. SPARKSkein is available through the Skein website.
References
1. J. E. Barnes, R. Chapman, R. Johnson, J. Widmaier, D. Cooper, B. Everett. "Engineering the Tokeneer Enclave Protection Software,” 1st IEEE International Symposium on Secure Software Engineering; (March 2006).
2. R. Chapman, E. Botcazou, and A. Wallenburg. “SPARKSkein: A Formal and Fast Reference Implementation of Skein,” in Proc. of the 14th Brazilian Symposium on Formal Methods; Sao Paulo, Brazil (September 2011).
|
|
|
|
|
Navigate to related information