Specification and verification of the UCLA Unix security kernel (Extended Abstract)
Bruce J. Walker, Richard A. Kemmerer, Gerald J. Popek · 1979
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.