Quantitative Information Flow as Safety and Liveness Hyperproperties

被引：0
|
作者：
Yasuoka, Hirotoshi [1 ]
Terauchi, Tachio [2 ]
机构：
[1] Tohoku Univ, Sendai, Miyagi, Japan
[2] Nagoya Univ, Nagoya, Aichi, Japan
来源：
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2012年 / 85期
关键词：
D O I：
10.4204/EPTCS.85.6
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页码：77 / 91
页数：15
相关论文
共 50 条
  • [1] Quantitative information flow as safety and liveness hyperproperties
    Yasuoka, Hirotoshi
    Terauchi, Tachio
    THEORETICAL COMPUTER SCIENCE, 2014, 538 : 167 - 182
  • [2] Quantitative Safety and Liveness
    Henzinger, Thomas A.
    Mazzocchi, Nicolas
    Sarac, N. Ege
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, FOSSACS 2023, 2023, 13992 : 349 - 370
  • [3] Model Checking Quantitative Hyperproperties
    Finkbeiner, Bernd
    Hahn, Christopher
    Torfah, Hazem
    COMPUTER AIDED VERIFICATION (CAV 2018), PT I, 2018, 10981 : 144 - 163
  • [4] Canonical Representations of k-Safety Hyperproperties
    Finkbeiner, Bernd
    Haas, Lennart
    Torfah, Hazem
    2019 IEEE 32ND COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2019), 2019, : 17 - 31
  • [5] RECOGNIZING SAFETY AND LIVENESS
    ALPERN, B
    SCHNEIDER, FB
    DISTRIBUTED COMPUTING, 1987, 2 (03) : 117 - 126
  • [6] Runtime Verification of k-Safety Hyperproperties in HyperLTL
    Agrawal, Shreya
    Bonakdarpour, Borzoo
    2016 IEEE 29TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2016), 2016, : 239 - 252
  • [7] Testing liveness properties: Approximating liveness properties by safety properties
    Ultes-Nitsche, U
    St James, S
    FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS, 2001, 69 : 369 - 376
  • [8] Verification of Quantitative Hyperproperties Using Trace Enumeration Relations
    Sahai, Shubham
    Subramanyan, Pramod
    Sinha, Rohit
    COMPUTER AIDED VERIFICATION (CAV 2020), PT I, 2020, 12224 : 201 - 224
  • [9] Abstraction for safety, induction for liveness
    Calder, M
    ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, 2004, 3116 : 20 - 20
  • [10] Safety and liveness in intelligent intersections
    Kowshik, Hemant
    Caveney, Derek
    Kumar, P. R.
    HYBRID SYSTEMS: COMPUTATION AND CONTROL, 2008, 4981 : 301 - +
12345