CoSMeDis - A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees
Explore a 19-minute IEEE conference talk on CoSMeDis, a distributed social media platform with formally verified confidentiality guarantees. Delve into the design, implementation, and information flow verification of this system, which allows users to post content and establish friendships across multiple interconnected nodes. Learn about the platform's kernel, verified in Isabelle/HOL and extracted as Scala code, and discover the formalized framework for composing information flow security guarantees in distributed systems. Examine the confidentiality properties for posts, friendship requests, and friendship status, and gain insights into dynamic declassification policies. Presented by Thomas Bauereiß from the German Research Center for Artificial Intelligence at the 2017 IEEE Symposium on Security & Privacy, this talk covers motivation, functionality, architecture, verification, and concludes with a Q&A session.