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. We also give an algorithm for inferring and simplifying principal types, which document the security requirements of programs.
CITATION STYLE
Volpano, D., & Smith, G. (1997). A type-based approach to program security. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1214, pp. 607–621). Springer Verlag. https://doi.org/10.1007/bfb0030629
Mendeley helps you to discover research relevant for your work.