Increasing Assurance with Literate Programming Techniques

The assurance argument that a trusted system satisfies its information security requirements must be convincing, because the argument supports the accreditation decision to allow the computer to process classified information in an operational environment. Assurance is achieved through understanding, but some evidence that supports the assurance argument can be difficult to understand. This paper describes a novel application of a technique, called literate programming [11], that significantly improves the readability of the assurance argument while maintaining its consistency with formal specifications that are input to specification and verification systems. We describe an application of this technique to a simple example and discuss the lessons learned from this effort.
Prepared in collaboration with Secure Computing Corp., Roseville, MN.