Hyperproperties
Hyperproperties
复制标题
DOI：
10.3233/jcs-2009-0393
复制
发表时间：
2010-01-01
影响因子：
1.2
通讯作者：
Schneider, Fred
中科院分区：
文献类型：
--
作者：
Clarkson, Michael;Schneider, Fred
长期以来一直用于系统推理的跟踪属性是一组执行跟踪。这里介绍的超属性是跟踪属性的集合。超属性可以表达跟踪属性无法表达的安全策略，如安全信息流和服务级别协议。将安全性和活性推广到超属性，并证明了每一个超属性都是安全超属性和活性超属性的交集。给出了一种安全超属性的验证技术，推广了现有的安全信息流验证技术。改进被证明适用于安全超性质。给出了超性质的一个拓扑刻画。
Trace properties, which have long been used for reasoning about systems, are sets of execution traces. Hyperproperties, introduced here, are sets of trace properties. Hyperproperties can express security policies, such as secure information flow and service level agreements, that trace properties cannot. Safety and liveness are generalized to hyperproperties, and every hyperproperty is shown to be the intersection of a safety hyperproperty and a liveness hyperproperty. A verification technique for safety hyperproperties is given and is shown to generalize prior techniques for verifying secure information flow. Refinement is shown to be applicable with safety hyperproperties. A topological characterization of hyperproperties is given.