Fresh from my INBOX:
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.
More on the Tokeneer project here.
Update: dds offers constructive criticism on the project’s source code after reviewing a single file!