The National Computer Security Center requires that for a computer system to achieve an A1 evaluation, one must show that the Formal Top Level Specification (FTLS) of the system satisfies the requirements of the security model the system is intended to maintain. HDM, along with its accompanying specification language, SPECIAL, is a software tool designed to help software developers meet this requirement. A limitation of HDM is that it supports only one security model. This paper describes the software tool Muse, which makes HDM more flexible by permitting the user to define a security model in SPECIAL and then to prove that the FTLS maintains the model.

The enhancement consists of a parser, a linker, a formula generator, and a theorem prover--the latter two components being the most interesting. Of particular note is the discussion of the reliability of the theorem prover. Compared to the amount of work being done on building programs to verify other programs, there is very little work taking place on the issue of why we should trust one program simply on the word of another program. Any effort made to assure that the latter is correct could be, perhaps, better spent on the former. The authors address the issue head on, saying that software bugs are eliminated through repeated use of a stable system. Hence, the system’s proof checker will be required to remain stable, while heuristic proof-finding facilities may change over time.