Abstract :
An algorithm that can be used to construct a definition of state equivalence that is meaningful in a security context is discussed. It the algorithm is followed, then at the completion of the algorithm, it has either been demonstrated that the system is secure in the sense that there can be no information flow from a higher level to a lower level, or an exploitation scenario for a covert channel has been demonstrated. The algorithm incrementally builds the definition of the equivalence relation in such a way that no effort is wasted. It allows for extensions to easily be made to the system without invalidating earlier work. Although it is generally thought that a noninterference analysis requires a verification environment, an informal analysis can still be performed without such an environment. This might result in slightly less confidence in the proofs, but it can save time. By doing this, one can analyze operations as they are being designed and errors can be corrected before they become entrenched in the system. When this point is reached, the security analysis will become a useful subtask of designing the system instead of an afterthought
