The US National Security Agency has released a case study demonstrating how to write reliable and secure code in a cost-effective manner. The report was produced by UK-based Praxis which wrote code for an access control system dubbed Tokeneer, which meets the stringent ISO software requirements "Common Criteria Evaluation Assurance Level 5", generally considered too expensive for commercial software companies to meet.
Praxis applied a mix of formal and semi-formal methods in order to achieve the results, writing 10,000 lines of code in 260 person days. The process included a specification written in the formal language Z, and was implemented using SPARK Ada, and subsequently verified using a toolset known as the SPARK Examiner.
The release has been greeted with delight from within the academic security community. "The Tokeneer project is a milestone in the transfer of program verification technology into industrial application," distinguished computer scientist Sir Tony Hoare said in a statement. "Publication of the full documents for the project has provided unprecedented experimental material for yet further development of the technology by pure academic research."
Professsor Daniel Jackson at MIT Computer Science Lab added "I’m very excited about the impact this might have in our field, in both teaching and research, and the potential it might have in moving us towards a more open community with greater collaboration between industry and academia, and a more constructive engagement of theory and practice.”
Comments