TY - JOUR
T1 - Quantitative information flow as safety and liveness hyperproperties
AU - Yasuoka, Hirotoshi
AU - Terauchi, Tachio
N1 - Funding Information:
This work was supported by MEXT KAKENHI 23700026 , 22300005 , 23220001 , and Global COE Program “CERIES.”
Publisher Copyright:
© 2013 Elsevier B.V.
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 -