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