Provably correct runtime enforcement of non-interference properties

被引:0
|
作者
Venkatakrishnan, V. N. [1 ]
Xu, Wei [2 ]
DuVarney, Daniel C. [2 ]
Sekar, R. [2 ]
机构
[1] Univ Illinois, Dept Comp Sci, Chicago, IL 60607 USA
[2] SUNY Stony Brook, Dept Comp Sci, Stony Brook, NY USA
来源
INFORMATION AND COMMUNICATIONS SECURITY, PROCEEDINGS | 2006年 / 4307卷
关键词
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Non-interference has become the standard criterion for ensuring confidentiality of sensitive data in the information flow literature. However, application of non-interference to practical software systems has been limited. This is partly due to the imprecision that is inherent in static analyses that have formed the basis of previous non-interference based techniques. Runtime approaches can be significantly more accurate than static analysis, and have often been more successful in practice. However, they can only reason about explicit information flows that take place via assignments in a program. Implicit flows that take place without involving assignments, and can be inferred from the structure and/or semantics of the program, are missed by runtime techniques. This paper seeks to bridge the gap between the accuracy provided by runtime techniques and the completeness provided by static analysis techniques. In particular, we develop a hybrid technique that relies primarily on runtime information-flow tracking, but augments it with static analysis to reason about implicit flows that arise due to unexecuted paths in a program. We prove that the resulting technique preserves non-interference, while providing some of the traditional benefits of dynamic analysis such as improved accuracy.
引用
收藏
页码:332 / +
页数:3
相关论文
共 50 条
  • [41] A decidable notion of timed non-interference
    Barbuti, R
    Tesei, L
    FUNDAMENTA INFORMATICAE, 2003, 54 (2-3) : 137 - 150
  • [42] The Myth of Academics' Non-interference in Legislatures
    Zelizer, Adam
    POLITICAL STUDIES REVIEW, 2022, 20 (02) : 228 - 235
  • [43] Non-Interference for Deterministic Interactive Programs
    Clark, David
    Hunt, Sebastian
    FORMAL ASPECTS IN SECURITY AND TRUST, 2009, 5491 : 50 - +
  • [44] Class-level Non-Interference
    Damiano Zanardini
    New Generation Computing, 2012, 30 : 241 - 270
  • [45] China Debates the Non-Interference Principle
    Zheng, Chen
    CHINESE JOURNAL OF INTERNATIONAL POLITICS, 2016, 9 (03): : 349 - 374
  • [46] Intransitive non-interference for cryptographic purposes
    Backes, M
    Pfitzmann, B
    2003 IEEE SYMPOSIUM ON SECURITY AND PRIVACY, PROCEEDINGS, 2003, : 140 - 152
  • [47] A notion of non-interference for timed automata
    Barbuti, R
    De Francesco, N
    Santone, A
    Tesei, L
    FUNDAMENTA INFORMATICAE, 2002, 51 (1-2) : 1 - 11
  • [48] DeFi Composability as MEV Non-interference
    Bartoletti, Massimo
    Marchesin, Riccardo
    Zunino, Roberto
    FINANCIAL CRYPTOGRAPHY AND DATA SECURITY, FC 2024, PT II, 2025, 14745 : 369 - 387
  • [49] Runtime enforcement of timed properties revisited
    Pinisetty, Srinivas
    Falcone, Ylies
    Jeron, Thierry
    Marchand, Herve
    Rollet, Antoine
    Timo, Omer Nguena
    FORMAL METHODS IN SYSTEM DESIGN, 2014, 45 (03) : 381 - 422
  • [50] GREP: Games for the Runtime Enforcement of Properties
    Renard, Matthieu
    Rollet, Antoine
    Falcone, Ylies
    TESTING SOFTWARE AND SYSTEMS (ICTSS 2017), 2017, 10533 : 259 - 275