Abstract
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.
Original language | English |
---|---|
Pages (from-to) | 321-356 |
Number of pages | 36 |
Journal | Journal of automated reasoning |
Volume | 65 |
Issue number | 2 |
Early online date | 16 Jul 2020 |
DOIs | |
Publication status | Published - Feb 2021 |
Externally published | Yes |
Keywords
- Conference management system
- Confidentiality
- Information-flow security
- Isabelle/HOL
- Theorem proving
- Unwinding proof method