Gray-Box Monitoring of Hyperproperties
Gray-Box Monitoring of Hyperproperties
复制标题
超属性的灰盒监控
DOI：
10.1007/978-3-030-30942-8_25
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Schneider, Gerardo
中科院分区：
文献类型：
--
作者：
Stucki, Sandro;Sanchez, Cesar;Schneider, Gerardo
许多重要的系统属性，特别是在安全性和隐私性方面，无法静态验证。因此，运行时验证是一个很有吸引力的选择。HyperLTL等超属性的逻辑支持丰富的此类属性集。我们首先表明，HyperLTL的黑盒监控通常是不可行的，并建议采用黑盒方法。灰盒监视意味着在运行时对系统进行分析，这给可监视性（解决监视问题的可行性）带来了新的限制。因此，作为本文的另一个贡献，我们改进了经典的可监控性概念，包括跟踪属性和超属性，并考虑到监控的可计算性。然后，通过在运行时使用基于smt的静态验证器，应用我们的方法来监视称为分布式数据最小化的隐私超属性，该属性表示为HyperLTL属性。
Many important system properties, particularly in security and privacy, cannot be verified statically. Therefore, runtime verification is an appealing alternative. Logics for hyperproperties, such as HyperLTL, support a rich set of such properties. We first show thatblack-boxmonitoring of HyperLTL is in general unfeasible, and suggest agray-boxapproach. Gray-box monitoring implies performing analysis of the system at run-time, which brings new limitations to monitorability (the feasibility of solving the monitoring problem). Thus, as another contribution of this paper, we refine the classic notions ofmonitorability, both for trace properties and hyperproperties, taking into account the computability of the monitor. We then apply our approach to monitor a privacy hyperproperty calleddistributed data minimality, expressed as a HyperLTL property, by using an SMT-based static verifier at runtime.