论文标题
Tokeneer ID站规范的自动验证的原型
An Automatically Verified Prototype of the Tokeneer ID Station Specification
论文作者
论文摘要
Tokeneer项目是国家安全局（NSA，美国）提出的一项计划，以证明可以通过以具有成本效益的方式应用严格的方法来制定开发高度安全的系统。 NSA选择了Altran Praxis（英国）来进行Tokeneer ID站的开发。该公司撰写了一份Z规范，后来用Spark ADA编程语言实施，该语言使用Spark Exciner Toolset进行了验证。在本文中，我们表明z规范可以在{log}设置约束语言中轻松自然地编码，从而生成功能原型。此外，我们表明{log}的自动证明功能可以履行有关状态不变的所有证明义务以及重要的安全属性。因此，原型可以被认为是相对于经过验证的属性正确的。这提供了经验证据，表明Z用户可以使用{log}从其Z规格中生成正确的原型。反过来，这些原型启用或简化了本文讨论的一些验证活动。
The Tokeneer project was an initiative set forth by the National Security Agency (NSA, USA) to be used as a demonstration that developing highly secure systems can be made by applying rigorous methods in a cost effective manner. Altran Praxis (UK) was selected by NSA to carry out the development of the Tokeneer ID Station. The company wrote a Z specification later implemented in the SPARK Ada programming language, which was verified using the SPARK Examiner toolset. In this paper, we show that the Z specification can be easily and naturally encoded in the {log} set constraint language, thus generating a functional prototype. Furthermore, we show that {log}'s automated proving capabilities can discharge all the proof obligations concerning state invariants as well as important security properties. As a consequence, the prototype can be regarded as correct with respect to the verified properties. This provides empirical evidence that Z users can use {log} to generate correct prototypes from their Z specifications. In turn, these prototypes enable or simplify some verificatio activities discussed in the paper.
