CoCon: A Conference Management System with Formally Verified Document Confidentiality

Andrei Popescu*, Peter Lammich, Ping Hou

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

3 Citations (Scopus)
48 Downloads (Pure)

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 languageEnglish
Pages (from-to)321-356
Number of pages36
JournalJournal of automated reasoning
Volume65
Issue number2
Early online date16 Jul 2020
DOIs
Publication statusPublished - Feb 2021
Externally publishedYes

Keywords

  • Conference management system
  • Confidentiality
  • Information-flow security
  • Isabelle/HOL
  • Theorem proving
  • Unwinding proof method

Fingerprint

Dive into the research topics of 'CoCon: A Conference Management System with Formally Verified Document Confidentiality'. Together they form a unique fingerprint.

Cite this