Advertisement

Secure Information Flow and CPS

  • Steve Zdancewic
  • Andrew C. Myers
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2028)

Abstract

Security-typed languages enforce secrecy or integrity policies by type-checking. This paper investigates continuation-passing style as a means of proving that such languages enforce non-interference and as a first step towards understanding their compilation. We present a low- level, secure calculus with higher-order, imperative features. Our type system makes novel use of ordered linear continuations.

Keywords

Operational Semantic Program Counter Covert Channel Primitive Operation Imperative Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon Riecke. A core calculus of dependency. In Proc. 26th ACM Symp. on Principles of Programming Languages (POPL), pages 147–160, 1999.Google Scholar
  2. 2.
    Samson Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111:3–57, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Johan Agat. Transforming out timing leaks. In Proc. 27th ACM Symp. on Principles of Programming Languages (POPL), January 2000.Google Scholar
  4. 4.
    Andrew Appel. Compiling with Continuations. Cambridge University Press, 1992.Google Scholar
  5. 5.
    Gavin Bierman. A classical linear lambda calculus. Theoretical Computer Science, 227(1-2):43–78, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Proc. 26th ACM Symp. on Principles of Programming Languages (POPL), pages 262–275, 1999.Google Scholar
  7. 7.
    Daniel Damian and Olivier Danvy. Syntactic accidents in program analysis: On the impact of the CPS transformation. In Proc. 5th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 209–220, 2000.Google Scholar
  8. 8.
    Olivier Danvy and Andrzej Filinski. Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science, 2:361–391, 1992.zbMATHMathSciNetCrossRefGoogle Scholar
  9. 9.
    Dorothy E. Denning and Peter J. Denning. Certification of Programs for Secure Information Flow. Comm. of the ACM, 20(7):504–513, July 1977.zbMATHCrossRefGoogle Scholar
  10. 10.
    J. Mylaert Filho and G. Burn. Continuation passing transformations and abstract interpretation. In Proc. First Imperial College, Department of Computing, Workshop on Theory and Formal Methods, 1993.Google Scholar
  11. 11.
    Andrzej Filinski. Linear continuations. In Proc. 19th ACM Symp. on Principles of Programming Languages (POPL), 1992.Google Scholar
  12. 12.
    Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Proceedings of the ACM’ 93 Conference on Programming Language Design and Implementation, 1993.Google Scholar
  13. 13.
    Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    J. A. Goguen and J. Meseguer. Security policies and security models. In Proc. IEEE Symposium on Security and Privacy, pages 11–20, April 1982.Google Scholar
  15. 15.
    Robert Harper and Mark Lillibridge. Explicit polymorphism and CPS conversion. In Proc. 20th ACM Symp. on Principles of Programming Languages (POPL), 1993.Google Scholar
  16. 16.
    Nevin Heintze and Jon G. Riecke. The SLam calculus: Programming with secrecy and integrity. In Proc. 25th ACM Symp. on Principles of Programming Languages (POPL), San Diego, California, January 1998.Google Scholar
  17. 17.
    Kohei Honda, Vasco Vasconcelos, and Nobuko Yoshida. Secure information flow as typed process behaviour. In Proc. of the 9th European Symposium on Programming, volume 1782 of Lecture Notes in Computer Science, pages 180–199. Springer, 2000.Google Scholar
  18. 18.
    Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From system F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):528–569, May 1999.CrossRefGoogle Scholar
  19. 19.
    Steven S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann Publishers, 1997.Google Scholar
  20. 20.
    Andrew C. Myers. JFlow: Practical mostly-static information flow control. In Proc. 26th ACM Symp. on Principles of Programming Languages (POPL), San Antonio, TX, USA, January 1999.Google Scholar
  21. 21.
    Andrew C. Myers and Barbara Liskov. A decentralized model for information flow control. In Proc. 17th ACM Symp. on Operating System Principles (SOSP), pages 129–142, Saint-Malo, France, 1997.Google Scholar
  22. 22.
    George C. Necula. Proof-carrying code. In Proc. 24th ACM Symp. on Principles of Programming Languages (POPL), pages 106–119, January 1997.Google Scholar
  23. 23.
    Flemming Nielson. A denotational framework for data flow analysis. Acta Informatica, 18:265–287, 1982.zbMATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    Jeff Polakow and Frank Pfenning. Properties of terms in continuation-passing style in an ordered logical framework. In J. Despeyroux, editor, 2nd Workshop on Logical Frameworks and Meta-languages, Santa Barbara, California, June 2000.Google Scholar
  25. 25.
    François Pottier and Sylvain Conchon. Information flow inference for free. In Proc. 5th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 46–57, 2000.Google Scholar
  26. 26.
    Andrei Sabelfeld and David Sands. A PER model of secure information flow in sequential programs. In Proceedings of the European Symposium on Programming. Springer-Verlag, March 1999. LNCS volume 1576.Google Scholar
  27. 27.
    Andrei Sabelfeld and David Sands. Probabilistic noninterference for multi-threaded programs. In Proceedings of the 13th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, July 2000.Google Scholar
  28. 28.
    Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation: An International Journal, 1993.Google Scholar
  29. 29.
    Amr Sabry and Matthias Felleisen. Is continuation-passing useful for data flow analysis? In Proc. SIGPLAN’ 94 Conference on Programming Language Design and Implementation, pages 1–12, 1994.Google Scholar
  30. 30.
    Geoffrey Smith and Dennis Volpano. Secure information flow in a multi-threaded imperative language. In Proc. 25th ACM Symp. on Principles of Programming Languages (POPL), San Diego, California, January 1998.Google Scholar
  31. 31.
    David N. Turner and Philip Wadler. Operational interpretations of linear logic. Theoretical Computer Science, 2000. To Appear.Google Scholar
  32. 32.
    Dennis Volpano, Geoffrey Smith, and Cynthia Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):167–187, 1996.Google Scholar
  33. 33.
    Philip Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, Programming Concepts and Methods. North Holland, 1990.Google Scholar
  34. 34.
    Philip Wadler. A taste of linear logic. In Mathematical Foundations of Computer Science, volume 711 of Lecture Notes in Computer Science. Springer-Verlag, 1993.Google Scholar
  35. 35.
    Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  36. 36.
    Steve Zdancewic and Andrew C. Myers. Confidentiality and integrity with untrusted hosts. Technical Report 2000-1810, Cornell University, 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Steve Zdancewic
    • 1
  • Andrew C. Myers
    • 1
  1. 1.Cornell UniversityIthacaUSA

Personalised recommendations