Abstract
Distributed applications can be structured using sessions that specify flows of messages between roles. We design a small specific language to declare sessions. We then build a compiler, called s2ml, that transforms these declarations down to ML modules securely implementing the sessions. Every run of a well-typed program executing a session through its generated module is guaranteed to follow the session specification, despite any low-level attempt by coalitions of remote peers to deviate from their roles. We detail the inner workings of our compiler, along with our design choices, and illustrate the usage of s2ml with two examples: a simple remote procedure call session, and a complex session for a conference management system.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bhargavan, K., Corin, R., Fournet, C., Gordon, A.D.: Secure sessions for web services. In: ACM Workshop on Secure Web Services (SWS), pp. 11–22 (October 2004)
Bhargavan, K., Fournet, C., Gordon, A.D., Tse, S.: Verified interoperable implementations of security protocols. In: 19th IEEE Computer Security Foundations Workshop (CSFW), July 2006, pp. 139–152 (2006)
J. Billings, P. Sewell, M. Shinwell, and R. Strniša. Type-Safe Distributed Programming for OCaml. In: ACM SIGPLAN Workshop on ML, September 2006 (2006)
Bonelli, E., Compagnoni, A., Gunter, E.: Correspondence assertions for process synchronization in concurrent communications. In: Brogi, A. (ed.) 1st International Workshop on Foundations of Coordination Languages and Software Architectures (FOCLASA). ENTCS, vol. 97, pp. 175–195. Elsevier, Amsterdam (2004)
Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred programming for web services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, Springer, Heidelberg (2007)
Carpineti, S., Laneve, C.: A basic contract language for web services. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 197–213. Springer, Heidelberg (2006)
Chaki, S., Rajamani, S.K., Rehof, J.: Types as models: model checking message-passing programs. In: 29th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL), January 2002, pp. 45–57 (2002)
Corin, R., Denielou, P.M., Fournet, C., Bhargavan, K., Leifer, J.: Secure implementations for typed session abstractions. In: 20th IEEE Computer Security Foundations Symposium (CSF 2007), Venice, Italy, July 2007, IEEE Computer Society Press, Los Alamitos (to appear, 2007)
Corin, R., Dénielou, P.-M., Fournet, C., Bhargavan, K., Leifer, J.: Secure sessions project (2007), http://www.msr-inria.inria.fr/projects/sec/sessions/
Deniélou, P.-M., Leifer, J.J.: Abstraction preservation and subtyping in distributed languages. In: 11th International Conference on Functional Programming (ICFP) (2006)
Dezani-Ciancaglini, M., Mostrous, D., Yoshida, N., Drossopoulou, S.: Session types for object-oriented languages. In: 20th European Conference for Object-Oriented Languages, July 2006 (2006)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)
Fahndrich, M., Aiken, M., Hawblitzel, C., Hodson, G.H.O., Larus, J.R., Levi, S.: Language support for fast and reliable message-based communication in Singularity OS. In: EUROSYS (2006)
Simon, J.: Gay and Malcolm Hole. Types and subtypes for client-server interactions. In: Programming Languages and Systems, 8th European Symposium on Programming (ESOP), pp. 74–90 (1999)
Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. Journal of Computer Security 11(4), 451–521 (2003)
Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type disciplines for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998 and ETAPS 1998. LNCS, vol. 1381, pp. 22–138. Springer, Heidelberg (1998)
Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008 (to appear, 2008)
Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. In: 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL), pp. 128–141 (2001)
Milner, R., Tofte, M., Harper, R.: The Definition of Standard ML. MIT Press, Cambridge (1990)
Objective Caml, http://caml.inria.fr
Sewell, P., Leifer, J.J., Wansbrough, K., Nardelli, F.Z., Allen-Williams, M., Habouzit, P., Vafeiadis, V.: Acute: High-level programming language design for distributed computation. In: 10th International Conference on Functional Programming (ICFP), September 2005 (2005)
Syme, D.: F# (2005), http://research.microsoft.com/fsharp/
Vallecillo, A., Vasconcelos, V.T., Ravara, A.: Typing the behavior of objects and components using session types. In: 1st International Workshop on Foundations of Coordination Languages and Software Architectures (FOCLASA). ENTCS, vol. 68, Elsevier, Amsterdam (2003)
Vasco, T.: Vasconcelos, Simon Gay, and António Ravara. Typechecking a multithreaded functional language with session types, TCS 368(1–2), 64–87 (2006)
Yoshida, N., Vasconcelos, V.T.: Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication. In: 1st International Workshop on Security and Rewriting Techniques, ENTCS (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Corin, R., Deniélou, PM. (2008). A Protocol Compiler for Secure Sessions in ML. In: Barthe, G., Fournet, C. (eds) Trustworthy Global Computing. TGC 2007. Lecture Notes in Computer Science, vol 4912. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78663-4_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-78663-4_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78662-7
Online ISBN: 978-3-540-78663-4
eBook Packages: Computer ScienceComputer Science (R0)