TABLE OF CONTENTS The goal of this book was to examine new techniques for designing and verifying a high-security kernel for use in cryptographic security applications. The vehicle for this was an implementation of a security kernel employed as the basis for an object-based cryptographic architecture. This was combined with an analysis of existing methods of verifying security kernels, followed by a proposed new design and verification strategy. The remainder of this section summarises each individual contribution.
The cryptlib security kernel is a separation kernel that acts as a mediator for all interactions within the architecture. Communication from subject to object is carried out through message passing, with the kernel acting as a reference monitor for all accesses by subjects to objects. The kernel is a standard separation kernel on top of which more specific security policies can be implemented.
Accompanying the kernel security mechanism is a policy portion that consists of a collection of filter rules that are applied to all messages processed by the kernel, which means all messages sent to objects, which in turn means all interactions with objects.
The use of this kind of kernel is unique in (non-classified) encryption technology. The kernelised design has proven to be both flexible and powerful, since the filter rules provide a powerful and user-configurable means of expressing an arbitrary security policy that doesn't usually conform to more traditional policy models such as Bell-LaPadula or Clark-Wilson. This policy will typically also include features such as...
