Publication
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, USA, IEEE, 2017.
Abstract
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.