MATHEMATICS, TECHNOLOGY, AND TRUST - FORMAL VERIFICATION, COMPUTER SECURITY, AND THE US MILITARY

A distinctive concern in the U.S. military for computer security dates from the emergence of time-sharing systems in the 1960s. This paper t races the subsequent development of the idea of a ''security kernel'' and of the mathematical modeling of security, focusing in particular o n the paradigmatic Bell-LaPadula model. The paper examines the connect ions between computer security and formal, deductive verification of t he properties of computer systems. It goes on to discuss differences b etween the cultures of communications security and computer security, the bureaucratic turf war over security, and the emergence and impact of the Department of Defense's Trusted Computer System Evaluation Crit eria (the so-called Orange Book), which effectively took its final for m in 1983. The paper ends by outlining the fragmentation of computer s ecurity since the Orange Book was written.