Runtime Verification of Hyperproperties for Deterministic Programs
Runtime Verification of Hyperproperties for Deterministic Programs
复制标题
确定性程序超属性的运行时验证
DOI：
10.1145/3193992.3193995
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
David Sands
中科院分区：
文献类型：
--
作者：
Srinivas Pinisetty;G. Schneider;David Sands
本文考虑确定性程序的安全超属性的运行时验证问题。一些安全和信息流策略，如数据最小化、不干扰、完整性和软件掺杂，自然被正式表示为安全超属性。虽然有超属性的监控结果，但算法非常复杂，因为这些属性是一组迹线上的属性，而不是单个迹线上的属性。对于我们考虑的确定性输入输出规划，以及我们感兴趣的特定安全超性质，问题可以归结为对迹性质的监控。在这篇文章中，我们提出了一种更简单的确定性程序安全超属性的监控方法。该方法将给定的安全超属性转换为迹属性，提取给定超属性的特征谓词，并提供以该谓词为参数的参数监控器。对于所考虑的子类中的任何超属性，我们展示了如何综合运行时验证监视器。我们以给定类的参数监控器的形式实现了我们的方法，并将其应用于一些超属性，包括数据最小化、无干扰、完整性和软件掺杂。我们展示了有关离线和在线监控的结果。
In this paper, we consider the runtime verification problem of safety hyperproperties for deterministic programs. Several security and information-flow policies such as data minimality, non-interference, integrity, and software doping are naturally expressed formally as safety hyperproperties. Although there are monitoring results for hyperproperties, the algorithms are very complex since these are properties over set of traces, and not over single traces. For the deterministic input-output programs that we consider, and the specific safety hyperproperties we are interested in, the problem can be reduced to monitoring of trace properties. In this paper, we present a simpler monitoring approach for safety hyperproperties of deterministic programs. The approach involves transforming the given safety hyperproperty into a trace property, extracting a characteristic predicate for the given hyperproperty, and providing a parametric monitor taking such predicate as parameter. For any hyperproperty in the considered subclass, we show how runtime verification monitors can be synthesised. We have implemented our approach in the form of a parameterised monitor for the given class, and have applied it to a number of hyperproperties including data minimisation, non-interference, integrity and software doping. We show results concerning both offline and online monitoring.