Publication
CoSMed: A Confidentiality-Verified Social Media Platform
Thomas Bauereiß; Armando Pesenti Gritti; Andrei Popescu; Franco Raimondi
In: Jasmin Christian Blanchette; Stephan Merz (Hrsg.). Interactive Theorem Proving. International Conference on Interactive Theorem Proving (ITP-2016), 7th, August 22-27, Nancy, France, Pages 87-106, LNCS, Vol. 9807, Springer, 8/2016.
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.