Quantitative information flow as safety and liveness hyperproperties

Hirotoshi Yasuoka, Tachio Terauchi

Research output: Contribution to journalArticle

3 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 languageEnglish
Pages (from-to)77-91
Number of pages15
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume85
DOIs
Publication statusPublished - 2012 Jul 3
Externally publishedYes

Fingerprint

Hardness
Chemical analysis

ASJC Scopus subject areas

  • Software

Cite this

Quantitative information flow as safety and liveness hyperproperties. / Yasuoka, Hirotoshi; Terauchi, Tachio.

In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 85, 03.07.2012, p. 77-91.

Research output: Contribution to journalArticle

@article{9882ce8064534405a561c7015f33ecd0,
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.",
author = "Hirotoshi Yasuoka and Tachio Terauchi",
year = "2012",
month = "7",
day = "3",
doi = "10.4204/EPTCS.85.6",
language = "English",
volume = "85",
pages = "77--91",
journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",
issn = "2075-2180",
publisher = "Open Publishing Association",

}

TY - JOUR

T1 - Quantitative information flow as safety and liveness hyperproperties

AU - Yasuoka, Hirotoshi

AU - Terauchi, Tachio

PY - 2012/7/3

Y1 - 2012/7/3

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.

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

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

U2 - 10.4204/EPTCS.85.6

DO - 10.4204/EPTCS.85.6

M3 - Article

AN - SCOPUS:84880196090

VL - 85

SP - 77

EP - 91

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

SN - 2075-2180

ER -