A Type Based Approach to Program Security

Abstract

This paper presents a type system which guarantees that well typed programs in a procedural programming language satisfy a noninterference security property With all program inputs and outputs classified at various security levels the property basically states that a program output classified at some level, can never change as a result of modifying only inputs classified at higher levels. Intuitively this means the program does not "leak" sensitive data. The property is similar to a notion introduced years ago by Goguen and Meseguer to model security in multi level computer systems [7]. We also give an algorithm for inferring and simplifying principal types, which document the security requirements of programs.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 01, 1997
Accession Number
ADA487401

Entities

People

  • Dennis Volpano
  • Geoffrey B. Smith

Organizations

  • Naval Postgraduate School

Tags

DTIC Thesaurus Topics

  • Algorithms
  • Computer Programming
  • Computer Science
  • Computers
  • Control Systems
  • Cybersecurity
  • Flow
  • Guarantees
  • Inequalities
  • Language
  • Procedural Programming
  • Procedural Programming Language
  • Programming Languages
  • Security
  • Security Protocols
  • Semantics

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Computational Modeling and Simulation
  • Cybersecurity.

Technology Areas

  • AI & ML
  • AI & ML - Neural Networks