On the Role of Formal Methods in Software Certification: An Experience Report

Abstract

This paper describes how formal methods were used to produce evidence in a certification, based on the Common Criteria, of a security-critical software system. The evidence included a top level specification (TLS) of the security-relevant software behavior, a formal statement of the required security properties, proofs that the specification satisfied the properties, and a demonstration that the source code, which had been annotated with preconditions and postconditions, was a refinement of the TLS. The paper also describes those aspects of our approach which were most effective and research that could significantly increase the effectiveness of formal methods in software certification.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2009
Accession Number
ADA511969

Entities

People

  • Constance L. Heitmeyer

Organizations

  • United States Naval Research Laboratory

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Automatic
  • Computer Programs
  • Computer Science
  • Computers
  • Data Processing
  • Information Systems
  • International Organizations
  • Language
  • Military Research
  • Natural Languages
  • Performance Tests
  • Security
  • Specifications
  • Standards
  • Theoretical Computer Science

Fields of Study

  • Computer science

Readers

  • Artificial Intelligence
  • Cybersecurity.
  • Database Systems and Applications