NSA (No Such Agency) & Writing Secure Code

The National Security Agency has released a case study showing how to cost-effectively develop code with zero defects.

The case study is the write-up of an NSA-funded project carried out by the U.K.-based Praxis High Integrity Systems and Spre Inc. NSA commissioned the project, which involved writing code for an access control system, to demonstrate high-assurance software engineering.
With NSA's approval, Praxis has posted the project materials, such as requirements, security target, specifications, designs and proofs.

The code itself, called Tokeneer, has also been made freely available.

For this project, three Praxis engineers wrote 10,000 lines of code in 260 person-days, or about 38 lines of code per day.

After the project was finished, a subsequent survey of the code found zero defects.

Moreover, Tokeneer meets or exceeds the Common Criteria Evaluation Assurance Level (EAL) (an ISO-recognized set of software security requirements established by government agencies and private companies). The claim has been that it would be too expensive for commercial software companies to write software programs that would meet EAL 5 standards.

The engineering team used a number of different techniques for writing the code, all bundled into a methodology they call Correctness by Construction, which emphasizes precise documentation, incremental developmental phases, frequent verification and use of a semantically unambiguous language.

The developers wrote the code in a subset of the Ada programming language called SPARK, which allows for annotations that permit static analysis of the program. They used the GNAT Pro integrated developer environment software from AdaCore.