Enforcing Safety Properties Using Type Specialization

  • Peter Thiemann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2028)


Type specialization can serve as a powerful tool in enforcing safety properties on foreign code. Using the specification of a monitoring interpreter, polyvariant type specialization can produce compiled code that is guaranteed to obey a specified safety policy. It propagates a security state at compile-time and generates code for each different security state. The resulting code contains virtually no run-time operations on the security state, at the price of some code duplication. A novel extension of type specialization by intersection types limits the amount of code duplication considerably, thus making the approach practical.


Security Policy Partial Evaluation Security State Safety Policy Lambda Calculus 
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.


  1. 1.
    A.-R. Adl-Tabatabai, G. Langdale, S. Lucco, and R. Wahbe. Efficient and language-independent mobile programs. In Proceedings of the ACM SIGPLAN’ 96 Conference on Programming Language Design and Implementation (PLDI), pages 127–136, Philadelphia, Pa., May 1996.Google Scholar
  2. 2.
    A. W. Appel and A. P. Felty. A semantics model of types and machine instructions for proof-carrying code. In Reps [29], pages 243–253.Google Scholar
  3. 3.
    F. Barbanera and M. Dezani-Ciancaglini. Intersection and union types. In T. Ito and A. Meyer, editors, Proc. Theoretical Aspects of Computer Software, volume 526 of Lecture Notes in Computer Science, Sendai, Japan, 1991. Springer-Verlag.Google Scholar
  4. 4.
    T. Colcombet and P. Fradet. Enforcing trace properties by program transformation. In Reps [29], pages 54–66.Google Scholar
  5. 5.
    M. Coppo and M. Dezani-Ciancaglini. A new type-assignment for λ-terms. Archiv. Math. Logik, 19(139–156), 1978.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    O. Danvy and A. Filinski. Abstracting control. In Proc. 1990 ACM Conference on Lisp and Functional Programming, pages 151–160, Nice, France, 1990. ACM Press.Google Scholar
  7. 7.
    O. Danvy and A. Filinski. Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science, 2:361–391, 1992.zbMATHMathSciNetGoogle Scholar
  8. 8.
    D. Evans and A. Twyman. Flexible policy-directed code safety. In IEEE Symposium on Security and Privacy, Oakland, CA, May 1999.Google Scholar
  9. 9.
    R. Glück. On the generation of specializers. Journal of Functional Programming, 4(4):499–514, Oct. 1994.Google Scholar
  10. 10.
    R. Glück and J. Jørgensen. Generating optimizing specializers. In IEEE International Conference on Computer Languages, pages 183–194. IEEE Computer Society Press, 1994.Google Scholar
  11. 11.
    R. Glück and J. Jørgensen. Generating transformers for deforestation and supercompilation. In B. Le Charlier, editor, Static Analysis, volume 864 of Lecture Notes in Computer Science, pages 432–448. Springer-Verlag, 1994.Google Scholar
  12. 12.
    J. Hughes. Type specialisation for the λ-calculus; or, a new paradigm for partial evaluation based on type inference. In O. Danvy, R. Glück, and P. Thiemann, editors, Partial Evaluation, volume 1110 of Lecture Notes in Computer Science, pages 183–215, Schloß Dagstuhl, Germany, Feb. 1996. Springer-Verlag.Google Scholar
  13. 13.
    J. Hughes. The correctness of type specialisation. In G. Smolka, editor, Proc. 9th European Symposium on Programming, volume 1782 of Lecture Notes in Computer Science, pages 215–229, Berlin, Germany, Mar. 2000. Springer-Verlag.Google Scholar
  14. 14.
    Java2 platform., 2000.
  15. 15.
    N. D. Jones, C. K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall, 1993.Google Scholar
  16. 16.
    D. Kozen. Language-based security. Technical Report TR99-1751, Cornell University, Computer Science, June 15, 1999.Google Scholar
  17. 17.
    Úlfar Erlingsson and F. B. Schneider. SASI enforcement of security policies: A retrospective. In Proceedings of the 1999 New Security Paradigms Workshop, Caledon Hills, Ontario, Canada, Sept. 1999.Google Scholar
  18. 18.
    T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996.Google Scholar
  19. 19.
    S. Lucco, O. Sharp, and R. Wahbe. Omniware: A universal substrate for web programming. WorldWideWeb Journal, 1(1), Dec. 1995.Google Scholar
  20. 20.
    N. G. Michael and A. W. Appel. Machine instruction syntax and semantics in higher order logic. In 17th International Conference on Automated Deduction (CADE-17), June 2000.Google Scholar
  21. 21.
    G. Morrisett, D. Walker, K. Crary, and N. Glew. From system F to typed assembly language. In L. Cardelli, editor, Proc. 25th Annual ACM Symposium on Principles of Programming Languages, San Diego, CA, USA, Jan. 1998. ACM Press.Google Scholar
  22. 22.
    G. C. Necula. Proof-carrying code. In Proceedings of the 24th ACM Symposium on Principles of Programming Languages, Paris, France, Jan. 1997.Google Scholar
  23. 23.
    G. C. Necula and P. Lee. Safe kernel extensions without run-time checking. In Proceedings of the Second Symposium on Operating System Design and Implementation, Seattle, Wa., Oct. 1996.Google Scholar
  24. 24.
    G. C. Necula and P. Lee. The design and implementation of a certifying compiler. In K. D. Cooper, editor, Proceedings of the 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 333–344, Montreal, Canada, June 1998. ACM. Volume 33(5) of SIGPLAN Notices.Google Scholar
  25. 25.
    G. C. Necula and P. Lee. Safe, Untrusted Agents Using Proof-Carrying Code. In G. Vigna, editor, Mobile Agent Security, Lecture Notes in Computer Science No. 1419, pages 61–91. Springer-Verlag: Heidelberg, Germany, 1998.CrossRefGoogle Scholar
  26. 26.
    B. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, Feb. 1991.Google Scholar
  27. 27.
    B. C. Pierce. Intersection types and bounded polymorphism. Mathematical Structures in Computer Science, 11, 1996.Google Scholar
  28. 28.
    F. Pottier, C. Skalka, and S. Smith. A systematic approach to static access control. In D. Sands, editor, Proc. 10th European Symposium on Programming, Lecture Notes in Computer Science, Genova, Italy, Apr. 2001. Springer-Verlag.Google Scholar
  29. 29.
    T. Reps, editor. Proc. 27th Annual ACM Symposium on Principles of Programming Languages, Boston, MA, USA, Jan. 2000. ACM Press.Google Scholar
  30. 30.
    J. C. Reynolds. Definitional interpreters for higher-order programming languages. In ACM Annual Conference, pages 717–740, July 1972.Google Scholar
  31. 31.
    F. B. Schneider. Enforceable security policies. Technical Report TR99-1759, Cornell University, Ithaca, NY, USA, July 1999.Google Scholar
  32. 32.
    M. Sperber, R. Glück, and P. Thiemann. Bootstrapping higher-order program transformers from interpreters. In Proc. 11th Annual Symposium on Applied Computing, SAC (SAC’ 96), pages 408–413, Philadelphia, PA, Feb. 1996. ACM.Google Scholar
  33. 33.
    M. Sperber and P. Thiemann. Two for the price of one: Composing partial evaluation and compilation. In Proc. of the ACM SIGPLAN’ 97 Conference on Programming Language Design and Implementation, pages 215–225, Las Vegas, NV, USA, June 1997. ACM Press.Google Scholar
  34. 34.
    V. F. Turchin. Program tranformation with metasystem transitions. Journal of Functional Programming, 3(3):283–313, July 1993.CrossRefGoogle Scholar
  35. 35.
    R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham. Efficient software-based fault isolation. In Proceedings of the 14th ACM Symposium on Operating Systems Principles, pages 203–216, 1993.Google Scholar
  36. 36.
    D. Walker. A type system for expressive security policies. In Reps [29], pages 254–267.Google Scholar
  37. 37.
    D. S. Wallach and E. W. Felten. Understanding java stack inspection. In Proceedings of 1998 IEEE Symposium on Security and Privacy, Oakland, CA, May 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Peter Thiemann
    • 1
  1. 1.Universität FreiburgFreiburg

Personalised recommendations