National Security Agency (NSA), has released a study showing how to cost-effectively develop code with zero defects. The U.K.-based Praxis High Integrity Systems and Spre Inc. wrote code for an access control system, to demonstrate high-assurance software engineering.
The Tokeneer project is a milestone in the transfer of program verification technology into industrial application,” said Sir Tony Hoare, noted Microsoft Research computer scientist, in a statement. “Publication of the full documents for the project has provided unprecedented experimental material for yet further development of the technology by pure academic research.”
The development process applied to the Tokeneer ID Station high-integrity development can be summarised in terms of the following key phases:
- Requirements analysis (the REVEAL® process)
- Formal specification (using the formal language Z)
- Design (formal refinement of the specification and the INFORMED process)
- Implementation in SPARK Ada
- Verification (using the SPARK Examiner toolset)
- Top-down system testing
This development and research work has now been made available by the NSA to the software development and security communities in an effort to prove that it is possible to develop secure systems rigorously in a cost effective manner.
By using Spark Ada, a static check was made of the software before it was run, to ensure all the possible conditions led to valid outcomes. In more than 9,939 lines of code, no defects were found after the testing and remediation process was completed.
Ada was named for Augusta Ada King, Countess of Lovelace, daughter of Lord Byron. In the early 19th century, she published what is considered by most to be the world’s first computer program, to be run on a prototype of a computer designed by Charles Babbage, called the Analytical Engine.