Abstract
The External COMSEC Adaptor (ECA) is a device responsible for providing cryptographic protection of information based on rules that (possibly coarsely) define the sensitivity of that information. The ECA is trusted to satisfy a set of critical requirements that support data confidentiality in the network in which it is embedded. Ensuring that the ECA is worthy of this trust requires defining its critical requirements precisely and constructing a strong argument that its implementation satisfies these requirements. This paper describes a software engineering methodology that uses formal methods for specifying and verifying the most critical requirements of the ECA and uses testing and simulation for verifying the overall functional requirements of the ECA. The methodology integrates the formal specifications and proofs with structured software documentation to clarify the relationship between the refinement of ECA functionality and the argument that the ECA meets its critical requirements. This methodology was used successfully to build the ECA using the KG84A to satisfy its cryptographic requirements.