Coding for a Believable Specification to Implementation Mapping

Abstract: One criterion for "Beyond Al" certification according to the DoD Trusted Computer Systems Evaluation Criteria will be code-level verification. We argue that, while verification at the actual code level may be infeasible for large secure systems, it is possible to push the verification to a low level of abstraction and then map the specification in an intuitive manner to the source code. Providing a suitable mapping requires adhering to a strict discipline on both the specification and code sides. We discuss the issues involved in this problem, particularizing the discussion to a mapping from Gypsy specifications to C code.