Abstract non-interference: parameterizing non-interference by abstract interpretation

ABSTRACT

In this paper we generalize the notion of non-interference making it parametric relatively to what an attacker can analyze about the input/output information flow. The idea is to consider attackers as data-flow analyzers, whose task is to reveal properties of confidential resources by analyzing public ones. This means that no unauthorized flow of information is possible from confidential to public data, relatively to the degree of precision of an attacker. We prove that this notion can be fully specified in standard abstract interpretation framework, making the degree of security of a program a property of its semantics. This provides a comprehensive account of non-interference features for language-based security. We introduce systematic methods for extracting attackers from programs, providing domain-theoretic characterizations of the most precise attackers which cannot violate the security of a given program. These methods allow us both to compare attackers and program secrecy by comparing the corresponding abstractions in the lattice of abstract interpretations, and to design automatic program certification tools for language-based security by abstract interpretation.

REFERENCES

• 1: Bell, D. E., and Burke, E. A software validation technique for certification: The methodology. Tech. Rep. MTR-2932, MITRE Corp., Badford, MA, 1974.
• 2: Bell, D. E., and LaPadula, L. J. Secure computer systems: Mathematical foundations and model. Tech. Rep. M74-244, MITRE Corp., Badford, MA, 1973.
• 3: Chiara Bodei , Pierpaolo Degano , Flemming Nielson , Hanne Riis Nielson, Static Analysis for Secrecy and Non-interference in Networks of Processes, Proceedings of the 6th International Conference on Parallel Computing Technologies, p.27-41, September 03-07, 2001
• 4: Clark, D., Hankin, C., and Hunt, S. Information flow for algol-like languages. Computer Languages 28, 1 (2002), 3--28.
• 5: Ellis Choen, Information transmission in computational systems, Proceedings of the sixth ACM symposium on Operating systems principles, p.133-139, November 16-18, 1977, West Lafayette, Indiana, United States
• 6: Patrick Cousot, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Theoretical Computer Science, v.277 n.1-2, p.47-103, April 28, 2002 [doi>10.1016/S0304-3975(00)00313-3 ]
• 7: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 8: Cousot, P., and Cousot, R. Constructive versions of Tarski's fixed point theorems. Pacific J. Math. 82, 1 (1979), 43--57.
• 9: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 10: Patrick Cousot , Radhia Cousot, Inductive definitions, semantics and abstract interpretations, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.83-94, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143184]
• 11: Davey, B. A., and Priestley, H. A. Introduction to Lattices and Order. Cambridge University Press, Cambridge, U.K., 1990.
• 12: Dorothy Elizabeth Robling Denning, Secure information flow in computer systems., 1975
• 13: Dorothy E. Denning, A lattice model of secure information flow, Communications of the ACM, v.19 n.5, p.236-243, May 1976 [doi>10.1145/360051.360056]
• 14: Dorothy E. Denning , Peter J. Denning, Certification of programs for secure information flow, Communications of the ACM, v.20 n.7, p.504-513, July 1977 [doi>10.1145/359636.359712]
• 15: Alessandra Di Pierro , Chris Hankin , Herbert Wiklicky, Approximate Non-Interference, Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW'02), p.3, June 24-26, 2002
• 16: Gilberto Filé , Roberto Giacobazzi , Francesco Ranzato, A unifying view of abstract domain design, ACM Computing Surveys (CSUR), v.28 n.2, p.333-336, June 1996 [doi>10.1145/234528.234742]
• 17: Roberto Giacobazzi , Elisa Quintarelli, Incompleteness, Counterexamples, and Refinements in Abstract Model-Checking, Proceedings of the 8th International Symposium on Static Analysis, p.356-373, July 16-18, 2001
• 18: Roberto Giacobazzi , Francesco Ranzato, Refining and Compressing Abstract Domains, Proceedings of the 24th International Colloquium on Automata, Languages and Programming, p.771-781, July 07-11, 1997
• 19: Roberto Giacobazzi , Francesco Ranzato, Optimal domains for disjunctive abstract interpretation, Science of Computer Programming, v.32 n.1-3, p.177-210, Sept. 1998 [doi>10.1016/S0167-6423(97)00034-8 ]
• 20: Roberto Giacobazzi , Francesco Ranzato , Francesca Scozzari, Making abstract interpretations complete, Journal of the ACM (JACM), v.47 n.2, p.361-416, March 2000 [doi>10.1145/333979.333989]
• 21: Goguen, J. A., and Meseguer, J. Security policies and security models. In Proc. IEEE Symp. on Security and Privacy (1982), IEEE Computer Society Press, pp. 11--20.
• 22: Goguen, J. A., and Meseguer, J. Unwinding and inference control. In Proc. IEEE Symp. on Security and Privacy (1984), IEEE Computer Society Press, pp. 75--86.
• 23: Rajeev Joshi , K. Rustan M. Leino, A semantic approach to secure information flow, Science of Computer Programming, v.37 n.1-3, p.113-138, May 2000 [doi>10.1016/S0167-6423(99)00024-6 ]
• 24: Landauer, J., and Redmond, T. A lattice of information. In Proc. of the IEEE Computer Security Foundations Workshop (1993), IEEE Computer Society Press, pp. 65--70.
• 25: Peeter Laud, Semantics and Program Analysis of Computationally Secure Information Flow, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.77-91, April 02-06, 2001
• 26: Gavin Lowe, Quantifying Information Flow, Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW'02), p.18, June 24-26, 2002
• 27: David Monniaux, An Abstract Analysis of the Probabilistic Termination of Programs, Proceedings of the 8th International Symposium on Static Analysis, p.111-126, July 16-18, 2001
• 28: Peter Ørbæk, Can you Trust your Data?, Proceedings of the 6th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.575-589, May 22-26, 1995
• 29: Francesco Ranzato , Francesco Tapparo, Making Abstract Model Checking Strongly Preserving, Proceedings of the 9th International Symposium on Static Analysis, p.411-427, September 17-20, 2002
• 30: Sabelfeld, A., and Myers, A. Language-based information-flow security. IEEE J. on selected ares in communications 21, 1 (2003), 5--19.
• 31: Andrei Sabelfeld , David Sands, A Per Model of Secure Information Flow in Sequential Programs, Higher-Order and Symbolic Computation, v.14 n.1, p.59-91, March 2001 [doi>10.1023/A:1011553200337 ]
• 32: Fred B. Schneider , J. Gregory Morrisett , Robert Harper, A Language-Based Approach to Security, Informatics - 10 Years Back. 10 Years Ahead., p.86-101, January 2001
• 33: Christian Skalka , Scott Smith, Static enforcement of security with types, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.34-45, September 2000
• 34: Dennis M. Volpano, Safety versus Secrecy, Proceedings of the 6th International Symposium on Static Analysis, p.303-311, September 22-24, 1999
• 35: Dennis Volpano , Geoffrey Smith, Verifying secrets and relative secrecy, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-276, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325729]
• 36: Dennis Volpano , Cynthia Irvine , Geoffrey Smith, A sound type system for secure flow analysis, Journal of Computer Security, v.4 n.2-3, p.167-187, Jan. 1996
• 37: Weiser, M. Program slicing. IEEE Transactions on software engineering 10, 4 (1984), 352--357.
• 38: Glynn Winskel, The formal semantics of programming languages: an introduction, MIT Press, Cambridge, MA, 1993
• 39: Mirko Zanotti, Security Typings by Abstract Interpretation, Proceedings of the 9th International Symposium on Static Analysis, p.360-375, September 17-20, 2002
• 40: Steve Zdancewic , Andrew C. Myers, Robust Declassification, Proceedings of the 14th IEEE Workshop on Computer Security Foundations, p.5, June 11-13, 2001

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)

General Terms:
Languages, Security

Keywords:
abstract domains, abstract interpretation, language-based security, non-interference