NSA posts secrets to writing secure code
Tokeener case study serves as an example of writing low-defect, highly-reliable code, researchers claim.
The National Security Agency has released a casestudy 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 Secure Software Engineering.
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 Adaprogramming 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."