Abstract
We consider a calculus for multiparty sessions with delegation, enriched with security levels for session participants and data. We propose a type system that guarantees both session safety and a form of access control. Moreover, this type system ensures secure information flow, including controlled forms of declassification. In particular, the type system prevents leaks that could result from an unrestricted use of the control constructs of the calculus, such as session opening, selection, branching and delegation. We illustrate the use of our type system with a number of examples, which reveal an interesting interplay between the constraints used in security type systems and those used in session types to ensure properties like communication safety and session fidelity.
Work partially funded by the INRIA Sophia Antipolis COLOR project MATYSS, by the ANR-SETI-06-010 and ANR-08-EMER-010 grants, and by the MIUR Projects DISCO and IPODS.
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
Almeida Matos, A., Boudol, G.: On Declassification and the Non-Disclosure Policy. Journal of Computer Security 17, 549–597 (2009)
Bettini, L., Coppo, M., D’Antoni, L., De Luca, M., Dezani-Ciancaglini, M., Yoshida, N.: Global Progress in Dynamically Interleaved Multiparty Sessions. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 418–433. Springer, Heidelberg (2008)
Bhargavan, K., Corin, R., Deniélou, P.-M., Fournet, C., Leifer, J.J.: Cryptographic Protocol Synthesis and Verification for Multiparty Sessions. In: Proc. CSF 2009, pp. 124–140. IEEE Computer Society, Los Alamitos (2009)
Boreale, M., Bruni, R., Nicola, R., Loreti, M.: Sessions and Pipelines for Structured Service Programming. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 19–38. Springer, Heidelberg (2008)
Boudol, G., Kolundzija, M.: Access Control and Declassification. In: Proc. Computer Network Security. CCIS, vol. 1, pp. 85–98. Springer, Heidelberg (2007)
Denning, D.E.R.: Cryptography and Data Security. Addison-Wesley, Reading (1982)
Dezani-Ciancaglini, M., de’Liguoro, U.: Sessions and Session Types: An Overview. In: Laneve, C. (ed.) WSFM 2010. LNCS, vol. 6194, pp. 1–28. Springer, Heidelberg (2010)
Focardi, R., Gorrieri, R.: Classification of Security Properties (Part I: Information Flow). In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001)
Goguen, J.A., Meseguer, J.: Security Policies and Security Models. In: Proc. IEEE Symposium on Security and Privacy, pp. 11–20. IEEE Computer Society, Los Alamitos (1982)
Honda, K., Yoshida, N.: A Uniform Type Structure for Secure Information Flow. In: Proc. POPL 2002, pp. 81–92. ACM Press, New York (2002)
Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchronous Session Types. In: Proc. POPL 2008, pp. 273–284. ACM Press, New York (2008)
Kobayashi, N.: Type-Based Information Flow Analysis for the Pi-Calculus. Acta Informatica 42(4-5), 291–347 (2005)
Kolundžija, M.: Security Types for Sessions and Pipelines. In: Bruni, R., Wolf, K. (eds.) WSFM 2008. LNCS, vol. 5387, pp. 175–190. Springer, Heidelberg (2009)
Milner, R.: Communicating and Mobile Systems: the Pi-Calculus. CUP, Cambridge (1999)
Planul, J., Corin, R., Fournet, C.: Secure Enforcement for Global Process Specifications. In: Proc. CONCUR 2009. LNCS, vol. 5710, pp. 511–526. Springer, Heidelberg (2009)
Sabelfeld, A., Myers, A.C.: Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)
Sabelfeld, A., Sands, D.: Probabilistic Noninterference for Multi-threaded Programs. In: Proc. CSFW 2000, pp. 200–214. IEEE Computer Society, Los Alamitos (2000)
Sabelfeld, A., Sands, D.: Dimensions and Principles of Declassification. In: Proc. CSFW 2005. IEEE Computer Society, Los Alamitos (2005)
Smith, G., Volpano, D.: Secure Information Flow in a Multi-threaded Imperative Language. In: Proc. POPL 1998, pp. 355–364. ACM Press, New York (1998)
Takeuchi, K., Honda, K., Kubo, M.: An Interaction-based Language and its Typing System. In: Halatsis, C., Philokyprou, G., Maritsas, D., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398–413. Springer, Heidelberg (1994)
Volpano, D., Irvine, C., Smith, G.: A Sound Type System for Secure Flow Analysis. Journal of Computer Security 4(2,3), 167–187 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Capecchi, S., Castellani, I., Dezani-Ciancaglini, M., Rezk, T. (2010). Session Types for Access and Information Flow Control . In: Gastin, P., Laroussinie, F. (eds) CONCUR 2010 - Concurrency Theory. CONCUR 2010. Lecture Notes in Computer Science, vol 6269. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15375-4_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-15375-4_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15374-7
Online ISBN: 978-3-642-15375-4
eBook Packages: Computer ScienceComputer Science (R0)