Gray-box monitoring of hyperproperties with an application to privacy
Gray-box monitoring of hyperproperties with an application to privacy
复制标题
通过隐私应用对超属性进行灰盒监控
DOI：
10.1007/s10703-020-00358-w
复制
发表时间：
2021
影响因子：
0.8
通讯作者：
Bonakdarpour, Borzoo
中科院分区：
文献类型：
--
作者：
Stucki, Sandro;Sánchez, César;Schneider, Gerardo;Bonakdarpour, Borzoo
运行时验证是测试、模型检查和其他静态验证技术的补充，用于验证软件属性。可监控性描述了在运行时可以验证(监视)的内容。对于轨迹属性和超属性(在轨迹集合上定义的属性)，都给出了不同的可监控性定义，但这些定义通常只涉及表征可监控性概念时重要的一些方面。本文的第一个贡献是对跟踪属性和超属性的经典可监控性概念的提炼，其中考虑了监控器的可计算性。我们工作的第二个贡献是证明了对HyperLTL(一种用于超属性的逻辑)的黑盒监控通常是不可行的，并提出了将静态验证和运行时验证相结合的灰盒方法。其主要思想是在运行时调用静态验证器作为预言，在某些情况下，允许对在黑盒方法下被认为不可监视的属性做出最终裁决。我们的第三个贡献是将这个解决方案实例化到称为分布式数据最小化的隐私属性中，该属性无法使用黑盒运行时验证进行验证。我们使用基于SMT的静态验证器作为运行时的预言器。我们已经在概念验证工具Minion中实现了监控数据最小化的灰盒方法。我们描述了该工具，并将其应用于几个案例研究，以显示其可行性。
Runtime verification is a complementary approach to testing, model checking and other static verification techniques to verify software properties.Monitorabilitycharacterizes what can be verified (monitored) at run time. Different definitions of monitorability have been given both for trace properties and forhyperproperties(properties defined over sets of traces), but these definitions usually cover only some aspects of what is important when characterizing the notion of monitorability. The first contribution of this paper is a refinement of classic notions of monitorability both for trace properties and hyperproperties, taking into account, among other things, the computability of the monitor. A second contribution of our work is to show thatblack-boxmonitoring of HyperLTL (a logic for hyperproperties) is in general unfeasible, and to suggest agray-boxapproach in which we combine static and runtime verification. The main idea is to call a static verifier as an oracle at run time allowing, in some cases, to give a final verdict for properties that are considered to be non-monitorable under a black-box approach. Our third contribution is the instantiation of this solution to a privacy property calleddistributed data minimizationwhich cannot be verified using black-box runtime verification. We use an SMT-based static verifier as an oracle at run time. We have implemented our gray-box approach for monitoring data minimization into the proof-of-concept toolMinion. We describe the tool and apply it to a few case studies to show its feasibility.
登录
查看更多内容
运行时验证讲座
DOI：
--
发表时间：
2018
期刊：
Lecture Notes in Computer Science
影响因子：
--
作者：
E. Bartocci;Yliès Falcone;G. Goos;J. Hartmanis;J. Leeuwen;David Hutchison
通讯作者：
David Hutchison
DOI：
--
发表时间：
1977
期刊：
Symposium on Operating Systems Principles
影响因子：
--
作者：
Ellis Choen
通讯作者：
Ellis Choen
运行时验证讲座：介绍性和高级主题
DOI：
--
发表时间：
2018
期刊：
影响因子：
--
作者：
E. Bartocci;Yliès Falcone
通讯作者：
Yliès Falcone
影响因子：
1.8
作者：
Aceto, Luca;Achilleos, Antonis;Lehtinen, Karoliina
通讯作者：
Lehtinen, Karoliina
DOI：
10.1145/3193992.3193995
发表时间：
2018
期刊：
2018 IEEE/ACM 6th International FME Workshop on Formal Methods in Software Engineering (FormaliSE)
影响因子：
--
作者：
Srinivas Pinisetty;G. Schneider;David Sands
通讯作者：
David Sands