Security Typings by Abstract Interpretation

  • Mirko Zanotti
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2477)


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 [6]), giving rise to a type system which is similar to, but strictly more expressive than, the one proposed by Volpano et al. in [10]. This shows that types and type systems for control flow analysis can be viewed as abstract interpretations.


Type System Secure Information Security Policy Semantic Property Abstract Interpretation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    D. E. Bell and L. J. LaPadula. Secure computer systems: Mathematical foundations. Technical report, Air Force Systems Command, 1973.Google Scholar
  2. 2.
    P. Cousot. Types as abstract interpretations. In Conference Record of the 24th ACM Symp. on Principles of Programming Languages (POPL’97), pages 316–331. ACM Press, New York, U.S.A., 1997.CrossRefGoogle Scholar
  3. 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
  4. 4.
    P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conference Record of the 6th ACM Symp. on Principles of Programming Languages (POPL’ 79), pages 269–282. ACM Press, New York, 1979.CrossRefGoogle Scholar
  5. 5.
    D.E. Denning. Secure Information Flow in Computer Systems. PhD thesis, Purdue University, 1975.Google Scholar
  6. 6.
    D. E. Denning. A lattice model of secure information flow. Communications of the ACM, 19(5):236–242, 1976.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    D.E. Denning and P. Denning. Certification of programs for secure information flow. Communications of the ACM, 20(7):504–513, 1977.zbMATHCrossRefGoogle Scholar
  8. 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. 9.
    B. W. Lampson. Dynamic protection structures. Proceedings of the AFIPS Fall Joint Computer Conference, pages 27–38, 1969.Google Scholar
  10. 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. 11.
    G. Winskel. The Formal Semantics of Programming Languages: an Introduction. Foundations of Computing Series. The MIT Press, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Mirko Zanotti
    • 1
    • 2
  1. 1.Dipartimento di InformaticaUniversitá di VeronaVeronaItaly
  2. 2.LIX — Laboratoire d’InformatiqueÈcole PolytechniquePalaiseauFrance

Personalised recommendations