A Type-Based Approach to Program Security
Loading...
Authors
Volpano, Dennis
Smith, Geoffrey
Subjects
Advisors
Date of Issue
1997-04
Date
April 1997.
Publisher
Language
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 secu- rity in multi-level computer systems [7]. We also give an algorithm for inferring and simplifying principal types, which document the security requirements of programs.
Type
Description
The article of record as published may be found at http://dx.doi.org/
Series/Report No
Department
Computer Science (CS)
Organization
Identifiers
NPS Report Number
Sponsors
Funder
Format
Citation
Proc. 7th Int'l Joint Conference on the Theory and Practice of Software Development, LNCS 1214, pp. 607-621, Lille France, April 1997.
Distribution Statement
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.