NSA edges into the open source realm with Tokeneer

By Angela Gunn | Published October 6, 2008, 6:15 PM

Components of a National Security Agency case study designed to demonstrate that open source, high security and cost effectiveness can all co-exist have been turned over to the open source community.

Tokeneer manages access control for a biometric ID verification tool. It's based on the SPARK subset of Ada developed by the UK's Praxis and was funded by the US National Security Agency, which chose to make information on the development and research available.

Praxis CEO Rod Chapman has described Spark, his company's product, as being unique in providing a decidable, sound information flow analysis framework. (Spark, essentially, mandates good design principles, not to mention squeaky-clean Ada code.) Such an IFA framework allows rigid separation of security levels.

In addition to serving as proof that an open source project can meet stringent security requirements, Tokeneer had timeliness and cost-of-development goals. According to Praxis, the project required 260 days from start to release, and contains 9939 lines of code. Since delivery of Tokeneer, one code defect has been unearthed.

Some observers on Monday were skeptical. On Slashdot, one member whose handle is "Wulfstan" grumbled that though Tokeneer has been released as open source, the SPARK tool chain is not itself governed by open source rules.

Downloads of Tokeneer and pertinent information are available from AdaCore.

Tokeneer has been in the works for several years. A paper on the project as it relates to high-assurance software development was presented in March at Microsoft's Cambridge research facility.