Tokeneer uses mathematical proofs to establish security
October 9, 2008 —
(Page 1 of 2)
Related Search Term(s): security, AdaCore, Praxis
Why bother testing your software when you can mathematically prove its stability? Six years after Praxis High Integrity Systems got a call from the National Security Agency (NSA) to write a secure and reliable piece of software, that work has matured into Tokeneer, a formal open-source project that at last has made its way into the public domain.
The project became available this past Monday as a demonstration of what's required in a piece of perfectly reliable, bug-free and secure code.
Rod Chapman, principal engineer at Praxis, said that the Tokeneer project actually took only 260 person-days to complete. The project was completed in 2004, but the NSA's involvement slowed it to a veritable crawl. In 2006, the team was allowed to speak at conferences on the project, and two years after that, it was finally available under a permissive license.
Bureaucracy aside, Robert Dewar, CEO and president of AdaCore, said, “It's blithering amazing to get that out of the NSA,” referring to the decision to open-source Tokeneer.
Tokeneer is purely a demonstration application. It runs on Windows, something both Dewar and Chapman both admit removes many of the security claims held by the application. Were it deployed in the wild, Tokeneer would likely live on a small embedded system that controls a biometrically activated security door. The software is designed to take in security credentials from a fingerprint reader or key card, and then control the door mechanism based on those credentials.
It's a fairly simple problem for standard software, but AdaCore, Praxis and the NSA weren't looking for standard. They wanted perfect.
To get perfect software, Chapman and Dewar said that the only place to develop was in the U.K., where formal methods of coding are more commonly used.
“It's another demonstration point in what's [been] a remarkable sequence of demonstration projects showing that formal methods can be used in a practical way,” said Dewar of Tokeneer. “There was a huge interest 20 years ago in proof of correctness. The idea that you wouldn't test your program, but you'd prove them correct using mathematical proof. It was oversold, especially in the U.S. The U.S. overreacted by thinking this is not a practical technology.”