NSA Open Sources Tokeneer Research Project

An anonymous reader writes to mention that the Tokeneer research project has been released to the open source community by the US National Security Agency. The main goal of this project was to show how highly secure software can be developed cost-effectively. "Tokeneer has been written in SPARK Ada, a high level programming language designed for high-assurance applications. Originally a subset of the Ada language, it is designed in such a way that all SPARK programs are legal Ada programs. Ada is the natural choice for mission-critical, high-integrity systems due to its combination of flexibility, reliability and ease of use, and SPARK further adds a static verification toolset that combines depth, soundness, efficiency and formal guarantees."

Comments

VERIFICATION

[A non-mouse Coward]

It's all about the formal verification, or the "correctness" of the implementation (binary executable) of the problem. If you follow the works of the late Edsger Dijkstra, he argued that all code should really be an abstraction of a formal mathematical proof of a solution to a problem. Now, most "agile" software developers through that out the window as shite, but we need to find a compromise somewhere in between.

If we were able to do formal verification of a binary, then the world wouldn't need to see source code to know you can trust third-party written code. Ada or whatever language, the research significance here is that the characteristics of the language and compilation that yields positive steps towards formal verification. So, maybe for you "secure" is "I patched it and today's signature database from [insert vuln scanner] doesn't find any holes", but for three letter institutions (and anyone who has worked diligently enough in security to become jaded like me) that's just not good enough. A better definition of "secure" software would be "I know what it is intended to do and I can formally prove it does that and only that."

Word of the day is verification.