Security Typings by Abstract Interpretation
Starting from a denotational semantics of imperative programs, the standard collecting semantics is defined as specifying the strongest program property. By successive Galois connection based abstractions, a type system that certifies secure information flows is designed as an abstract semantics approximating the collecting semantics of imperative programs. Security abstract analysis embodies the secure flow conditions of Denning’s lattice model (see ), giving rise to a type system which is similar to, but strictly more expressive than, the one proposed by Volpano et al. in . This shows that types and type systems for control flow analysis can be viewed as abstract interpretations.
KeywordsType System Secure Information Security Policy Semantic Property Abstract Interpretation
Unable to display preview. Download preview PDF.
- 1.D. E. Bell and L. J. LaPadula. Secure computer systems: Mathematical foundations. Technical report, Air Force Systems Command, 1973.Google Scholar
- 3.P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symp. on Principles of Programming Languages (POPL’ 77), pages 238–252. ACM Press, New York, 1977.CrossRefGoogle Scholar
- 5.D.E. Denning. Secure Information Flow in Computer Systems. PhD thesis, Purdue University, 1975.Google Scholar
- 8.R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, Proc. of the 24th Internat. Colloq. on Automata, Languages and Programming (ICALP’ 97), volume 1256 of Lecture Notes in Computer Science, pages 771–781. Springer-Verlag, Berlin, 1997.Google Scholar
- 9.B. W. Lampson. Dynamic protection structures. Proceedings of the AFIPS Fall Joint Computer Conference, pages 27–38, 1969.Google Scholar
- 10.D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(2,3):167–187, 1996.Google Scholar
- 11.G. Winskel. The Formal Semantics of Programming Languages: an Introduction. Foundations of Computing Series. The MIT Press, 1993.Google Scholar