Combining behavioural types with security analysis

Massimo Bartoletti; Ilaria Castellani; Pierre Malo Deniélou; Mariangiola Dezani-Ciancaglini; Silvia Ghilezan; Jovanka Pantovic; Jorge A. Pérez; Peter Thiemann; Bernardo Toninho; Hugo Torres Vieira

doi:10.1016/j.jlamp.2015.09.003

Combining behavioural types with security analysis

Massimo Bartoletti, Ilaria Castellani, Pierre Malo Deniélou, Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Jovanka Pantovic, Jorge A. Pérez, Peter Thiemann, Bernardo Toninho, Hugo Torres Vieira

Research output: Contribution to journal › Article › peer-review

14 Citations (Scopus)

Abstract

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.

Original language	English
Pages (from-to)	763-780
Number of pages	18
Journal	Journal of Logical and Algebraic Methods in Programming
Volume	84
Issue number	6
DOIs	https://doi.org/10.1016/j.jlamp.2015.09.003
Publication status	Published - 1 Nov 2015

Keywords

DYNAMIC WEB DATA
INFORMATION-FLOW
SESSION TYPES
PI-CALCULUS
CORRESPONDENCE ASSERTIONS
ACCESS-CONTROL
LANGUAGE
NONINTERFERENCE

Access to Document

10.1016/j.jlamp.2015.09.003Licence: CC BY-NC-ND

Cite this

@article{52a57c79a8c6477cac3b2890b4439377,

title = "Combining behavioural types with security analysis",

abstract = "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.",

keywords = "DYNAMIC WEB DATA, INFORMATION-FLOW, SESSION TYPES, PI-CALCULUS, CORRESPONDENCE ASSERTIONS, ACCESS-CONTROL, LANGUAGE, NONINTERFERENCE",

author = "Massimo Bartoletti and Ilaria Castellani and Deni{\'e}lou, {Pierre Malo} and Mariangiola Dezani-Ciancaglini and Silvia Ghilezan and Jovanka Pantovic and P{\'e}rez, {Jorge A.} and Peter Thiemann and Bernardo Toninho and Vieira, {Hugo Torres}",

note = "We acknowledge support from COST Action IC1201 Behavioural Types for Reliable Large-Scale Software Systems (BETTY) and we thank the members of BETTY working group on Security (WG2) for interesting related discussions. We are grateful to the anonymous reviewers for their feedback and many insightful remarks, which greatly helped us to improve the quality of this document.",

year = "2015",

month = nov,

day = "1",

doi = "10.1016/j.jlamp.2015.09.003",

language = "English",

volume = "84",

pages = "763--780",

journal = "Journal of Logical and Algebraic Methods in Programming",

issn = "2352-2216",

publisher = "Elsevier BV",

number = "6",

}

TY - JOUR

T1 - Combining behavioural types with security analysis

AU - Bartoletti, Massimo

AU - Castellani, Ilaria

AU - Deniélou, Pierre Malo

AU - Dezani-Ciancaglini, Mariangiola

AU - Ghilezan, Silvia

AU - Pantovic, Jovanka

AU - Pérez, Jorge A.

AU - Thiemann, Peter

AU - Toninho, Bernardo

AU - Vieira, Hugo Torres

N1 - We acknowledge support from COST Action IC1201 Behavioural Types for Reliable Large-Scale Software Systems (BETTY) and we thank the members of BETTY working group on Security (WG2) for interesting related discussions. We are grateful to the anonymous reviewers for their feedback and many insightful remarks, which greatly helped us to improve the quality of this document.

PY - 2015/11/1

Y1 - 2015/11/1

N2 - 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.

AB - 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.

KW - DYNAMIC WEB DATA

KW - INFORMATION-FLOW

KW - SESSION TYPES

KW - PI-CALCULUS

KW - CORRESPONDENCE ASSERTIONS

KW - ACCESS-CONTROL

KW - LANGUAGE

KW - NONINTERFERENCE

UR - http://www.scopus.com/inward/record.url?scp=84997755144&partnerID=8YFLogxK

U2 - 10.1016/j.jlamp.2015.09.003

DO - 10.1016/j.jlamp.2015.09.003

M3 - Article

AN - SCOPUS:84997755144

SN - 2352-2216

VL - 84

SP - 763

EP - 780

JO - Journal of Logical and Algebraic Methods in Programming

JF - Journal of Logical and Algebraic Methods in Programming

IS - 6

ER -

Combining behavioural types with security analysis

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this