Hostname: page-component-8448b6f56d-dnltx Total loading time: 0 Render date: 2024-04-18T07:23:21.826Z Has data issue: false hasContentIssue false
  • English
  • Français

Types and trace effects of higher order programs

Part of: JFP Research Articles

Published online by Cambridge University Press:  01 March 2008

CHRISTIAN SKALKA ,
SCOTT SMITH  and
DAVID VAN HORN
CHRISTIAN SKALKA
Affiliation:
The University of Vermont, Burlington, Vermont, USA (email: skalka@cs.uvm.edu)
SCOTT SMITH
Affiliation:
The Johns Hopkins University, Baltimore, Maryland, USA (email: scott@cs.jhu.edu)
DAVID VAN HORN
Affiliation:
Brandeis University, Waltham, Massachusetts, USA (email: dvanhorn@cs.brandeis.edu)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

This paper shows how type effect systems can be combined with model-checking techniques to produce powerful, automatically verifiable program logics for higher order programs. The properties verified are based on the ordered sequence of events that occur during program execution, so-called event traces. Our type and effect systems infer conservative approximations of the event traces arising at run-time, and model-checking techniques are used to verify logical properties of these histories. Our language model is based on the λ-calculus. Technical results include a type inference algorithm for a polymorphic type effect system, and a method for applying known model-checking techniques to the trace effects inferred by the type inference algorithm, allowing static enforcement of history- and stack-based security mechanisms. A type safety result is proven for both unification and subtyping constraint versions of the type system, ensuring that statically well-typed programs do not contain trace event checks that can fail at run-time.

Type
Articles
Information
Journal of Functional Programming , Volume 18 , Issue 2 , March 2008 , pp. 179 - 249
Copyright
Copyright © Cambridge University Press 2007

References

Abadi, M. & Fournet, C. (2003) Access control based on execution history. In Proceedings of the 10th Annual Network and Distributed System Security Symposium (NDSS'03).Google Scholar
Amtoft, T., Nielson, F. & Nielson, H. R. (1999) Type and Effect Systems: Behaviours for Concurrency. London: Imperial College Press.CrossRefGoogle Scholar
Ball, T. & Rajamani, S. K. (2000) Bebop: A symbolic model checker for boolean programs. In proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification. Lecture Notes in Computer Science vol. 1885, pp. 113–130.CrossRefGoogle Scholar
Bartoletti, M., Degano, P. & Ferrari, G. L. (2005a) Enforcing secure service composition. In CSFW. IEEE Computer Society, pp. 211–223.Google Scholar
Bartoletti, M., Degano, P. & Ferrari, G. L. (2005b) History-based access control with local policies. In FoSSaCS, Vladimiro, S. (ed), Lecture Notes in Computer Science, vol. 3441. Springer, pp. 316–332Google Scholar
Bauer, L., Ligatti, J. & Walker, D. (2002a) More enforceable security policies. In Proceedings of the Foundations of Computer Security Workshop.Google Scholar
Bauer, L., Ligatti, J. & Walker, D. (2002b) Types and effects for non-interfering program monitors. In Proceedings of the International Symposium on Software Security.CrossRefGoogle Scholar
Besson, F., Jensen, T., Métayer, D. Le & Thorn, T. (2001) Model checking security properties of control flow graphs. J. Comput. Secur. 9, 217–250.CrossRefGoogle Scholar
Besson, F., deGrenier de Latour, T. Grenier de Latour, T. & Jensen, T. (2002) Secure calling contexts for stack inspection. In PPDP '02: Proceedings of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 76–87.CrossRefGoogle Scholar
Burkart, O., Caucal, D., Moller, F. & Steffen, B. (2001) Verification on infinite structures. In Handbook on Process Algebra, Bergstra, J., Pons, A., & Smolka, S. (eds), Elsevier, pp. 545–623.CrossRefGoogle Scholar
Chen, H. & Wagner, D. (2002) MOPS: An infrastructure for examining security properties of software. In CCS '02: Proceedings of the 9th ACM Conference on Computer and Communications Security, pp. 235–244.CrossRefGoogle Scholar
Colcombet, T. & Fradet, P. (2000) Enforcing trace properties by program transformation. In POPL '00: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 54–66.CrossRefGoogle Scholar
Das, M., Lerner, S. & Seigle, M. (2002) ESP: path-sensitive program verification in polynomial time. In PLDI '02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, pp. 57–68.CrossRefGoogle Scholar
DeLine, R. & Fähndrich, M. (2001) Enforcing high-level protocols in low-level software. In PLDI '01: Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, pp. 59–69.CrossRefGoogle Scholar
Edjlali, G., Acharya, A. & Chaudhary, V. (1998) History-based access control for mobile code. In ACM Conference on Computer and Communications Security, pp. 38–48.Google Scholar
Eifrig, J., Smith, S. & Trifonov, V. (1995) Type inference for recursively constrained types and its application to OOP. In Proceedings of the 1995 Mathematical Foundations of Programming Semantics Conference. Electronic Notes in Computer Science, vol. 1. Elsevier.CrossRefGoogle Scholar
Erlingsson, Ú. & Schneider, F. B. (2000) SASI enforcement of security policies: A retrospective. In NSPW '99: Proceedings of the 1999 Workshop on New Security Paradigms, pp. 87–95.Google Scholar
Esparza, J. (1994) On the decidability of model checking for several mu-calculi and Petri nets. In Proceeding of CAAP '94. Lecture Notes in Computer Science, vol. 787.Google Scholar
Esparza, J., Kucera, A. & Schwoon, S. (2001) Model-checking LTL with regular valuations for pushdown systems. In TACS: 4th International Conference on Theoretical Aspects of Computer Software.CrossRefGoogle Scholar
Foster, J. S., Terauchi, T. & Aiken, A. (2002) Flow-sensitive type qualifiers. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 1–12.CrossRefGoogle Scholar
Gong, L., Mueller, M., Prafullchandra, H. & Schemers, R. (1997) Going beyond the sandbox: An overview of the new security architecture in the Java Development Kit 1.2. In USENIX Symposium on Internet Technologies and Systems, pp. 103–112.Google Scholar
Hamlen, K. W., Morrisett, G. & Schneider, F. B. (2006) Certified in-lined reference monitoring on. NET. In Plas '06: Proceedings of the 2006 Workshop on Programming Languages and Analysis for Security. New York: ACM Press, pp. 7–16.CrossRefGoogle Scholar
Higuchi, Tomoyuki & Ohori, Atsushi. (2007) A static type system for JVM access control. ACM Trans. Program. Lang. Syst. 29 (1), 4.CrossRefGoogle Scholar
Igarashi, A. & Kobayashi, N. (2002) Resource usage analysis. In Conference Record of POPL'02: The 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 331–342.CrossRefGoogle Scholar
Jensen, T., Métayer, D. Le & Thorn, T. (1999) Verification of control flow based security properties. In Proceedings of the 1999 IEEE Symposium on Security and Privacy.Google Scholar
Marriott, K., Stuckey, P. J. & Sulzmann, M. (2003) Resource usage verification. In Proceedings of First Asian Programming Languages Symposium, APLAS 2003.CrossRefGoogle Scholar
Kozen, D. (1983) Results on the propositional mu-calculus. Theor. Comput. Sci., 27, 333–354.CrossRefGoogle Scholar
Mandelbaum, Y., Walker, D. & Harper, R. (2003) An effective theory of type refinements. In Proceedings of the the Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP'03).CrossRefGoogle Scholar
Nierstrasz, O. (1993) Regular types for active objects. In Proceedings of the OOPSL '93 Conference on Object-Oriented Programming Systems, Languages, and Applications, pp. 1–15.CrossRefGoogle Scholar
Palsberg, J. & O'Keefe, P. (1995) A type system equivalent to flow analysis. ACM Trans. Program. Lang. Syst., 17 (4), 576–599.CrossRefGoogle Scholar
Pierce, B. C. (2002) Types and Programming Languages. The MIT Press, Chap. 22.Google Scholar
Pottier, F., Skalka, C. & Smith, S. (2001) A systematic approach to static access control. In Proceedings of the 10th European Symposium on Programming (ESOP'01), Sands, D. (ed), Lecture Notes in Computer Science, vol. 2028. Springer-Verlag, pp. 30-45.CrossRefGoogle Scholar
Rossie, J. G. Jr., (1998) Logical observable entities. In OOPSLA '98: Proceedings of the 13th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 154–165.CrossRefGoogle Scholar
Schmidt, D. A. (1998) Trace-based abstract interpretation of operational semantics. Lisp Symbol. Comput, 10 (3), 237–271.CrossRefGoogle Scholar
Schneider, F. B. (2000) Enforceable security policies. Inform. Syst. Secur. 3 (1), 30–50.Google Scholar
Skalka, C. (2005) Trace effects and object orientation. In PPDP '05: Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 139–150.CrossRefGoogle Scholar
Skalka, C. & Pottier, F. (2003) Syntactic type soundness for HM(X). Electro. Notes Theor. Comput. Sci., 75, pp. 61–74.CrossRefGoogle Scholar
Skalka, C. & Smith, S. (2000) Static enforcement of security with types. In Proceedings of the the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP'00), pp. 34–45.CrossRefGoogle Scholar
Skalka, C. & Smith, S. (2004) History effects and verification. In Asian Programming Languages Symposium.CrossRefGoogle Scholar
Skalka, C., Smith, S. & Van Horn, D. (2005, January) A type and effect system for flexible abstract interpretation of Java. In Proceedings of the ACM Workshop on Abstract Interpretation of Object Oriented Languages. Electronic Notes in Theoretical Computer Science.CrossRefGoogle Scholar
Steffen, B. & Burkart, O. (1992) Model checking for context-free processes. In CONCUR'92, Stony Brook (NY). Lecture Notes in Computer Science (LNCS), vol. 630. Heidelberg, Germany: Springer-Verlag, pp. 123–137.Google Scholar
Stone, C. (2000) Singleton Types and Singleton Kinds. Tech. Rept. CMU-CS-00-153. Carnegie Mellon University.Google Scholar
Sulzmann, M. (2001) A general type inference framework for Hindley/Milner style systems. In International Symposium on Functional and Logic Programming. Lecture Notes in Computer Science, vol. 2024. Springer-Verlag, pp. 246–263.CrossRefGoogle Scholar
Talpin, J.-P. & Jouvelot, P. (1992) The type and effect discipline. In Seventh Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California. Los Alamitos, CA: IEEE Computer Society Press, pp. 162–173.CrossRefGoogle Scholar
Tarski, A. (1955) A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5 (2), 285–309.CrossRefGoogle Scholar
Trifonov, V. & Smith, S. (1996) Subtyping constrained types. In Proceedings of the Third International Static Analysis Symposium, vol. 1145. Springer-Verlag, pp. 349–365.CrossRefGoogle Scholar
VanHorn, D. Horn, D. (2006a) Algorithmic Trace Effect Analysis. M.Phil. thesis, University of Vermont.Google Scholar
VanHorn, D. Horn, D. (2006b) Trace effect analyis, OCaml implementation. Available at: http://www.cs.uvm.edu/dvanhorn/trace/. Accessed June 2007.Google Scholar
Walker, D. (2000) A type system for expressive security policies. In Conference Record of POPL'00: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 254–267.CrossRefGoogle Scholar
Wallach, D. S. & Felten, E. (1998) Understanding Java stack inspection. In Proceedings of the 1998 IEEE Symposium on Security and Privacy.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.