A Type-Based Approach to Program Security

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.

• Type: Conference
• Year: 1997
• Where: TAPSOFT
• Authors: Dennis M. Volpano, Geoffrey Smith
• Keywords: Noninterference Security Property, Security, Software Engineering, TAPSOFT 1997, Various Security Levels