Specification and verification of the UCLA Unix security kernel

Abstract

Data Secure Unix, a kernel structured operating system, was constructed as part of an ongoing effort at UCLA to develop procedures by which operating systems can be produced and shown secure. Program verification methods were extensively applied as a constructive means of demonstrating security enforcement. Here we report the specification and verification experience in producing a secure operating system. The work represents a significant attempt to verify a largescale, production level software system, including all aspects from initial specification to verification of implemented code. © 1980, ACM. All rights reserved.