Bounded-Deducibility Security (Invited Paper)

Andrei Popescu; Thomas Bauereiss; Peter Lammich

doi:10.4230/LIPIcs.ITP.2021.3

Bounded-Deducibility Security (Invited Paper)

Andrei Popescu, Thomas Bauereiss, Peter Lammich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

44 Downloads (Pure)

Abstract

We describe Bounded-Deducibility (BD) security, an expressive framework for the specification and verification of information-flow security. The framework grew by confronting concrete challenges of specifying and verifying fine-grained confidentiality properties in some realistic web-based systems. The concepts and theorems that constitute this framework have an eventful history of such "confrontations", often involving trial and error, which are reported in previous papers. This paper is the first to focus on the framework itself rather than the case studies, gathering in one place all the abstract results about BD security.

Original language	English
Title of host publication	12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)
Editors	Liron Cohen, Cezary Kaliszyk
Publisher	Dagstuhl
Pages	3:1-3:20
DOIs	https://doi.org/10.4230/LIPIcs.ITP.2021.3
Publication status	Published - 21 Jun 2021
Event	12th International Conference on Interactive Theorem Proving, ITP 2021 - Online Conference Duration: 29 Jun 2021 → 1 Jul 2021 Conference number: 12

Conference

Conference	12th International Conference on Interactive Theorem Proving, ITP 2021
Abbreviated title	ITP 2021
City	Online Conference
Period	29/06/21 → 1/07/21

Access to Document

10.4230/LIPIcs.ITP.2021.3Licence: CC BY

LIPIcs-ITP-2021-3Final published version, 828 KBLicence: CC BY

Cite this

@inproceedings{efe99a2fff3d43ceae31b735f780fbc3,

title = "Bounded-Deducibility Security (Invited Paper)",

abstract = "We describe Bounded-Deducibility (BD) security, an expressive framework for the specification and verification of information-flow security. The framework grew by confronting concrete challenges of specifying and verifying fine-grained confidentiality properties in some realistic web-based systems. The concepts and theorems that constitute this framework have an eventful history of such {"}confrontations{"}, often involving trial and error, which are reported in previous papers. This paper is the first to focus on the framework itself rather than the case studies, gathering in one place all the abstract results about BD security.",

author = "Andrei Popescu and Thomas Bauereiss and Peter Lammich",

year = "2021",

month = jun,

day = "21",

doi = "10.4230/LIPIcs.ITP.2021.3",

language = "English",

pages = "3:1--3:20",

editor = "Liron Cohen and Cezary Kaliszyk",

booktitle = "12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)",

publisher = "Dagstuhl",

address = "Germany",

note = "12th International Conference on Interactive Theorem Proving, ITP 2021, ITP 2021 ; Conference date: 29-06-2021 Through 01-07-2021",

}

Popescu, A, Bauereiss, T & Lammich, P 2021, Bounded-Deducibility Security (Invited Paper). in L Cohen & C Kaliszyk (eds), 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference). Dagstuhl, pp. 3:1-3:20, 12th International Conference on Interactive Theorem Proving, ITP 2021, Online Conference, 29/06/21. https://doi.org/10.4230/LIPIcs.ITP.2021.3

Bounded-Deducibility Security (Invited Paper). / Popescu, Andrei; Bauereiss, Thomas; Lammich, Peter.

12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference). ed. / Liron Cohen; Cezary Kaliszyk. Dagstuhl, 2021. p. 3:1-3:20.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Bounded-Deducibility Security (Invited Paper)

AU - Popescu, Andrei

AU - Bauereiss, Thomas

AU - Lammich, Peter

N1 - Conference code: 12

PY - 2021/6/21

Y1 - 2021/6/21

N2 - We describe Bounded-Deducibility (BD) security, an expressive framework for the specification and verification of information-flow security. The framework grew by confronting concrete challenges of specifying and verifying fine-grained confidentiality properties in some realistic web-based systems. The concepts and theorems that constitute this framework have an eventful history of such "confrontations", often involving trial and error, which are reported in previous papers. This paper is the first to focus on the framework itself rather than the case studies, gathering in one place all the abstract results about BD security.

AB - We describe Bounded-Deducibility (BD) security, an expressive framework for the specification and verification of information-flow security. The framework grew by confronting concrete challenges of specifying and verifying fine-grained confidentiality properties in some realistic web-based systems. The concepts and theorems that constitute this framework have an eventful history of such "confrontations", often involving trial and error, which are reported in previous papers. This paper is the first to focus on the framework itself rather than the case studies, gathering in one place all the abstract results about BD security.

U2 - 10.4230/LIPIcs.ITP.2021.3

DO - 10.4230/LIPIcs.ITP.2021.3

M3 - Conference contribution

SP - 3:1-3:20

BT - 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)

A2 - Cohen, Liron

A2 - Kaliszyk, Cezary

PB - Dagstuhl

T2 - 12th International Conference on Interactive Theorem Proving, ITP 2021

Y2 - 29 June 2021 through 1 July 2021

ER -

Bounded-Deducibility Security (Invited Paper)

Abstract

Conference

Access to Document

Fingerprint

Cite this