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 条
  • [41] Studying document information flow on the information safety problems
    Fedorenko, Vyacheslav
    Mishurov, Nikolay
    Demidov, Dmitry
    Chavykin, Yury
    NAUCHNYE I TEKHNICHESKIE BIBLIOTEKI-SCIENTIFIC AND TECHNICAL LIBRARIES, 2019, (06): : 51 - 70
  • [42] Information Flow Safety in Multiparty Sessions
    Capecchi, Sara
    Castellani, Ilaria
    Dezani-Ciancaglini, Mariangiola
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (64): : 16 - 30
  • [43] Secure Information Flow as a Safety Property
    Boudol, Gerard
    FORMAL ASPECTS IN SECURITY AND TRUST, 2009, 5491 : 20 - 34
  • [44] PRESERVING LIVENESS - COMMENTS ON SAFETY AND LIVENESS FROM A METHODOLOGICAL POINT-OF-VIEW - REPLY
    DEDERICHS, F
    WEBER, R
    INFORMATION PROCESSING LETTERS, 1991, 40 (03) : 143 - 143
  • [45] Secure information flow as a safety problem
    Terauchi, T
    Aiken, A
    STATIC ANALYSIS, PROCEEDINGS, 2005, 3672 : 352 - 367
  • [46] Information flow safety in multiparty sessions
    Capecchi, Sara
    Castellani, Ilaria
    Dezani-Ciancaglini, Mariangiola
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2016, 26 (08) : 1352 - 1394
  • [47] VERIFYING LIVENESS PROPERTIES BY VERIFYING SAFETY PROPERTIES
    BURCH, JR
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 531 : 224 - 232
  • [48] Intuitionistic LTL and a new characterization of safety and liveness
    Maier, P
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2004, 3210 : 295 - 309
  • [49] Dolmen: FPGA Swarm for Safety and Liveness Verification
    Fournier, Emilien
    Teodorov, Ciprian
    Lagadec, Loic
    PROCEEDINGS OF THE 2022 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE 2022), 2022, : 1425 - 1430
  • [50] Copying safety and liveness properties of computational artefacts
    Angius, Nicola
    Primiero, Giuseppe
    JOURNAL OF LOGIC AND COMPUTATION, 2023, 33 (05) : 1089 - 1117
12345