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 条
  • [21] Quantitative Information Flow as Network Flow Capacity
    McCamant, Stephen
    Ernst, Michael D.
    PLDI'08: PROCEEDINGS OF THE 2008 SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN & IMPLEMENTATION, 2008, : 193 - 205
  • [22] Safety, Closure, and the Flow of Information
    Jens Kipper
    Erkenntnis, 2016, 81 : 1109 - 1126
  • [23] Safety, Closure, and the Flow of Information
    Kipper, Jens
    ERKENNTNIS, 2016, 81 (05) : 1109 - 1126
  • [24] A Safety and Liveness Theory for Total Reversibility
    Mezzina, Claudio Antares
    Koutavas, Vasileios
    PROCEEDINGS 11TH 2017 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE), 2017, : 103 - 110
  • [25] Safety and liveness in concurrent pointer programs
    Distefano, Dino
    Katoen, Joost-Pieter
    Rensink, Arend
    FORMAL METHODS FOR COMPONENTS AND OBJECTS, 2006, 4111 : 280 - 312
  • [26] PRESERVING LIVENESS - COMMENTS ON SAFETY AND LIVENESS FROM A METHODOLOGICAL POINT-OF-VIEW
    ABADI, M
    ALPERN, B
    APT, KR
    FRANCEZ, N
    KATZ, S
    LAMPORT, L
    SCHNEIDER, FB
    INFORMATION PROCESSING LETTERS, 1991, 40 (03) : 141 - 142
  • [27] Spanning the Spectrum from Safety to Liveness
    Faran, Rachel
    Kupferman, Orna
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015, 2015, 9364 : 183 - 200
  • [28] Spanning the spectrum from safety to liveness
    Faran, Rachel
    Kupferman, Orna
    ACTA INFORMATICA, 2018, 55 (08) : 703 - 732
  • [29] Spanning the spectrum from safety to liveness
    Rachel Faran
    Orna Kupferman
    Acta Informatica, 2018, 55 : 703 - 732
  • [30] Program algebra for quantitative information flow
    McIver, A. K.
    Morgan, C. C.
    Rabehaja, T.
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2019, 106 : 55 - 77
12345