A Technique for Proving Specifications are Multilevel Secure

Abstract
This document describe a technique for verifying that a design for an operating system or subsystem expressed in terms of a formal specification is consistent with a particular model of multilevel security. The technique to be described is mathematically rigorous and, if applied properly, gives assurance that the given design is multilevel secure by this particular model. The technique is supported by a collection of automated tools. These tools assist the user in the performance of a large amount of detailed routine tasks that must be performed to apply the technique. In general, contemporary formal verification techniques such as the one described here involve a great deal of repetitive, detailed, uninteresting steps that are necessary to maintain the rigor of the proof process. The proof are usually larger and more complex than the system being proved. Keywords: Critical technology.

This publication has 0 references indexed in Scilit: