Praxis develops vault access system

As the result of work developing secure software for Mondex, now part of Mastercard, the engineering team at Praxis, in Bath, UK, was approached by the US National Security Agency (NSA) to develop software for an unclassified research demonstration programme.
The challenge the NSA set the engineers was to rebuild software for the Tokeneer, a system that controls access to a vault through the use of a smart-card reader/writer and a fingerprint reader. However, this was no ordinary software development task – the software itself had to be robust, reliable and error free.

Most of the engineering on the project was conducted by a team of three specialists over a nine-month period; once completed, it was delivered to the NSA.

According to Dr Rod Chapman, a principal engineer at Altran Praxis, the software development process involved a great deal of work precisely defining the environment in which the system was to function.

The team began by creating a specific engineering process requirement for the system. At this stage, the engineers documented the operational environment of the system, detailing how it would function in the real world. From that, they built a requirements specification and created a security policy – a clear statement of the security properties that the system had to enforce.

For the next step, the team created a mathematical specification of the system. Chapman said that, in doing so, the engineers were forced to think hard about the operational environment of the system and, as a result, they gained a level of understanding of it that they might not have otherwise had.

’We needed to focus on the entire security properties of the system, taking into account the most malicious or unlikely things that might occur to it,’ he added. ’The formalisation process was key to enabling us to understand the entire behaviour of the system – not just what it’s supposed to do on a good day, but all of the possible scenarios where things might go wrong.’

During the course of the development, the team followed the Common Criteria, an international ISO standard used in the creation of secure systems, to demonstrate that the approach it was following could meet the level of discipline and rigour demanded by that standard.
With the formal specification complete, the engineers undertook the design and implementation of the software itself.

’The implementation was executed in SPARK, a slightly unusual programming language that is designed from scratch for building high-assurance systems,’ said Chapman. ’It enables various styles of analysis and verification to be performed that guarantee the absence of very large classes of defects and, more importantly, errors in the software.’

The completed software was then independently tested – another US company was contracted to discover if it could find any bugs in the system. It found none.

After the software was completed to the satisfaction of the NSA, the Praxis engineers asked if it might be possible to release the whole project – all the designs, the requirements and the source code – to the outside world. Eventually, the NSA gave Praxis a licence to distribute the archive of the project in both readable and modifiable form.