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. CoCon's kernel is implemented in
the Isabelle theorem prover, where we specify and
verify confidentiality properties, as well as complementary safety and
accountability properties. The information flow expressiveness challenges posed
by this development have led to bounded-deducibility (BD) security, a novel
security model and verification method generally applicable to systems
describable as input/output automata.
This paper has
been submitted to the Journal
of Automated Reasoning. A draft of the paper is available here.
A zip archive
with the Isabelle formalization is available here.