[Popek79] G.J. Popek, M. Kampe, C.S. Kline, A. Stoughton, M. Urban, and E.J. Walton, UCLA Secure Unix, AIFIPS. National Computer Conference 1979:355--364. [This paper describes a secure implementation of the Unix operating system in which much of the implementation was proven correct mathematically.]