Abstract
Distributed applications may be specified as parallel compositions of processes that summarize their global interactions and hide local implementation details. These processes define a fixed protocol (also known as a contract, or a session) which may be used for instance to compile or verify code for these applications.
Security is a concern when the runtime environment for these applications is not fully trusted. Then, parts of their implementation may run on remote, corrupted machines, which do not comply with the global process specification. To mitigate this concern, one may write defensive implementations that monitor the application run and perform cryptographic checks. However, hand crafting such implementations is ad hoc and error-prone.
We develop a theory of secure implementations for process specifications. We propose a generic defensive implementation scheme, relying on history-tracking mechanisms, and we identify sufficient conditions on processes, expressed as a new type system, that ensure that our implementation is secure for all integrity properties. We illustrate our approach on a series of examples and special cases, including an existing implementation for sequential multiparty sessions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bhargavan, K., Corin, R., Deniélou, P.-M., Fournet, C., Leifer, J.J.: Cryptographic protocol synthesis and verification for multiparty sessions. In: 22nd IEEE Computer Security Foundations Symposium (CSF 2009) (July 2009)
Boudol, G., Castellani, I.: Flow models of distributed computations: three equivalent semantics for CCS. Information and Computation 114(2), 247–314 (1994)
Corin, R., Deniélou, P.-M., Fournet, C., Bhargavan, K., Leifer, J.J.: A secure compiler for session abstractions. Journal of Computer Security (Special issue for CSF 2007) 16(5), 573–636 (2008)
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)
Gay, S.J., Hole, M.: Types and subtypes for client-server interactions. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 74–90. Springer, Heidelberg (1999)
Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type disciplines for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)
Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 273–284. ACM, New York (2008)
Milner, R.: Communication and Concurrency. Prentice-Hall, Inc., Englewood Cliffs (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Planul, J., Corin, R., Fournet, C. (2009). Secure Enforcement for Global Process Specifications. In: Bravetti, M., Zavattaro, G. (eds) CONCUR 2009 - Concurrency Theory. CONCUR 2009. Lecture Notes in Computer Science, vol 5710. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04081-8_34
Download citation
DOI: https://doi.org/10.1007/978-3-642-04081-8_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04080-1
Online ISBN: 978-3-642-04081-8
eBook Packages: Computer ScienceComputer Science (R0)