| This book describes various aspects of cryptographic security architecture design, with a particular emphasis on the use of rigorous security models and practices in the design. The first portion of the book presents the overall architectural basis for the design, providing a general overview of features such as the object model and inter-object communications. The objective of this portion of the work is to provide an understanding of the software architectural underpinnings on which the rest of the book is based.
Following on from this, the remainder of the book contains an analysis of security policies and kernel design that are used to support the security side of the architecture. The goal of this part of the book is to provide an awareness and understanding of various security models and policies, and how they may be applied towards the protection of cryptographic information and data. The security kernel design presented here uses a novel design that bases its security policy on a collection of filter rules enforcing a cryptographic modulespecific security policy. Since the enforcement mechanism (the kernel) is completely independent of the policy database (the filter rules), it is possible to change the behaviour of the architecture by updating the policy database without having to make any changes to the kernel itself. This clear separation of policy and mechanism contrasts with current cryptographic 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.
To provide assurance of the correctness of the implementation, this thesis presents a design and implementation process that has been selected to allow the implementation to be verified in a manner that can reassure an outsider that it does indeed function as required. In addition to producing verification evidence that is understandable to the average user, the verification process for an implementation needs to be fully automated and capable of being taken down to the level of running code, an approach that is currently impossible with traditional methods. The approach presented here makes it possible to perform verification at this level, something that had previously been classed as “beyond A1” (that is, not achievable using any known technology). |