Title :
Implementing a verification methodology for McCullough security
Author :
Rosenthal, David
Author_Institution :
Odyssey Res. Associates, Inc., Ithaca, NY, USA
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;
Conference_Titel :
Computer Security Foundations Workshop II, 1989., Proceedings of the
Conference_Location :
Franconia, NH
DOI :
10.1109/CSFW.1989.40596
