Proving Noninterference and Functional Correctness Using Traces

Abstract

The trace method of software specification is extended to provide a natural semantics for a procedural programming language. This extension provides a method for proving program correctness that permits a direct proof of program Noninterference without having to produce an intermediate finite state machine and unwinding conditions. This approach provides a uniform framework for reasoning about abstract software system specifications and their implementations. It also allows us to prove security at an abstract level so that changes to programs that do not affect functional behavior will not affect the security proof.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1992
Accession Number
ADA463011

Entities

People

  • John A. McLean

Organizations

  • United States Naval Research Laboratory

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Abstracts
  • Clearances
  • Computer Programming
  • Construction
  • Language
  • Lists (Data Structures)
  • Load Monitoring
  • Military Research
  • Procedural Programming
  • Procedural Programming Language
  • Programming Languages
  • Security
  • Semantics
  • Sequences
  • Software Development
  • Specifications
  • Standards

Fields of Study

  • Computer science
  • Engineering

Readers

  • Mathematical Modeling and Probability Theory.
  • Software Engineering.