CoSMed: A confidentiality-verified social media platform

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.


This entry contains the confidentiality verification of the (functional kernel of) the CoSMed social media platform. The confidentiality properties are formalized as instances of BD Security [1, 2]. An innovation in the deployment of BD Security compared to previous work is the use of dynamic declassification triggers, incorporated as part of inductive bounds, for providing stronger guarantees that account for the repeated opening and closing of access windows. To further strengthen the confidentiality guarantees, we also prove "traceback" properties about the accessibility decisions affecting the information managed by the system.


BSD License


Session CoSMed