News
NSA Posts Secrets to Writing Secure Code
- By Joab Jackson
- 10/10/2008
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 (GCN.com).