A Software Validation Technique for Certification: The Methodology

Certification is the approval, by some appropriate authority, that a system meets some functional criteria. In the past, critical software systems, such as security controls have not been certifiable because of the unavailability of a formal validation technique. This paper establishes such a formal methodology for validating the correctness of a software system. The methodology is both rigorous and general and is suitable for certifying the effectiveness of software security controls that are to be used in an open environment. A companion volume will develop a detailed example based on a security kernel for a PDP-1145.