From Openproofs

Jump to: navigation, search

Tokeneer is a demonstration of how to develop highly secure systems, with greater rigor, using the "Correct by Construction" development process including implementation in SPARK Ada.

Tokeneer is an open proof:

  • The Tokeneer implementation is open source software
  • Its proofs are also open source software (see this discussion on its license)
  • There are open source software programs that meet all its tooling requirements:
    • It has a formal specification in the Z language. This can be processed using the LaTeX document processor and and the Z type checker fuzz (tex-zfuzz); both are open source software.
    • An Ada compiler is required to create an executable. GNAT Ada can compile it (GPL)
    • Proof tools for SPARK are required to create and check the proofs. The SPARK GPL Edition meets this requirement.

The Tokeneer project objectives, as described in Tokeneer ID Station EAL5 Demonstrator: Summary Report, can be summarized as followed: "... to undertake an experiment for the introduction of formal methods (mathematically based) into the biometrics prototype called Tokeneer. In addition this experiment hopes to demonstrate the practicality/cost effectiveness of employing the rigorous security standards for assurance as expressed in the Common Criteria... (Praxis) will redevelop part of the Tokeneer system — the Identification Station — with the SPARK Ada high integrity development processes. The subsystem includes functions of biometric authentication and smartcards in a networked system requiring identification and authentication mechanisms... this project should demonstrate not only the feasibility of building real projects following the Common Criteria Guidelines (at EAL 5) but also demonstrate the effectiveness of high assurance techniques like formal methods needed by Government systems to process classified information."

As described in the Summary Report, the entire "Tokeneer" system is actually a larger system that provides protection to secure information held on a network of workstations situated in a physically secure enclave, and has three parts:

  • An Enrolment Station is used to issue a token to an approved user. In order to generate the token the Enrolment Station relies on a Certificate Authority to generate a signed X.509 ID certificate and an Attribute Authority to generate signed X.509 Attribute certificates holding Privilege and Clearance information (Privilege Certificate) and Biometric information (I&A Certificate).
  • The Tokeneer ID Station (TIS) is a stand-alone “trusted” entity responsible for performing biometric verification of the user. To perform this task it makes use of the biometric information in the I&A Certificate on the user’s token and a fingerprint scan read from the user. If a successful identification is made then, assuming the user has sufficient clearance (held on the Privilege certificate), the TIS adds a signed Authorisation Certificate to the user’s token and releases the lock on the enclave door to allow the user access to the enclave.
  • The Workstation checks the Authorisation Certificate to determine whether the user is currently authorised to use the facilities it provides.

The "Tokeneer" project discussed on this page implements just one part: The Tokeneer ID station (TIS).

The Tokeneer ID Station system’s key statistics are:

  • lines of code: 9939
  • total effort (days): 260
  • productivity (lines of code per day, overall): 38
  • productivity (lines of code per day, coding phase): 203
  • defects discovered since delivery: 2 (or 0, see below)

Engineering the Tokeneer Enclave Protection Software discusses Tokeneer in more detail, including interesting issues involving defects. The number of defects found during independent system reliability testing and since delivery is zero, from one point of view. Independent testers from SPRE Inc. logged two in-scope failures from testing; "both were aspects missing from the user manual, and hence do not reflect errors in the TIS Core (the part of the system developed to (the) high-integrity process, and the prime subject of study". But even 2 defects is remarkably low.

It was developed using these processes:

  • Requirements analysis (the REVEAL® process)
  • Formal specification (using the formal language Z)
  • Design (formal refinement of the specification and the INFORMED process)
  • Implementation in SPARK Ada
  • Verification (using the SPARK Examiner toolset)
  • Top-down system testing

See also:

Personal tools