Compositional BD Security

Thomas Bauereiss 📧 and Andrei Popescu 🌐

August 16, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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

License

BSD License

Topics

Session BD_Security_Compositional