Structuring Systems for Formal Verification

High levels of assurance for a secure system are obtained, in part, by the description of its trusted computing base in terms of a formal top-level specification. Nevertheless, the use of a single-level specification can result in an inability to link the behavior of the trusted computing base with the security policy of the system as a whole. This paper discusses some of the resulting problems and preaents an approach to structuring sys terns that will support their verification. Such structuring is shown to be effective in bridging the gap between the trusted computing base itself and the system seen as a whole.