This paper describes a set of principles and methods for validating, via testing, security properties of a security kernel. A basic objective is to reduce the number of tests needed by combining the advantages of “black-box” testing and “program-structure-based” testing. An important aspect of the method is the use of an “access check graph” that models the dependencies that exist among the security checks performed by the kernel. An extensive discussion of using the method to test the Secure Xenix Kernel is given.

The presentation is largely descriptive, illustrated with many examples drawn from Xenix. The purpose of the paper, to provide an exposition of the method so that others may adapt it, does suffer somewhat from this very detailed description. However, the difficulty of abstracting the essential ideas may be an inherent problem of this topic. Despite this difficulty, the paper does provide a very comprehensive and complete discussion of the problem of testing for security properties, a very different exercise from that of testing for functional or performance properties.

The paper is intended for a reader who is familiar with both the testing literature and the security literature, and I suggest that it is essential reading for those interested in the practical validation of secure systems that are being built now.