CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees

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

In: 2017 IEEE Symposium on Security and Privacy. IEEE Symposium on Security and Privacy (SP-17) May 22-24 San Jose CA United States IEEE 2017.


We present the design, implementation and information flow verification of CoSMeDis, a distributed social media platform. The system consists of an arbitrary number of communicating nodes, deployable at different locations over the Internet. Its registered users can post content and establish intra-node and inter-node friendships, used to regulate access control over the posts. The system's kernel has been verified in the proof assistant Isabelle/HOL and automatically extracted as Scala code. We formalized a framework for composing a class of information flow security guarantees in a distributed system, applicable to input/output automata. We instantiated this framework to confidentiality properties for CoSMeDis's sources of information: posts, friendship requests, and friendship status.


CoSMeDis.pdf (pdf, 254 KB )

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