Secure Xenix™ is an experimental system designed to run on IBM PC/AT workstations. Like Xenix, it is a Unix™ System V implementation on the PC/AT workstation; unlike Xenix, it eliminates the Unix security deficiencies and it enhances security policies. In this paper, we present the design features of Secure Xenix, their integration within Xenix, and some of the lessons learned from this experiment to date.

A new security testing method is proposed that combines the advantages of both traditional "black box" (monolithic functional) testing and "white box" (functional-synthesis-based) testing. The new method allows significant coverage both for security model-based tests and for individual kernel-call tests. It eliminates redundant kernel test cases 1) by using a variant of control synthesis graphs, 2) by analyzing dependencies between descriptive kernel-call specifications, and 3) by exploiting access check separability. A higher degree of test assurance is achieved than that of other security testing methods because the new method helps eliminate cyclic dependencies among test programs for different kernel calls. The application of this method to the testing of the Secure Xenix™ kernel is illustrated.

Secure Xenix * is an experimental system designed to run on IBM PC/AT workstations. Like Xenix, it is a Unix implementation on the PC/AT workstation; unlike Xenix, it eliminates the Unix security deficiencies and it enhances security policies. In this paper, we present the design features of Secure Xenix, their integration within Xenix, and some of the lessons learned from this experiment to date. In addition, we address some of the problems specific to workstations in the security management area. The major design differences between Secure Xenix and other experiments with Unix security enhancements, such as LINUS IV, are also presented. In a companion paper, we present the important problems that arise in the testing of Secure Xenix and their solutions.

A new security testing method is proposed that combines the advantages of both traditional "black box" (monolithic functional) testing and "white box" (functional-synthesis- based) testing. The new method allows significant coverage both for security model-based tests and for individual kernel-call tests. It eliminates redundant kernel test cases (1) by using a variant of control synthesis graphs, (2) by analyzing dependencies between descriptive kernel-call specifications, and (3) by exploiting access check separability. A higher degree of test assurance is achieved than that of other security testing methods because the new method helps eliminate cyclic dependencies among test programs for different kernel calls. The application of this method to the testing of the Secure Xenix* kernel is illustrated. The design and the implementation of Secure Xenix are presented in a companion paper.