Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-25T16:32:52.735Z Has data issue: false hasContentIssue false
  • English
  • Français

Information flow safety in multiparty sessions†

Published online by Cambridge University Press:  02 January 2015

SARA CAPECCHI ,
ILARIA CASTELLANI  and
MARIANGIOLA DEZANI-CIANCAGLINI
SARA CAPECCHI
Affiliation:
Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149 Torino, Italy Email: [email protected]
ILARIA CASTELLANI
Affiliation:
INRIA, 2004 route des Lucioles, 06902 Sophia Antipolis, France Email: [email protected]
MARIANGIOLA DEZANI-CIANCAGLINI
Affiliation:
Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149 Torino, Italy Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We consider a calculus for multiparty sessions enriched with security levels for messages. We propose a monitored semantics for this calculus, which blocks the execution of processes as soon as they attempt to leak information. We illustrate the use of this semantics with various examples, and show that the induced safety property is compositional and that it is strictly included between a typability property and a security property proposed for an extended calculus in previous work.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 26 , Special Issue 8: Special Issue: Express'11 , December 2016 , pp. 1352 - 1394
Copyright
Copyright © Cambridge University Press 2015 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

†

Work partially funded by the ANR-08-EMER-010 grant PARTOUT, by the EU Collaborative project ASCENS 257414, by the ICT COST Action IC1201 BETTY, by the MIUR PRIN Project CINA Prot. 2010LHT4KM and by the Torino University/Compagnia San Paolo Project SALT.

References

Askarov, A. and Sabelfeld, A. (2009) Tight enforcement of information-release policies for dynamic languages. In: CSF'09: Proceedings of 22nd IEEE Computer Security Foundations Symposium 43–59.Google Scholar
Bettini, L., Coppo, M., D'Antoni, L., De Luca, M., Dezani-Ciancaglini, M. and Yoshida, N. (2008) Global progress in dynamically interleaved multiparty sessions. In: Proceedings of CONCUR'08. Springer Lecture Notes in Computer Science 5201 418–433.Google Scholar
Bhargavan, K., Corin, R., Deniélou, P. M., Fournet, C. and Leifer, J. J. (2009) Cryptographic protocol synthesis and verification for multiparty sessions. In: CSF'09: Proceedings of 2009 22nd IEEE Computer Security Foundations Symposium 124–140.Google Scholar
Bossi, A., Focardi, R., Piazza, C. and Rossi, S. (2004) Verifying persistent security properties. Computer Languages, Systems & Structures 30 (3–4) 231–258.Google Scholar
Boudol, G. (2009) Secure information flow as a safety property. In: Proceedings of FAST'08. Springer Lecture Notes in Computer Science 5491 20–34.CrossRefGoogle Scholar
Capecchi, S., Castellani, I. and Dezani-Ciancaglini, M. (2011) Information flow safety in multiparty sessions. In: Proceedings of EXPRESS'11. Electronic Proceedings in Theoretical Computer Science 64 16–30.Google Scholar
Capecchi, S., Castellani, I. and Dezani-Ciancaglini, M. (2014) Typing access control and secure information flow in sessions. Information and Computation 238 68–105.CrossRefGoogle Scholar
Capecchi, S., Castellani, I., Dezani Ciancaglini, M. and Rezk, T. (2010) Session types for access and information flow control. In: Proceedings of CONCUR'10. Springer Lecture Notes in Computer Science 6269 237–252.CrossRefGoogle Scholar
Coppo, M., Dezani-Ciancaglini, M., Yoshida, N. and Padovani, L. (2014) Global progress for dynamically interleaved multiparty sessions. Mathematical Structures in Computer Science. to appear.CrossRefGoogle Scholar
De Nicola, R. and Hennessy, M. (1983) Testing equivalence for processes. In: Proceedings of ICALP'83. Springer Lecture Notes in Computer Science 154 548–560.Google Scholar
Dezani-Ciancaglini, M. and de' Liguoro, U. (2010) Sessions and session types: An overview. In: Proceedings of WS-FM'09. Springer Lecture Notes in Computer Science 6194 1–28.Google Scholar
Guernic, G. L., Banerjee, A., Jensen, T. and Schmidt, D. A. (2007) Automata-based confidentiality monitoring. In: Proceedings of ASIAN'06. Springer Lecture Notes in Computer Science 4435 75–89.Google Scholar
Honda, K. (1993) Types for dyadic interaction. In: Proceedings of CONCUR'93. Springer Lecture Notes in Computer Science 715 509–523.CrossRefGoogle Scholar
Honda, K., Vasconcelos, V. T. and Kubo, M. (1998) Language primitives and type disciplines for structured communication-based programming. In: Proceedings of ESOP'98. Springer Lecture Notes in Computer Science 1381 22–138.Google Scholar
Honda, K., Yoshida, N. and Carbone, M. (2008) Multiparty asynchronous session types. In: POPL'08: Proceedings of 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages 273–284.CrossRefGoogle Scholar
Milner, R. (1999) Communicating and Mobile Systems: The Pi-Calculus, Cambridge University Press.Google Scholar
Myers, A. C. and Liskov, B. (2000) Protecting privacy using the decentralized label model. ACM Transactions on Software Engineering and Methodology 9 410–442.CrossRefGoogle Scholar
Planul, J., Corin, R. and Fournet, C. (2009) Secure enforcement for global process specifications. In: Proceedings of CONCUR'09. Springer Lecture Notes in Computer Science 5710 511–526.Google Scholar
Sabelfeld, A. and Russo, A. (2010) From dynamic to static and back: Riding the roller coaster of information-flow control research. In: Proceedings of PSI'06. Springer Lecture Notes in Computer Science 5947 352–365.Google Scholar
Takeuchi, K., Honda, K. and Kubo, M. (1994) An interaction-based language and its typing system. In: Proceedings of PARLE'94. Springer Lecture Notes in Computer Science 817 398–413.CrossRefGoogle Scholar
Zheng, L. and Myers, A. C. (2007) Dynamic security labels and static information flow control. International Journal of Information Security 6 67–84.Google Scholar