The Design and Verification of a Cryptographic Security Architecture

In August 2000 I finally submitted my PhD thesis "The Design and Verification of a Cryptographic Security Architecture", wrapping up my long career as a tenured graduate student. I've put a few chapters online for those who are interested. The thesis has also been published in book form. I'd recommend getting the book form, since it's a considerably revised and updated version of what's in the thesis.

Abstract

Traditional security architectures have concentrated mostly on defining a programming interface (API) and left the internals up to individual implementers. This thesis presents a design for a portable, flexible high- security architecture based on a traditional computer security model involving a kernel implementing a reference monitor which controls access to security- relevant objects and attributes based on a configurable security policy. Layered over the kernel are various objects which abstract core functionality such as encryption and digital signature capabilities, certificate management, and secure sessions and data enveloping (email encryption) in a manner which allows them to be easily moved into cryptographic devices such as smart cards and crypto accelerators for extra performance or security.

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.

Sample Chapters

The main part of the thesis, Chapters 1-5, is available here. These chapters look at an alternative way of building what people have been trying to do with Orange Book B3/A1-type systems, but in a way which is feasible and practical for an open source system where you don't have tens of millions of dollars and 5-10 years available to produce a product.

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.