Mathematics, Technology, and Trust: Formal Verification, Computer Security, and the U.S. Military

Get BibTex-formatted data

Author

Donald MacKenzie, Garrel Pottinger

Entry type

techreport

Abstract

A distinctive concern in the U.S. military for computer security dates from the emergence of time-sharing systems in the 1960s. This paper traces the subsequent dvelopment of the idea of a \"security kernel\" and of the mathmtical modeling of security, focusing in particular on the paradigmatic Bell LaPadula model. The paper examines the connections between security and formal , deductiv verification of the properties of computer systems. It goes on to discuss differencs between 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 Criteria (the so-called Orange Book), which effectively took its final form in 1983. The paper ends by outlining the fragmentation of computer security since the Orange Book was written.

Journal

IEEE Annals of the History of Computing

Key alpha

Pottinger

Number

Publisher

IEEE

Volume

Publication Date

0000-00-00

Copyright

1997

Language

English

Location

A hard-copy of this is in the Papers Cabinet

Price

10.00

BibTex-formatted data

To refer to this entry, you may select and copy the text below and paste it into your BibTex document. Note that the text may not contain all macros that BibTex supports.

@Techreport{ Pottinger,
	title = "Mathematics, Technology, and Trust: Formal Verification, Computer Security, and the U.S. Military",
	author = "Donald MacKenzie, Garrel Pottinger",
	journal = "IEEE Annals of the History of Computing",
	number = "3",
	publisher = "IEEE",
	volume = "19",
	abstract = "A distinctive concern in the U.S. military for computer security dates from the emergence of time-sharing systems in the 1960s.  This paper traces the subsequent dvelopment of the idea of a \"security kernel\" and of the mathmtical modeling of security, focusing in particular on the paradigmatic Bell LaPadula model.  The paper examines the connections between security and formal , deductiv verification of the properties of computer systems.  It goes on to discuss differencs between 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 Criteria (the so-called Orange Book), which effectively took its final form in 1983.  The paper ends by outlining the fragmentation of computer security since the Orange Book was written.",
	copyright = "1997",
	language = "English",
	price = "10.00",
}