Publikation

CoSMed: A Confidentiality-Verified Social Media Platform

Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi

In: Journal of Automated Reasoning (JAR) 61 1-4 Seiten 113-139 Springer Heidelberg 12/2017.

Abstrakt

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.

Projekte

Weitere Links

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence