论文标题
安全系统中不透明度性能的定量验证
Quantitative Verification of Opacity Properties in Security Systems
论文作者
论文摘要
我们描述了一种在不透明框架中表达的流安全性属性的规范和验证的方法。我们提出了一种逻辑，用于直接在系统中直接表达该属性，该属性可以建模为可观察到的标记过渡系统。我们开发验证技术，以分析有关观察概念的属性不透明度。将概率运算符添加到规范语言中，可以实现定量分析和验证。该分析是作为对Prism模型检查器的扩展而实施的，并通过许多示例进行了说明。最后，绘制了一种基于熵的不透明度属性的替代方法。
We delineate a methodology for the specification and verification of flow security properties expressible in the opacity framework. We propose a logic, OpacTL , for straightforwardly expressing such properties in systems that can be modelled as partially observable labelled transition systems.We develop verification techniques for analysing property opacity with respect to observation notions. Adding a probabilistic operator to the specification language enables quantitative analysis and verification. This analysis is implemented as an extension to the PRISM model checker and illustrated via a number of examples. Finally, an alternative approach to quantifying the opacity property based on entropy is sketched.
