Skip to main content
SpringerLink
Log in

The PER Model of Abstract Non-interference

  • Conference paper
Static Analysis (SAS 2005)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 3672))

Included in the following conference series:

Abstract

In this paper, we study the relationship between two models of secure information flow: the PER model (which uses equivalence relations) and the abstract non-interference model (which uses upper closure operators). We embed the lattice of equivalence relations into the lattice of closures, re-interpreting abstract non-interference over the lattice of equivalence relations. For narrow abstract non-interference, we show that the new definition is equivalent to the original, whereas for abstract non-interference it is strictly less general. The relational presentation of abstract non-interference leads to a simplified construction of the most concrete harmless attacker. Moreover, the PER model of abstract non-interference allows us to derive unconstrained attacker models, which do not necessarily either observe all public information or ignore all private information. Finally, we show how abstract domain completeness can be used for enforcing the PER model of abstract non-interference.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

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

    Google Scholar 

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

    MATH  Google Scholar 

  3. Cohen, E.S.: Information transmission in sequential programs. In: Foundations of Secure Computation, pp. 297–335 (1978)

    Google Scholar 

  4. Cortesi, A., Filé, G., Winsborough, W.: The quotient of an abstract interpretation. Theor. Comput. Sci. 202(1-2), 163–192 (1998)

    Article  MATH  Google Scholar 

  5. 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 

  6. Cousot, P., Cousot, R.: Constructive versions of Tarski’s fixed point theorems. Pacific J. Math. 82(1), 43–57 (1979)

    MATH  MathSciNet  Google Scholar 

  7. 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 

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

    Article  MATH  Google Scholar 

  9. 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)

    Chapter  Google Scholar 

  10. Giacobazzi, R., Mastroeni, I.: Adjoining declassification and attack models by abstract interpretation. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 295–310. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. of the ACM 47(2), 361–416 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  12. Hunt, S.: Pers generalise projections for strictness analysis (extended abstract). In: Proc. 1990 Glasgow Workshop on Functional Programming, Workshops in Computing, Ullapool. Springer, Heidelberg (1991)

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  14. Landauer, J., Redmond, T.: A lattice of information. In: Proc. of the IEEE Computer Security Foundations Workshop, pp. 65–70. IEEE Computer Society Press, Los Alamitos (1993)

    Google Scholar 

  15. 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 

  16. Ranzato, F., Tapparo, F.: Strong preservation as completeness in abstract interpretation. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 18–32. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  17. 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 

  18. 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  MATH  Google Scholar 

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

    Google Scholar 

  20. Tarski, A.: A lattice theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 285–310 (1955)

    MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  22. Zdancewic, S., Myers, A.C.: Robust declassification. In: Proc. of the IEEE Computer Security Foundations Workshop, pp. 15–23. IEEE Computer Society Press, Los Alamitos (2001)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing, School of Informatics, City University, London, UK

    Sebastian Hunt

  2. Department of Computing and Information Sciences, Kansas State University, Manhattan, Kansas, USA

    Isabella Mastroeni

Authors
  1. Sebastian Hunt
    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. Department of Computing, Imperial College London,  

    Chris Hankin

  2. Department of Computing, Imperial College London, 180 Queen’s Gate, SW7 2BZ, London, UK

    Igor Siveroni

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hunt, S., Mastroeni, I. (2005). The PER Model of Abstract Non-interference. In: Hankin, C., Siveroni, I. (eds) Static Analysis. SAS 2005. Lecture Notes in Computer Science, vol 3672. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11547662_13

Download citation

  • DOI: https://doi.org/10.1007/11547662_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-28584-7

  • Online ISBN: 978-3-540-31971-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation