Altran Praxis, a specialist in embedded and critical systems engineering, has been named the inaugural winner of the Microsoft Research Verified Software Milestone Award.
The award is for the company's Tokeneer Project at the US National Security Agency. The technology is a software system that uses biometrics and smart card technology to protect and secure classified buildings.
Protection is provided by a multi-modal biometric access control system. The US National Security Agency (NSA) wanted to determine how to build systems that are cost-effective, ultra-secure and certifiable to EAL5 standards. Praxis worked alongside SPRE Inc. to build a Tokeener ID System to meet these requirements.
Praxis' REVEAL development method was used and the system was specified in the Z formal computing notation. The implementation was in Ada, and SPARK static analysis tools were used.
As the project was security-critical, a security target and security policy model was derived from the Tokeneer Protection Profile. Proofs of security policy were carried out for the Z and the annotated SPARK code.
The technology met the higher levels of the Common Criteria Security Evaluation, the ISO/IEC 15408 standard for computer security certification.
Project leader Dr Janet Barnes and principal engineer Dr Rod Chapman will pick up the award on behalf of Praxis at the 11th International Workshop on Automated Verification of Critical Systems, hosted by the University of Newcastle on 12 to 15 September.
Professor Sir Tony Hoare of Microsoft Research, said, "Congratulations to Janet and Rod as well-deserved recipients of this award. The project has given a persuasive demonstration of the cost effectiveness of formal methods in application to security software, and complements similar experience at Microsoft."
In other recent biometric security news, the FBI recently announced it has made the long-awaited switch from its Automated Fingerprint Identification System (AFIS) to an upgraded, faster solution called Advanced Fingerprint Information Technology (AFIT).
The AFIT replacement prepares the way for going beyond fingerprint identification to other biometrics, including latent palm prints and facial recognition, the next steps in the FBI's multi-year strategy known as the Next Generation Identification (NGI) system.