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

Re:ADA propaganda?

[Actually, I do RTFA]

I don't know one way or the other, but one thing is certain -- anything the tax payers pay for should be owned by the taxpayers and controlled by taxpayers as far as can be deemed appropriate. (So, government buildings cannot be used by the homeless to sleep in!) But something as easy to share as software should definitely be owned by and made available to the people.

And I have shares of Blizzard, I want free WoW. I have shares of Apple, I want free OS X upgrades. I have shares of Microsoft, I want free copies of Vista and Office (feel free to throw out jokes about "why?" Short answer, I like security and I have Vista drivers for my hardware).

The tax payers do own it, and it is controlled by the taxpayers via their proxies in Washington/State Capital. Or sometimes, with software, the taxpayers only license some rights.