CoCon: A Conference Management System with Formally Verified Document Confidentiality
2020
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 to bounded-deducibility security, a novel security model and verification method generally applicable to systems describable as input/output automata.
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
77
References
0
Citations
NaN
KQI