The kernel itself constitutes a novel design which bases its security policy on a collection of filter rules which enforce a cryptographic module-specific security policy. This clear separation of policy and mechanism contrasts with current security architecture approaches which, if they enforce controls at all, hardcode them into the implementation, making it difficult to either change the controls to meet application-specific requirements or to assess and verify them.
The traditional means of verifying the correctness of the type of system described in this thesis has been to apply various formal methods-based approaches, however this has a number of drawbacks which are examined in some detail. An alternative means of building a trustworthy system based on concepts from cognitive psychology and established software engineering principles is presented, and its application to verifying the correctness of an implementation of the architecture down to the level of the running code is examined.
Finally, the thesis looks at various related issues such as the generation of cryptovariables and the application of the architecture design to cryptographic hardware. The versatility of the architecture has been proven through its use in implementations ranging from 16-bit microcontrollers through to supercomputers, as well as a number of unusual areas such as security modules in ATMs and cryptographic coprocessors for general-purpose computers.
The chapters are The software architecture, wherein the cryptlib software architecture is presented, The security architecture, wherein the cryptlib security architecture is presented, The kernel implementation, wherein the implementation details of the cryptlib security kernel are examined, Verification techniques, wherein existing methods for building secure systems are examined and found wanting, and Verification of the cryptlib kernel, wherein a new method for building a secure system is presented.