Implementing a verification methodology for McCullough security

Author

Rosenthal, David

Author_Institution

Odyssey Res. Associates, Inc., Ithaca, NY, USA

fYear

1989

fDate

11-14 Jun 1989

Firstpage

133

Lastpage

140

Abstract

Previously, the author described a methodology for proving McCullough security (also called RADC hook-up security, restriction, and flow security) (Proc. Comput. Security Found. Workshop, pp.90-97, Mitre Tech Report M88-37, June 1988). He describes how to build a theorem generation mechanism for the validation of a security property which implies McCullough Security. He makes use of the USL language

Keywords

formal specification; program verification; security of data; specification languages; theorem proving; McCullough security; RADC hook-up security; USL language; flow security; proving McCullough security; security property; theorem generation mechanism; verification methodology; Delay; Government; Mechanical factors; Security;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Security Foundations Workshop II, 1989., Proceedings of the

Conference_Location

Franconia, NH

Type

conf

DOI

10.1109/CSFW.1989.40596

Filename

40596

Link To Document

https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3196781