CoSMed: A Confidentiality-Verified Social Media Platform
Pesenti Gritti, Armando
Journal of Automated Reasoning
MetadataShow full item record
Bauereiss, T., Pesenti Gritti, A., Popescu, A., & Raimondi, F. (2018). CoSMed: A Confidentiality-Verified Social Media Platform. Journal of Automated Reasoning, 61 (1-4), 113-139. https://doi.org/10.1007/s10817-017-9443-3
This paper describes progress with our agenda of formal verification of information flow security for realistic systems. We present CoSMed, a social media platform with verified document confidentiality. The system’s kernel is implemented and verified in the proof assistant Isabelle/HOL. For verification, we employ the framework of Bounded-Deducibility (BD) Security, previously introduced for the conference system CoCon. CoSMed is a second major case study in this framework. For CoSMed, the static topology of declassification bounds and triggers that characterized previous instances of BD Security has to give way to a dynamic integration of the triggers as part of the bounds. We also show that, from a theoretical viewpoint, the removal of triggers from the notion of BD Security does not restrict its expressiveness.
External DOI: https://doi.org/10.1007/s10817-017-9443-3
This record's URL: https://www.repository.cam.ac.uk/handle/1810/271844