NSA Posts Secrets to Writing Secure Code

The National Security Agency has released a case study showing how to cost-effectively develop code with zero defects. If adopted widely, the practices advocated in the case study could help make commercial software programs more reliable and less vulnerable to attack, the researchers of the project conclude.

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.

"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."

Developing code with very few defects has long been viewed as a difficult and expensive task, according to a 2006 paper by Praxis engineers describing the work that was published in the International Symposium on Signals, Systems and Electronics.

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) 5, researchers said. Common Criteria is an ISO-recognized set of software security requirements established by government agencies and private companies. Industry observers have long concluded that it would be too expensive for commercial software companies to write software programs that would meet EAL 5 standards.

According to the 2006 paper, 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.

"This case study has shown that software-based security products can be built that are reliable, verifiable and cost effective against Common Criteria guidelines," the paper concluded. "The bar has been raised for both procurers and suppliers."

About the Author

Joab Jackson is the chief technology editor of Government Computing News.