Skip to main content
SpringerLink
Log in

A Per Model of Secure Information Flow in Sequential Programs

  • Published:
Higher-Order and Symbolic Computation

Abstract

This paper proposes an extensional semantics-based formal specification of secure information-flow properties in sequential programs based on representing degrees of security by partial equivalence relations (pers). The specification clarifies and unifies a number of specific correctness arguments in the literature and connections to other forms of program analysis. The approach is inspired by (and in the deterministic case equivalent to) the use of partial equivalence relations in specifying binding-time analysis, and is thus able to specify security properties of higher-order functions and “partially confidential data”. We also show how the per approach can handle nondeterminism for a first-order language, by using powerdomain semantics and show how probabilistic security properties can be formalised by using probabilistic powerdomain semantics. We illustrate the usefulness of the compositional nature of the security specifications by presenting a straightforward correctness proof for a simple type-based security analysis.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abadi, M., Banerjee, A., Heintze, N., and Riecke, J. A core calculus of dependency. In POPL '99, Proceedings of the 26th Annual ACM Symposium on Principles of Programming Languages (January 1999), 1999.

  2. Abadi, M. and Plotkin, G. A per model of polymorphism and recursive types. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, 1990, pp. 355-365.

  3. Andrews, G.R. and Reitman, R.P. An axiomatic approach to information flow in programs. ACM TOPLAS 2(1) (1980) 56-75.

    Google Scholar 

  4. Banâ tre, J.-P., Bryce, C., and Le Métayer, D. Compile-time detection of information flow in sequential programs. In Computer Security-ESORICS '94, 3rd European Symposium on Research in Computer Security, 1994, D. Gollmann (Ed.). pp. 55-73. Vol. 875 of Lecture Notes in Computer Science.

  5. Bell, D. and LaPadula, L. Secure computer systems: Unified exposition and multics interpretation. MTR-2997, Rev. 1, The MITRE Corporation, Bedford, Mass, 1976.

    Google Scholar 

  6. Cohen, E.S. Information transmission in computational systems. ACM SIGOPS Operating Systems Review 11(5) (1977) 133-139.

    Google Scholar 

  7. Cohen, E.S. Information transmission in sequential programs. In Foundations of Secure Computation, R.A. DeMillo, D.P. Dobkin, A.K. Jones, and R.J. Lipton (Eds.). Academic Press, 1978, pp. 297-335.

  8. Das, M., Reps, T., and Hentenryck, P.V. Semantic foundations of binding-time analysis for imperative programs. Partial Evaluation and Seman-tics-Based Program Manipulation. La Jolla, California, 1995, pp. 100-110.

  9. Denning, D.E. A lattice model of secure information flow. Communications of the ACM 19(5) (1976) 236-243.

    Google Scholar 

  10. Denning, D.E. and Denning, P.J. Certification of programs for secure information flow. Communications of the ACM 20(7) (1977) 504-513.

    Google Scholar 

  11. Focardi, R. and Gorrieri, R. A classification of security properties for process algebra. J. Computer Security 3(1) (1994) 5-33.

    Google Scholar 

  12. Goguen, J. and Meseguer, J. Security policies and security models. In Proceedings of the IEEE Symposium on Security and Privacy, 1982.

  13. Gray III, J. Probabilistic interference. In Proceedings of the IEEE Symposium on Security and Privacy, Oakland, California, 1990, pp. 170-179.

  14. Hankin, C.L. and Le Métayer, D. A type-based framework for program analysis. In Proceedings of the First Static Analysis Symposium, 1994. Vol. 864 of LNCS.

  15. Heintze, N. and Riecke, J.G. The slam calculus: Programming with secrecy and integrity. In Conference Record of POPL'98: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California 1998, pp. 365-377.

  16. Henglein, F. and Sands, D. A semantic model of binding times for safe partial evaluation. In Proc. Programming Languages: Implementations, Logics and Programs (PLILP), Utrecht, The Netherlands, M. Hermenegildo and S.D. Swierstra (Eds.). 1995, pp. 299-320. Vol. 982 of Lecture Notes in Computer Science.

  17. Hunt, L.S. Abstract interpretation of functional languages: From theory to practice. Ph.D. thesis, Department of Computing, Imperial College of Science, Technology and Medicine, 1991.

  18. Hunt, S. PERs generalise projections for strictness analysis. In Draft Proceedings of the third glasgow Functional Programming Workshop. Ullapool, 1900.

  19. Hunt, S. and Sands, D. Binding time analysis: A new perspective. In Proceedings of the ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'91), 1991, pp. 154-164. ACM SIGPLAN Notices 26(9).

  20. Jensen, T.P. Abstract interpretation in logical form. Ph.D. thesis, Imperial College, University of London. 1992. Available as DIKU Report 93/11 from DIKU, University of Copenhagen.

  21. Jones, C. and Plotkin, G.D. A probabilistic powerdomain of evaluations. In Proceedings, Fourth Annual Symposium on Logic in Computer Science, Asilomar Conference Center, Pacific Grove, California, 1989, pp. 186-195.

  22. Kozen, D. Semantics of probabilistic programs. Journal of Computer and System Sciences 22 (1981) 328-350.

    Google Scholar 

  23. Kozen, D. A probabilistic PDL. Journal of Computer and System Sciences 30 (1985) 162-178.

    Google Scholar 

  24. Launchbury, J. Projection factorisations in partial evaluation. Ph.D. thesis, Department of Computing, University of Glasgow, 1989.

  25. Leino, K.R.M. and Joshi, R. A semantic approach to secure information flow. In MPC'98, 1998.

  26. Leino, K.R.M. and Joshi, R. A semantic approach to secure information flow. Science of Computer Programming 37(1-3) (2000) 113-138.

    Google Scholar 

  27. Manes, E. Graduate Texts in Mathematics. Vol. 26, 1976, Springer-Verlag.

  28. McCullough, D. Specifications for multi-level security and hook-up property. In Proceedings of the IEEE Symposium on Security and Privacy, 1987, pp. 161-166.

  29. McLean, J. Security models and information flow. In Proceedings of the IEEE Symposium on Security and Privacy, Oakland, California, 1990a, pp. 180-187.

  30. McLean, J. The specification and modeling of computer security. Computer 23(1) (1990b) 9-16.

    Google Scholar 

  31. McLean, J. Security models. In Encyclopedia of Software Engineering, J. Marciniak (Ed.). Wiley &;;; Sons. 1994.

  32. Mizuno, M. and Schmidt, D. Ascurity flowcontrol algorithm and its denotational semantics correctness proof. Formal Aspects of Computing 4(6A) (1992) 727-754.

    Google Scholar 

  33. Moskowitz, I.S. and Costich, O.L. A classical automata approach to noninterference type problems. In The Computer Security Foundations Workshop V proceedings, the Franconia Inn, Franconia, New Hampshire. June 16-18, 1992, pp. 2-8.

  34. Nielson, F. Two-level semantics and abstract interpretation. Theoretical Computer Science-Fundamental Studies 69 (1989) 117-242.

    Google Scholar 

  35. Ørbæ k, P. Can you trust your data?. In Proceedings of the TAPSOFT/FASE'95 Conference, P.D. Mosses, M.I. Schwartzbach, and M. Nielsen (Eds.). Aarhus, Denmark, 1995, pp. 575-590.

  36. Ørbæ k, P. Trust and dependence analysis. Ph.D. thesis, Dept. of Computer Science, Univ. of Aarhus. BRICS report DS-97-2, 1997.

  37. Ørbæ k, P. and Palsberg, J. Trust in the λ-calculus. Journal of Functional Programming 7(4) (1997).

  38. Plotkin, G. Post-graduate lecture notes in advanced domain theory (incorporating the “Pisa Notes”). Dept. of Computer Science, Univ. of Edinburgh. 1981.

  39. Plotkin, G.D. A power domain construction. SIAM Journal on Computing 5(3) (1976) 452-487.

    Google Scholar 

  40. Reynolds, J.C. Types, abstraction and parametric polymorphism. In Proceedings 9th IFIP World Computer Congress, Information Processing '83, Paris, France, 19-23 Sept 1983, R.E.A. Mason (Ed.). North Holland, Amsterdam; 1983, pp. 513-523.

    Google Scholar 

  41. Sabelfeld, A. and Sands, D. A per model of secure information flow in sequential programs. In Proceedings of the 8th European Symposium on Programming, ESOP'99, Amsterdam, 1999, pp. 40-58.

  42. Sabelfeld, A. and Sands, D. Probabilistic noninterference for multi-threaded programs. In Proceedings of the 13th IEEE Computer Security Foundations Workshop, Cambridge, England, 2000.

  43. Smith, G. and Volpano, D. Secure information flow in a multi-threaded imperative language. In Conference Record of POPL '98: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1998, pp. 355-364.

  44. Smyth, M.B. Power domains. Journal of Computer and Systems Sciences 16(1) (1978) 23-36.

    Google Scholar 

  45. Thiemann, P. and Klaeren, H. Binding-time analysis by security analysis. Universitt Tübingen, 1997.

  46. Volpano, D. and Smith, G. Eliminating covert flows with minimum typings. In Proc. 10th IEEE Computer Security Foundations Workshop, 1997, pp. 156-168.

  47. Volpano, D. and Smith, G. Probabilistic noninterference in a concurrent language. Journal of Computer Security 7(2,3) (1999) 231-253.

    Google Scholar 

  48. Volpano, D., Smith, G., and Irvine, C. A sound type system for secure flow analysis. J. Computer Security 4(3) (1996) 1-21.

    Google Scholar 

  49. Wadler, P. Theorems for free. Functional Programming Languages and Computer Architecture. 1989, pp. 347-359.

  50. Wadler, P. and Hughes, R.J.M. Projections for strictness analysis. In 1987 Conference on Functional Programming and Computer Architecture, Portland, Oregon, 1987, pp. 385-407.

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Chalmers University of Technology and the University of Göteborg, 412 96, Göteborg, Sweden

    Andrei Sabelfeld & David Sands

Authors
  1. Andrei Sabelfeld
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Sands
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Sabelfeld, A., Sands, D. A Per Model of Secure Information Flow in Sequential Programs. Higher-Order and Symbolic Computation 14, 59–91 (2001). https://doi.org/10.1023/A:1011553200337

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1011553200337

Search

Navigation