CoSMed: A Confidentiality-Verified Social Media Platform


Type
Article
Change log
Authors
Bauereiß, Thomas 
Pesenti Gritti, Armando 
Raimondi, Franco 
Abstract

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.

Description
Keywords
46 Information and Computing Sciences, 4604 Cybersecurity and Privacy
Journal Title
Journal of Automated Reasoning
Conference Name
Journal ISSN
0168-7433
1573-0670
Volume Title
61
Publisher
Springer Science and Business Media LLC
Sponsorship
Engineering and Physical Sciences Research Council (EP/K008528/1)