Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Computer Science Logic

CSL 2004: Computer Science Logic pp 280–294Cite as

Proving Abstract Non-interference

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3210))

Abstract

In this paper we introduce a compositional proof-system for certifying abstract non-interference in programming languages. Certifying abstract non-interference means proving that no unauthorized flow of information is observable by the attacker from confidential to public data. The properties of the computation that an attacker may observe are specified as an abstract domain. Assertions specify the secrecy of a program relatively to the given attacker and the proof-system specifies how these assertions can be composed in a syntax-directed a la Hoare deduction of secrecy. We prove that the proof-system is sound relatively to the standard semantics of an imperative programming language. This provides a sound proof-system for both certifying secrecy in language-based security and deriving attackers which do not violate secrecy inductively on program’s syntax.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andrews, G.R., Reitman, R.P.: An axiomatic approach to information flow in programs. ACM Trans. Program. Lang. Syst. 2(1), 56–76 (1980)

    Article  Google Scholar 

  2. Appel, A.: Foundational proof-carrying code. In: Proc. of the 16th IEEE Symp. on Logic in Computer Science LICS 2001, pp. 247–258. IEEE Computer Society Press, Los Alamitos (2001)

    Google Scholar 

  3. Apt, K., Olderog, E.-R.: Verification of sequential and concurrent programs. Springer, Berlin (1997)

    Book  Google Scholar 

  4. Bell, D.E., Burke, E.: A software validation technique for certification: The methodology. Technical Report MTR-2932, MITRE Corp. Badford, MA (1974)

    Google Scholar 

  5. Bell, D.E., LaPadula, L.J.: Secure computer systems: Mathematical foundations and model. Technical Report M74-244, MITRE Corp. Badford, MA (1973)

    Google Scholar 

  6. Clark, D., Hankin, C., Hunt, S.: Information flow for algol-like languages. Computer Languages 28(1), 3–28 (2002)

    MATH  Google Scholar 

  7. Cohen, E.S.: Information transmission in computational systems. ACM SIGOPS Operating System Review 11(5), 133–139 (1977)

    Article  Google Scholar 

  8. Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci. 277(1-2), 47, 103 (2002)

    Article  MathSciNet  Google Scholar 

  9. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of Conf. Record of the 4th ACM Symp. on Principles of Programming Languages (POPL 1977), pp. 238–252. ACM Press, New York (1977)

    Google Scholar 

  10. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. Of Conf. Record of the 6th ACM Symp. on Principles of Programming Languages (POPL 1979), pp. 269–282. ACM Press, New York (1979)

    Google Scholar 

  11. Cousot, P., Cousot, R.: Inductive definitions, semantics and abstract interpretation. In: Proc. of Conf. Record of the 19th ACM Symp. on Principles of Programming Languages (POPL 1992), pp. 83–94. ACM Press, New York (1992)

    Google Scholar 

  12. Darvas, A., Hähnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Gorrieri, R. (ed.) Workshop on Issues in the Theory of Security, WITS. IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS (2003)

    Google Scholar 

  13. Denning, D.E.: A lattice model of secure information flow. Communications of the ACM 19(5), 236–242 (1976)

    Article  MathSciNet  Google Scholar 

  14. Denning, D.E., Denning, P.: Certification of programs for secure information flow. Communications of the ACM 20(7), 504–513 (1977)

    Article  Google Scholar 

  15. Flanagan, C., Qadeer, S.: Pedicate abstraction for software verification. In: Proc. of Conf. Record of the 29th ACM Symp. on Principles of Programming Languages (POPL 2002), pp. 191–202. ACM Press, New York (2002)

    Google Scholar 

  16. Giacobazzi, R., Mastroeni, I.: Abstract non-interference: Parameterizing non-interference by abstract interpretation. In: Proc. of the 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), pp. 186–197. ACM Press, New York (2004)

    Google Scholar 

  17. Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples, and refinements in abstract model-checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 356–373. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  18. Giacobazzi, R., Ranzato, F.: Optimal domains for disjunctive abstract interpretation. Sci. Comput. Program 32(1-3), 177–210 (1998)

    Article  MathSciNet  Google Scholar 

  19. Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proc. IEEE Symp. on Security and Privacy, pp. 11–20. IEEE Computer Society Press, Los Alamitos (1982)

    Google Scholar 

  20. Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: Proc. IEEE Symp. On Security and Privacy, pp. 75–86. IEEE Computer Society Press, Los Alamitos (1984)

    Google Scholar 

  21. Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  22. Joshi, R., Leino, K.R.M.: A semantic approach to secure information flow. Science of Computer Programming 37, 113–138 (2000)

    Article  MathSciNet  Google Scholar 

  23. Laud, P.: Semantics and program analysis of computationally secure information flow. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 77–91. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  24. Necula, G.: Proof-carrying code. In: Proc. of Conf. Record of the 24th ACM Symp. on Principles of Programming Languages (POPL 1997), pp. 106–119. ACM Press, New York (1997)

    Google Scholar 

  25. Ranzato, F., Tapparo, F.: Making abstract model checking strongly preserving. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 411–427. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  26. Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. on selected ares in communications 21(1), 5–19 (2003)

    Article  Google Scholar 

  27. Sabelfeld, A., Sands, D.: A PER model of secure information flow in sequential programs. Higher-Order and Symbolic Computation 14(1), 59–91 (2001)

    Article  Google Scholar 

  28. Skalka, C., Smith, S.: Static enforcement of security with types. In: ICFP 2000, pp. 254–267. ACM Press, New York (2000)

    Google Scholar 

  29. Volpano, D.: Safety versus secrecy. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 303–311. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  30. Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Journal of Computer Security 4(2,3), 167–187 (1996)

    Article  Google Scholar 

  31. Winskel, G.: The formal semantics of programming languages: an introduction. MIT Press, Cambridge (1993)

    Book  Google Scholar 

  32. Zanotti, M.: Security typings by abstract interpretation. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 360–375. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università di Verona, Strada Le Grazie 15, I-37134, Verona, Italy

    Roberto Giacobazzi & Isabella Mastroeni

Authors
  1. Roberto Giacobazzi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Isabella Mastroeni
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Wroclaw University, Poland

    Jerzy Marcinkowski

  2. Polish Academy of Sciences, Institute of Computer Science, Poland

    Andrzej Tarlecki

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Giacobazzi, R., Mastroeni, I. (2004). Proving Abstract Non-interference. In: Marcinkowski, J., Tarlecki, A. (eds) Computer Science Logic. CSL 2004. Lecture Notes in Computer Science, vol 3210. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30124-0_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-30124-0_23

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-23024-3

  • Online ISBN: 978-3-540-30124-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation