Compositional BD Security

Title:	Compositional BD Security
Authors:	Thomas Bauereiss (thomas /at/ bauereiss /dot/ name) and Andrei Popescu
Submission date:	2021-08-16
Abstract:	Building on a previous AFP entry that formalizes the Bounded-Deducibility Security (BD Security) framework [1], we formalize compositionality and transport theorems for information flow security. These results allow lifting BD Security properties from individual components specified as transition systems, to a composition of systems specified as communicating products of transition systems. The underlying ideas of these results are presented in the papers [1] and [2]. The latter paper also describes a major case study where these results have been used: on verifying the CoSMeDis distributed social media platform (itself formalized as an AFP entry that builds on this entry).
BibTeX:	@article{BD_Security_Compositional-AFP, author = {Thomas Bauereiss and Andrei Popescu}, title = {Compositional BD Security}, journal = {Archive of Formal Proofs}, month = aug, year = 2021, note = {\url{https://isa-afp.org/entries/BD_Security_Compositional.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Bounded_Deducibility_Security
Used by:	CoSMeDis
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.