CoSMed: A confidentiality-verified social media platform

Title:	CoSMed: A confidentiality-verified social media platform
Authors:	Thomas Bauereiss (thomas /at/ bauereiss /dot/ name) and Andrei Popescu
Submission date:	2021-08-16
Abstract:	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.
BibTeX:	@article{CoSMed-AFP, author = {Thomas Bauereiss and Andrei Popescu}, title = {CoSMed: A confidentiality-verified social media platform}, journal = {Archive of Formal Proofs}, month = aug, year = 2021, note = {\url{https://isa-afp.org/entries/CoSMed.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Bounded_Deducibility_Security, Fresh_Identifiers
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.