LOGIN | REGISTER NOW | SUBSCRIBE
 
 
News on Monday
more>>
SharePoint Tech Report
more>>


   

 
 
Download Current Issue
ISSUE 7/1/2009 PDF

Need Back Issues?
DOWNLOAD HERE

Receive the print Edition?


 
Is the mystery Borland suitor Serena?
Borland software is considering an offer from another company after a preliminary deal with MicroFocus. Is Serena the new company?
06/30/2009 01:55 PM EST

Windows 7 - An eBayer's dream product?
Windows 7 pre-orders can make people money on eBay.
06/29/2009 03:48 PM EST

Know thine cloud provider
Cloud computing require companies to understand compliance and regulation. Third parties will play a big role in regulated industries.
06/29/2009 02:58 PM EST

 

Microsoft Worldwide Partner Conf.
7/13/2009 to 7/16/2009
New Orleans
Microsoft

OSCON (Open Source Convention)
7/20/2009 to 7/24/2009
San Jose
O'Reilly Media

XBRL Technology Workshop & Summit
7/28/2009 to 7/30/2009
Santa Clara
XBRL US

ACM SIGGRAPH
8/3/2009 to 8/7/2009
New Orleans
ACM SIGGRAPH

OpenSource World (formerly LinuxWorld)
8/12/2009 to 8/13/2009
San Francisco
IDG World Expo


 
print Printable version 
Most Read Latest News Blog Resources
Kapow automates website data retrieval
Kapow Technology's Web Data Server 7.0 can be used to create modules that navigate through...

Oracle's Fusion 11g lays groundwork for ERP platform
Fusion's components are standards-based and integrated, but some abilities are lost if non...

COBOL’s future lies in the clouds
After 50 years of use in businesses, COBOL is still lingering around mainframes. But the s...

Digg!  Digg
Reddit  Reddit
Slashdot  Slashdot
Share on facebook  Facebook
Share on Twitter  Twitter

Tokeneer uses mathematical proofs to establish security


By Alex Handy
October 9, 2008 — 
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.”

But that technology is at the core of Praxis' Spark, a framework designed around reliability, security and provability. Chapman and two co-workers actually wrote Tokeneer on Spark and used mathematical proofs to show that there were no buffer overflows or other anomalies. Spark, said Chapman, actually prevents developers from making such errors during coding and can offer the assurance that the software is perfect.

But why Ada? It's not exactly a mainstream programming language. “There is not any other basis for building such a powerful technology,” said Chapman. “Why Ada? Because it remains the best basis for building such technology.”

Dewar said that “Ada has settled into a niche of high-reliability programs. Most new avionics systems are Ada-based including the Boeing 787. Ada was designed for that purpose.”

Tokeneer is available online at AdaCore's website.  A comprehensive description of the project and its development is available at  www.adacore.com/multimedia/tokeneer/Tokeneer_Report.pdf.


Related Search Term(s): security, AdaCore, Praxis


Share this link: http://www.sdtimes.com/link/32952
 

Add comment


Name*
Email*  
Country     


  • Comment
  • Preview
Loading