Skip Navigation



Journal of Logic and Computation Advance Access published online on September 17, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp053
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Giacobazzi, R.
Right arrow Articles by Mastroeni, I.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

A Proof System for Abstract Non-interference

Roberto Giacobazzi and Isabella Mastroeni

Dipartimento di Informatica, Università di Verona, Strada le Grazie, 15 37134 Verona, Italy.
E-mail: roberto.giacobazzi{at}univr.it; isabella.mastroeni{at}univr.it

Received 20 May 2009.

In this article, we provide an inductive proof system for a notion of abstract non-interference (ANI) which fits in every field of computer science where we are interested in observing how different programs data interfere with each other. The idea is to abstract from language-based security and consider generically data as distinguished between internal (that has to be protected by the program) and observable. In this more general context, we derive a proof system that allows us -to characterize ANI properties inductively on the syntactic structure of programs. We finally show how this framework can be instantiated to language-based security.

Keywords: Abstract interpretation; abstract domains; non-interference; closure operators; semantics; static program analysis; logic of programs; verification



References

  1. Andrews GR, Reitman RP. An axiomatic approach to information flow in programs. ACM Transactions Programming Languages Systems (1980) 2:56–76.[CrossRef]
  2. Appel A. Foundational proof-carrying code. (2001) California: Los Alamitos. 247–258. In Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS’01).
  3. Banerjee A, Giacobazzi R, Mastroeni I. What you lose is what you leak: information leakage in declassifivation policies. (2007) Amsterdam. Elsevier. In Proceedings of the 23th International Symposium on Mathematical Foundations of Programming Semantics (MFPS’07), Vol. 1514 of Electronic Notes in Theoretical Computer Science.
  4. Clark D, Hankin C, Hunt S. Information flow for algol-like languages. Computer Languages (2002) 28:3–28.
  5. Cohen ES. Information transmission in computational systems. ACM SIGOPS Operating System Review (1977) 11:133–139.[CrossRef]
  6. Cohen ES. Information transmission in sequential programs. In: Foundations of Secure Computation—, ed. (1978) Academic Press. 297–335.
  7. Cousot P. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science (2002) 277:47–103.[CrossRef][Web of Science]
  8. Cousot P, Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. (1977) ACM Press. 238–252. In Proceedings of Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL’77).
  9. Cousot P, Cousot R. Systematic design of program analysis frameworks. (1979) ACM Press. 269–282. In Proceedings of Conference Record of the 6th ACM Symposium on Principles of Programming Languages (POPL’79).
  10. Darvas A, Hähnle R, Sands D. A theorem proving approach to analysis of secure information flow. Hutter D, Ullmann M, eds. (2005) 3450. Springer. 193–209. In Security in Pervasive Computing: Second International Conference (SPC 2005).
  11. Flanagan C, Qadeer S. Pedicate abstraction for software verification. (2002) ACM Press. 191–202. In Proceedings of Conference Record of the 29th ACM Symposium on Principles of Programming Languages (POPL’02).
  12. Giacobazzi R, Mastroeni I. Abstract non-interference: parameterizing non-interference by abstract interpretation. (2004) ACM-Press. 186–197. In Proceedings of the 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’04).
  13. Giacobazzi R, Mastroeni I. Proving abstract non-interference. Tarlecki A, Marcinkowski J, eds. (2004) 3210. Springer. 280–294. In Annual Conference of the European Association for Computer Science Logic (CSL’04).
  14. Giacobazzi R, Mastroeni I. Adjoining declassification and attack models by abstract interpretation. Sagiv S, ed. (2005) Springer. 295–310. In Proceedings of the European Symposium on Programming (ESOP’05), Vol. 3444 of Lecture Notes in Computer Science.
  15. Giacobazzi R, Mastroeni I. Abstract non-interference. In: Technical report (2008) Department of Computer Science, University of Verona.
  16. Giacobazzi R, Mastroeni I. Adjoining classified and unclassified information by abstract interpretation. Journal of Computer Security (2009) to appear.
  17. Goguen JA, Meseguer J. Security policies and security models. (1982) IEEE Computer Society Press. 11–20. In Proceedings of IEEE Symposium on Security and Privacy.
  18. Joshi R, Leino KRM. A semantic approach to secure information flow. Science of Computer Programming (2000) 37:113–138.[CrossRef][Web of Science]
  19. Laud P. Semantics and program analysis of computationally secure information flow. Sands D, ed. (2001) Springer. 77–91. In Programming Languages and Systems, 10th European Symposium On Programming (ESOP’01), Vol. 2028 of Lecture Notes in Computer Science.
  20. Mastroeni I. On the rôle of abstract non-interference in language-based security. Yi K, ed. (2005) Springer. 418–433. In Third Asian Symposium on Programming Languages and Systems (APLAS’05), Vol. 3780 of Lecture Notes in Computer Science.
  21. Necula G. Proof-carrying code. (1997) ACM Press. 106–119. In Proceedings of Conference Record of the 24th ACM Symposium on Principles of Programming Languages (POPL’97).
  22. Ranzato F, Tapparo F. Strong preservation as completeness in abstract interpretation. Schmidt D, ed. (2004) Springer. 18–32. In Proceedings of the 13th European Symposium on Programming (ESOP’04), Vol. 2986 of Lecture Notes in Computer Science.
  23. Sabelfeld A, Myers AC. Language-based information-flow security. IEEE Journal on Selected Areas in Communications (2003) 21:5–19.[CrossRef][Web of Science]
  24. Sabelfeld A, Sands D. A PER model of secure information flow in sequential programs. Higher-Order and Symbolic Computation (2001) 14:59–91.[CrossRef]
  25. Skalka C, Smith S. Static enforcement of security with types. (2000) ACM Press. 254–267. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming(ICFP’00).
  26. Smith G, Volpano D. Secure information flow in a multi-threaded imperative language. (1998) ACM Press. 355–364. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’98).
  27. Volpano D, Smith G, Irvine C. A sound type system for secure flow analysis. Journal of Computer Security (1996) 4:167–187.
  28. Winskel G. The Formal Semantics of Programming Languages: An Introduction (1993) MIT press.
  29. Zanotti M. Security typings by abstract interpretation. Hermenegildo M, Puebla H, eds. (2002) Springer. 360–375. In Proceedings of the 9th International Static Analysis Symposium (SAS’02), Vol. 2477 of Lecture Notes in Computer Science.

Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Giacobazzi, R.
Right arrow Articles by Mastroeni, I.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?