Role of Formal Methods in High-Grade InfoSec Evaluations

摘要

With the increasing use of computer systems in governmental, commercial and industrial equipment, we must be sure that these systems remain secure. The Common Criteria is an internationally recognised criteria for evaluating IT products with security functionality. To achieve a high level of assurance from the Common Criteria, formal methods should be applied in the development process. This report concentrates on formal methods support for development and evaluation of security-critical systems in the Common Criteria. In particular, the Defence Signal Directorate (DSD) is charged with the oversight of the security evaluations program in Australia. The report attempts to indicate what DSD should know about formal methods for the high-grade evaluations, and where they can find out more as desired.