NSA posts secrets to writing secure code in SPARK

NSA posts secrets to writing secure code in SPARK

[Arthur Evans Jr]

The relevance of this fascinating item to Ada shows up near the end of 
this posting in comp.risks. Many of us have believed this sort of thing 
for years, so it's good to see an independent verification.

Art Evans

-----------------------------

Reused without explicit authorization under blanket permission granted 
for all Risks-Forum Digest materials. The author(s), the RISKS 
moderator, and the ACM have no connection with this reuse.


RISKS-LIST: Risks-Forum Digest  Friday 17 October 2008  Volume 25 : 
Issue 39

Date: October 14, 2008 11:58:28 AM EDT From: "Jim Innes" 
<james.innes@carrierclasstowers.com> Subject: NSA posts secrets to 
writing secure code

Joab Jackson, Tokeneer case study serves as an example of writing 
low-defect, highly-reliable code, researchers claim, *Government 
Computer News* weekly newsletter.

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

Re: NSA posts secrets to writing secure code in SPARK

[Randy Brukardt]

"Arthur Evans Jr" <nospam@someISP.net> wrote in message 
news:nospam-9CECCC.18172417102008@earthlink.vsrv-sjc.supernews.net...
> The relevance of this fascinating item to Ada shows up near the end of
> this posting in comp.risks. Many of us have believed this sort of thing
> for years, so it's good to see an independent verification.

Well, it's just a rehash to the Tokeneer stuff, which was discussed here two 
weeks ago. You can find a link to the original GCN article on the AdaIC web 
site http://www.adaic.com/news/nsa-0-defects.html (which was posted on 
Tuesday).

                                  Randy.