Abstract: “The UCLA Data Secure Unix operating system is intended as a demonstration that verifiable data security with general purpose functionality is attainable today in medium scale computing systems. More specifically, the UCLA system has the characteristic that data security, the assurance that data can not be directly read or modified without specific permission, is enforced via a limited amount of kernel software. High levels of care are being applied to demonstrate that the security properties of that software are correctly implemented. In addition, the system is designed so that confinement can be demonstrated by audit of some additional, isolated code.

To achieve these goals, a number of design and implementation principles have been integrated into a single system. These include a tightly constrained base kernel, a second-level policy kernel, a well known and accepted operating system interface, implementation in the high-level language Pascal, and application of formal, semi-automated program verification methods to the source code of both kernels. The system interface is essentially identical to Unix as released by Bell Laboratories,9 and the software presently runs on DEC PDP-III45s and PDP-II!70s. The kernel structures and verification procedures, together with the choice of language, provide a powerful means by which the systerm’s security and integrity can be demonstrated and assessed.”

That came with major downsides, too, due to effects of legacy code not designed for security, weak methods for managing complexity, immature tools for verification, and early hardware. More details in paper.