CoCon: A Non-Leaking Conference System

VCLA hosted a talk by Ondřej Kunčar

ABSTRACT

In our project we are working on a framework that provides holistic security guarantees for web-based systems in which information flows heavily but not all flows should be allowed. As a case study we developed CoCon, a conference management system with verified document confidentiality. In my talk, I will start with a demo of CoCon, show which properties of the system we verified in the interactive theorem prover Isabelle and explain how we technically capture the intuitive idea that an attacker cannot learn any secrets of the system. A discussion of limitations of our approach will follow together with a summary of our experience with deployment of CoCon for real-life conferences. At the end, I will shortly mention future work.