Secure Software Verification Tools
Abstract
This phase I effort demonstrated the viability of automated security verification at the implementation level. Source code verification capability would represent a technology advancement that would greatly aid the developement of secure software systems. Currently, source code verification is a tedious process consisting of manual code-to-design correspondence checking. If an implementer deviates from the secure design, whether intentionally or negligently, the discrepancy can be detected through manual analysis. This analysis is only as valid as the skill and expertise of the individual conducting the correspondence check. Furthermore, manual analysis is typically performed only on selected code due to its high cost. Therefore, a large secure software system remains vulnerable to insertion of surreptitious code throughout the implementation phase. This problem can be alleviated by an automated extension of the formal verification process that can operate directly on the source code. Phase I research focused on the evaluation of two different approaches to the automation of source code: (1) Source-to-Special. STOS is an automated translation of source to Special that will function as a front-end for the Hierarchical Development Methodology (HDM) verification environment; (2) Source-to-Formulas. STOF is an automated translation of source directly to formulas. This innovative concept serves to streamline the verification process by eliminating the need for a specification language. COMPUSEC concludes that STOF is the approach of choice; representing innovative technical progress in field of softwave verification.
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 10, 1987
- Accession Number
- ADA189731