Combining behavioural types with security analysis
Massimo Bartoletti, Ilaria Castellani, Pierre-Malo Deni\'elou,, Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Jovanka Pantovic, Jorge A., P\'erez, Peter Thiemann, Bernardo Toninho, Hugo Torres Vieira
TL;DR
This paper reviews how behavioural types can be used to analyze and enforce security properties in distributed, communicating software systems, emphasizing their role in ensuring correctness and trustworthiness.
Contribution
It provides a unified overview of existing proposals that combine behavioural types with security analysis for distributed systems.
Findings
Behavioural types help specify structured communication behaviors.
They can be used to verify security properties in distributed systems.
The overview highlights the potential of behavioural types in security enforcement.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.