Analysis of the Hardware Verification of the Honeywell SCOMP

An analysis of the verification approach used for the SCOMP hardware is presented herein. Although the SCOMP approach is informal it is extensive and thorough. In general, it provides sufficient evidence to conclude that the SCOMP hardware forms a sound basis for the development of a security kernel. However, the SCOMP approach presents a number of problems which are common to most informal verification approaches. These problems include: (1) incomplete formal top-level specification of the hardware functions that are visible at the TCB interface, and (2) incomplete coverage of design (and implementation) analysis and testing. The existence of verification problems does not imply that design/implementation flaws are left undiscovered and uncorrected in the SCOMP system. However, it does require that complete confidence in the hardware design (and implementation) be gained in alternate ways; e.g., by careful review of all possible implications of the verification omissions, and, possibly, by penetration analysis. All concerns raised along these lines with the system designers were answered in a satisfactory way.