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.
展开▼
