We hear a lot about Java and C++, but that doesn't mean they're the only languages developers are using.
Tokeneer was developed for the U.S. National Security Agency (NSA), an outfit known for keeping things secret. Which makes it even more surprising that not only did the NSA acknowledge Tokeneer's existence, but they released it as open source software.
In a nutshell, Tokeneer is a proof-of-concept of what's called "high-assurance software engineering." Secure software, in other words. Software you can trust. Software that must work correctly or else the consequences could be calamitous. And software that's written in Ada—yes, Ada—and developed using Praxis High Integrity Systems (www.praxis-his.com) Correctness-by-Construction (CbyC) methodology, the SPARK Ada language (www.sparkada.com), and AdaCore's GNAT Pro environment (www.adacore.com). The project demonstrates how to meet or exceed all those things that are necessary to achieve high assurance, such as Evaluation Assurance Level 5 in the Common Criteria (whatever that is). All in all, Tokeneer was created in just 260-person days, and implemented in about 10,000 lines of code. Originally a subset of the Ada language, SPARK Ada is designed in such a way that all SPARK programs are legal Ada programs.
No less than Tony Hoare, Fellow of the Royal Society of Microsoft Research, says that "the Tokeneer project is a milestone in the transfer of program verification technology into industrial application. Publication of the full documents for the project has provided unprecedented experimental material for yet further development of the technology by pure academic research. It will serve as a touchstone to chart and measure progress of the basic science of programming, on which the technology is based." Tokeneer is aimed at both the industrial and academic communities, forming an base for research in program verification and as a high-level teaching aid for educators. You can download the entire Tokeneer project, including requirements, security target, specifications, designs, source code, and proofs at www.adacore.com/home/gnatpro/tokeneer/.
Jonathan Erickson
Editor-in-Chief
jerickson@ddj.com
Read more on:
www.adacore.com/home/gnatpro/tokeneer/.
IntellaSys (www.intellasys.net) ,www.python.org,
Tokeneer was developed for the U.S. National Security Agency (NSA), an outfit known for keeping things secret. Which makes it even more surprising that not only did the NSA acknowledge Tokeneer's existence, but they released it as open source software.
In a nutshell, Tokeneer is a proof-of-concept of what's called "high-assurance software engineering." Secure software, in other words. Software you can trust. Software that must work correctly or else the consequences could be calamitous. And software that's written in Ada—yes, Ada—and developed using Praxis High Integrity Systems (www.praxis-his.com) Correctness-by-Construction (CbyC) methodology, the SPARK Ada language (www.sparkada.com), and AdaCore's GNAT Pro environment (www.adacore.com). The project demonstrates how to meet or exceed all those things that are necessary to achieve high assurance, such as Evaluation Assurance Level 5 in the Common Criteria (whatever that is). All in all, Tokeneer was created in just 260-person days, and implemented in about 10,000 lines of code. Originally a subset of the Ada language, SPARK Ada is designed in such a way that all SPARK programs are legal Ada programs.
No less than Tony Hoare, Fellow of the Royal Society of Microsoft Research, says that "the Tokeneer project is a milestone in the transfer of program verification technology into industrial application. Publication of the full documents for the project has provided unprecedented experimental material for yet further development of the technology by pure academic research. It will serve as a touchstone to chart and measure progress of the basic science of programming, on which the technology is based." Tokeneer is aimed at both the industrial and academic communities, forming an base for research in program verification and as a high-level teaching aid for educators. You can download the entire Tokeneer project, including requirements, security target, specifications, designs, source code, and proofs at www.adacore.com/home/gnatpro/tokeneer/.
Jonathan Erickson
Editor-in-Chief
jerickson@ddj.com
Read more on:
www.adacore.com/home/gnatpro/tokeneer/.
IntellaSys (www.intellasys.net) ,www.python.org,
Comments