Verification of secure distributed systems in higher order logic:
A modular approach using generic components

J. Alves-Foss, K. Levitt

A generalization of D. McCullough's (1987; 1988) restrictiveness
model is given as the basis for providing security properties for
distributed system designs. This generalization is mechanized for an
event-based model of computer systems in the HOL (higher order logic)
system to prove the composability of the model and several other
properties about the model. A set of generalized classes of system
components is developed and it is shown for which families of user
views they satisfy the model. Using these classes, a collection of
general system components that are specializations of one of these
classes is delineated and it is shown that the specializations also
satisfy the security property. A sample distributed secure system
is presented along with an example of how the proposed mechanized
verification system can be used to verify such designs.