CoCon: A Conference Management System with Formally Verified Document Confidentiality

Andrei Popescu; Peter Lammich; Ping Hou

doi:10.1007/s10817-020-09566-9

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 journal › Article › Academic › peer-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 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	https://doi.org/10.1007/s10817-020-09566-9
Publication status	Published - Feb 2021
Externally published	Yes

Keywords

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

Access to Document

10.1007/s10817-020-09566-9Licence: CC BY

ArticleFinal published version, 1.19 MBLicence: CC BY

Cite this

@article{cf04eeda39664e9a8f5afbcd38cfdb5f,

title = "CoCon: A Conference Management System with Formally Verified Document Confidentiality",

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.",

keywords = "Conference management system, Confidentiality, Information-flow security, Isabelle/HOL, Theorem proving, Unwinding proof method",

author = "Andrei Popescu and Peter Lammich and Ping Hou",

note = "Publisher Copyright: {\textcopyright} 2020, The Author(s).",

year = "2021",

month = feb,

doi = "10.1007/s10817-020-09566-9",

language = "English",

volume = "65",

pages = "321--356",

journal = "Journal of automated reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "2",

}

TY - JOUR

T1 - CoCon

T2 - A Conference Management System with Formally Verified Document Confidentiality

AU - Popescu, Andrei

AU - Lammich, Peter

AU - Hou, Ping

PY - 2021/2

Y1 - 2021/2

N2 - 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.

AB - 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.

KW - Conference management system

KW - Confidentiality

KW - Information-flow security

KW - Isabelle/HOL

KW - Theorem proving

KW - Unwinding proof method

UR - http://www.scopus.com/inward/record.url?scp=85087950805&partnerID=8YFLogxK

U2 - 10.1007/s10817-020-09566-9

DO - 10.1007/s10817-020-09566-9

M3 - Article

SN - 0168-7433

VL - 65

SP - 321

EP - 356

JO - Journal of automated reasoning

JF - Journal of automated reasoning

IS - 2

ER -

CoCon: A Conference Management System with Formally Verified Document Confidentiality

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this