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. Bodei, C., Degano, P., Nielson, F., and Nielson, H. Static analysis for secrecy and non-interference in networks of processes. In Proc. of 6th Internat. Conference on Parallel Computing Technologies : (PaCT'01) (2001), vol. 2127 of Lecture Notes in Computer Science, Springer-Verlag, pp. 27--41.]]
4. Clark, D., Hankin, C., and Hunt, S. Information flow for algol-like languages. Computer Languages 28, 1 (2002), 3--28.]]
5. Cohen, E. S. Information transmission in computational systems. ACM SIGOPS Operating System Review 11, 5 (1977), 133--139.]]
6. Cousot, P. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci. 277, 1--2 (2002), 47,103.]]
7. Cousot, P., and Cousot, R. 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) (1977), ACM Press, New York, pp. 238--252.]]
8. Cousot, P., and Cousot, R. Constructive versions of Tarski's fixed point theorems. Pacific J. Math. 82, 1 (1979), 43--57.]]
9. Cousot, P., and Cousot, R. Systematic design of program analysis frameworks. In Conference Record of the 6th ACM Symp. on Principles of Programming Languages ( POPL '79) (1979), ACM Press, New York, pp. 269--282.]]
10. Cousot, P., and Cousot, R. Inductive definitions, semantics and abstract interpretation. In Conference Record of the 19th ACM Symp. on Principles of Programming Languages (POPL '92) (1992), ACM Press, New York, pp. 83--94.]]
11. Davey, B. A., and Priestley, H. A. Introduction to Lattices and Order. Cambridge University Press, Cambridge, U.K., 1990.]]
12. Denning, D. E. Secure Information Flow in Computer Systems. PhD thesis, Purdue University, 1975.]]
13. Denning, D. E. A lattice model of secure information flow. Communications of the ACM 19, 5 (1976), 236--242.]]
14. Denning, D. E., and Denning, P. Certification of programs for secure information flow. Communications of the ACM 20, 7 (1977), 504--513.]]
15. Di Pierro, A., Hankin, C., and Wiklicky, H. Approximate non-interference. In Proc. of the IEEE Computer Security Foundations Workshop (2002), IEEE Computer Society Press, pp. 1--17.]]
16. Filé, G., Giacobazzi, R., and Ranzato, F. A unifying view of abstract domain design. ACM Comput. Surv. 28, 2 (1996), 333--336.]]
17. Giacobazzi, R., and Quintarelli, E. Incompleteness, counterexamples and refinements in abstract model-checking. In Proc. of The 8th Internat. Static Analysis Symposium, (SAS'01) (2001), P. Cousot, Ed., vol. 2126 of Lecture Notes in Computer Science, Springer-Verlag, pp. 356--373.]]
18. Giacobazzi, R., and Ranzato, F. Refining and compressing abstract domains. In Proc. of the 24th Internat. Colloq. on Automata, Languages and Programming (ICALP '97) (1997), P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, Eds., vol. 1256 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 771--781.]]
19. Giacobazzi, R., and Ranzato, F. Optimal domains for disjunctive abstract interpretation. Sci. Comput. Program. 32, 1-3 (1998), 177--210.]]
20. Giacobazzi, R., Ranzato, F., and Scozzari, F. Making abstract interpretations complete. J. of the ACM. 47, 2 (2000), 361--416.]]
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. Joshi, R., and Leino, K. R. M. A semantic approach to secure information flow. Sci. Comput. Program. 37 (2000), 113--138.]]
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. Laud, P. Semantics and program analysis of computationally secure information flow. In In Programming Languages and Systems, 10th European Symposium On Programming, (ESOP'01) (2001), vol. 2028 of Lecture Notes in Computer Science, Springer-Verlag, pp. 77--91.]]
26. Lowe, G. Quantifying information flow. In Proc. of the IEEE Computer Security Foundations Workshop (2002), IEEE Computer Society Press, pp. 18--31.]]
27. Monniaux, D. An abstract analysis of the probabilistic termination programs. In Proc. of The 8th Internat. Static Analysis Symposium, (SAS'01) (2001), vol. 2126 of Lecture Notes in Computer Science, Springer-Verlag, pp. 111--127.]]
28. Ørbæk, P. Can you trust your data? In Proc. of the 6th Internat. Joint Conf. CAAP/FASE, Theory and Practice of Software Devolpment (TAPSOFT '95) (1995), P. Mosses, M. Nielsen, and M. Schwartzbach, Eds., vol. 915 of Lecture Notes in Computer Science, Springer-Verlag, pp. 575--589.]]
29. Ranzato, F., and Tapparo, F. Making abstract model checking strongly preserving. In Proc. of The 9th Internat. Static Analysis Symposium, (SAS'02) (2002), M. Hermenegildo and G. Puebla, Eds., vol. 2477 of Lecture Notes in Computer Science, Springer-Verlag, pp. 411--427.]]
30. Sabelfeld, A., and Myers, A. Language-based information-flow security. IEEE J. on selected ares in communications 21, 1 (2003), 5--19.]]
31. Sabelfeld, A., and Sands, D. A PER model of secure information flow in sequential programs. Higher-Order and Symbolic Computation 14, 1 (2001), 59--91.]]
32. Schneider, F., Morrisett, G., and Harper, R. A language-based approach to security. In In Informatics: 10 Years Back, 10 Years Ahead (2000), vol. 2000 of Lecture Notes in Computer Science, Springer-Verlag, pp. 86--101.]]
33. Skalka, C., and Smith, S. Static enforcement of security with types. In Proc. Internat. Conference on Functional Programming (ICFP'00) (2000), ACM Press, New York, pp. 254--267.]]
34. Volpano, D. Safety versus secrecy. In Proc. of The 6th Internat. Static Analysis Symposium (SAS'99) (1999), A. Cortesi and G. Filé, Eds., vol. 1694 of Lecture Notes in Computer Science, Springer-Verlag, pp. 303--311.]]
35. Volpano, D., and Smith, G. Verifying secrets and relative secrecy. In Conference Record of the 27th ACM Symp. on Principles of Programming Languages (POPL '00) (2000), ACM Press, New York, pp. 268--276.]]
36. Volpano, D., Smith, G., and Irvine, C. A sound type system for secure flow analysis. J. of Computer Security 4, 2,3 (1996), 167--187.]]
37. Weiser, M. Program slicing. IEEE Transactions on software engineering 10, 4 (1984), 352--357.]]
38. Winskel, G. The formal semantics of programming languages: an introduction. MIT Press, 1993.]]
39. Zanotti, M. Security typings by abstract interpretation. In Proc. of The 9th Internat. Static Analysis Symposium, (SAS'02) (2002), M. Hermenegildo and H. Puebla, Eds., vol. 2477 of Lecture Notes in Computer Science, Springer-Verlag, pp. 360--375.]]
40. Zdancewic, S., and Myers, A. C. Robust declassification. In Proc. of the IEEE Computer Security Foundations Workshop (2001), IEEE Computer Society Press, pp. 15--23.]]

Index Terms

• Security and privacy

• Social and professional topics

  • Computing / technology policy

    • Computer crime

• Software and its engineering

  • Software notations and tools

    • Formal language definitions

      • Semantics

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program analysis

    • Program semantics