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 (

comments powered by Disqus


  • Visual Studio 2019 for Mac v8.9 Ships with .NET 6 Preview 1 Support

    During its Ignite 2021 online event for IT pros and developers this week, Microsoft shipped Visual Studio 2019 for Mac v8.9, arriving with out-of-the-box support for .NET 6 Preview 1, which the company also released recently.

  • Black White Wave IMage

    Neural Regression Using PyTorch: Training

    The goal of a regression problem is to predict a single numeric value, for example, predicting the annual revenue of a new restaurant based on variables such as menu prices, number of tables, location and so on.

  • Microsoft Ships Visual Studio 2019 v16.9 Servicing Baseline Release

    Microsoft is urging enterprises and professional coders to standardize on the new Visual Studio 2019 v16.9, a servicing baseline release that's guaranteed to receive official support for an extended period.

Upcoming Events