Combining behavioural types with security analysis

Massimo Bartoletti (1) , Ilaria Castellani (2) , Pierre-Malo Deniélou (3, 4) , Mariangiola Dezani-Ciancaglini (5) , Silvia Ghilezan (6) , Jovanka Pantovic (6) , Jorge A. Pérez (7) , Peter Thiemann (8) , Bernardo Toninho (9) , Hugo Torres Vieira (10)

1 Dipartimento di Matematica e Informatica
2 INDES - Secure Diffuse Programming
3 RHUL - Royal Holloway [University of London]
4 Google Inc
5 Dipartimento di Informatica [Torino]
6 Faculty of Technical Sciences [Novi Sad]
7 University of Groningen [Groningen]
8 University of Freiburg [Freiburg]
9 Department of Computing [London]
10 IMT Institute for Advanced Studies [Lucca]

Today's software systems are highly distributed and interconnected, and they increasingly rely on communication to achieve their goals; due to their societal importance, security and trustworthiness are crucial aspects for the correctness of these systems. Behavioural types, which extend data types by describing also the structured behaviour of programs, are a widely studied approach to the enforcement of correctness properties in communicating systems. This paper offers a unified overview of proposals based on behavioural types which are aimed at the analysis of security properties.

Mots clés: Communication-centred computing; Distributed systems; Behavioural types; Session types; Security properties

Domaines: Informatique ubiquitaire; Calcul parallèle, distribué et partagé [cs.DC]

Massimo Bartoletti, Ilaria Castellani, Pierre-Malo Deniélou, Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, et al.. Combining behavioural types with security analysis. Journal of Logical and Algebraic Methods in Programming, 2015, pp.18. ⟨10.1016/j.jlamp.2015.09.003⟩. ⟨hal-01213201⟩