Quantitative information flow as safety and liveness hyperproperties

Hirotoshi Yasuoka; Tachio Terauchi

doi:10.1016/j.tcs.2013.07.031

Quantitative information flow as safety and liveness hyperproperties

Hirotoshi Yasuoka, Tachio Terauchi

Research output: Contribution to journal › Article › peer-review

16 Citations (Scopus)

Abstract

We employ Clarkson and Schneider's "hyperproperties" to classify various verification problems of quantitative information flow. The results of this paper unify and extend the previous results on the hardness of checking and inferring quantitative information flow. In particular, we identify a subclass of liveness hyperproperties, which we call ". k-observable hyperproperties", that can be checked relative to a reachability oracle via self composition.

Original language	English
Pages (from-to)	167-182
Number of pages	16
Journal	Theoretical Computer Science
Volume	538
Issue number	C
DOIs	https://doi.org/10.1016/j.tcs.2013.07.031
Publication status	Published - 2014
Externally published	Yes

Keywords

Hyperproperties
Quantitative information flow
Verification

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1016/j.tcs.2013.07.031

Fingerprint Dive into the research topics of 'Quantitative information flow as safety and liveness hyperproperties'. Together they form a unique fingerprint.

Cite this

@article{4e7f8ecdaedc4c1dbfbe4ede054528ca,

title = "Quantitative information flow as safety and liveness hyperproperties",

abstract = "We employ Clarkson and Schneider's {"}hyperproperties{"} to classify various verification problems of quantitative information flow. The results of this paper unify and extend the previous results on the hardness of checking and inferring quantitative information flow. In particular, we identify a subclass of liveness hyperproperties, which we call {"}. k-observable hyperproperties{"}, that can be checked relative to a reachability oracle via self composition.",

keywords = "Hyperproperties, Quantitative information flow, Verification",

author = "Hirotoshi Yasuoka and Tachio Terauchi",

year = "2014",

doi = "10.1016/j.tcs.2013.07.031",

language = "English",

volume = "538",

pages = "167--182",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier",

number = "C",

}

TY - JOUR

T1 - Quantitative information flow as safety and liveness hyperproperties

AU - Yasuoka, Hirotoshi

AU - Terauchi, Tachio

PY - 2014

Y1 - 2014

N2 - We employ Clarkson and Schneider's "hyperproperties" to classify various verification problems of quantitative information flow. The results of this paper unify and extend the previous results on the hardness of checking and inferring quantitative information flow. In particular, we identify a subclass of liveness hyperproperties, which we call ". k-observable hyperproperties", that can be checked relative to a reachability oracle via self composition.

AB - We employ Clarkson and Schneider's "hyperproperties" to classify various verification problems of quantitative information flow. The results of this paper unify and extend the previous results on the hardness of checking and inferring quantitative information flow. In particular, we identify a subclass of liveness hyperproperties, which we call ". k-observable hyperproperties", that can be checked relative to a reachability oracle via self composition.

KW - Hyperproperties

KW - Quantitative information flow

KW - Verification

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

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

U2 - 10.1016/j.tcs.2013.07.031

DO - 10.1016/j.tcs.2013.07.031

M3 - Article

AN - SCOPUS:84926279387

VL - 538

SP - 167

EP - 182

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - C

ER -