CoCon: A Conference Management System with Formally Verified Document Confidentiality

摘要

We present a case study in formally verified security for realistic systems: the information flow security verification of the functional kernel of a web application, the CoCon conference management system. We use the Isabelle theorem prover to specify and verify fine-grained confidentiality properties, as well as complementary safety and "traceback" properties. The challenges posed by this development in terms of expressiveness have led tobounded-deducibility security, a novel security model and verification method generally applicable to systems describable as input/output automata.