Third European Symposium on Research in Computer Security (ESORICS 94)
Security through Type Analysis
C. O'Halloran, C. T. Sennett
Keywords : Types, formal techniques, secure computer systems, security evaluation
Abstract : The objective of the work reported in this paper is to develop very low cost techniques for demonstrating that the trusted software for a secure system has the security properties claimed for it. The approach also supports integrity properties. The approach is based on type checking, which ensures that operations cannot be called with arguments they should not handle. This paper presents an informal technical description of the work with respect to a particular case study. An outline of the type checking algorithm is given in an appendix.
(Pages 75-89)