Eliminating Covert Flows with Minimum Typings

Abstract

A type system is given that eliminates two kinds of covert flows in an imperative programming language. The first kind arises from nontermination and the other from partial operations that can raise exceptions. The key idea is to limit the source of nontermination in the language to constructs with minimum typings, and to evaluate partial operations within expressions of "try" commands which also have minimum typings. A mutual progress theorem is proved that basically states that no two executions of a well-typed program can be distinguished on the basis of nontermination versus abnormal termination due to a partial operation. The proof uses a new style of programming language semantics which we call a natural transition semantics.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 1997
Accession Number
ADA494979

Entities

People

  • Dennis Volpano
  • Geoffrey B. Smith

Organizations

  • Naval Postgraduate School

Tags

DTIC Thesaurus Topics

  • Agreements
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Cybersecurity
  • Flow
  • Hypotheses
  • Information Processing
  • Judgment
  • Language
  • Procedural Programming Language
  • Programming Languages
  • Security
  • Semantics
  • Test And Evaluation
  • Transitions

Fields of Study

  • Computer science

Readers

  • Operations Research
  • Parallel and Distributed Computing.
  • Traumatic Brain Injury (TBI) and Cognitive Aging in the Guam and Border Populations Affected by Alzheimer's Disease and Tau-Associated Dementias.