Program-level Specification and Deductive Verification of Security Properties

该项目的主题是程序级安全属性的规格说明和演绎验证。近年来，计算机程序功能属性的形式化验证取得了巨大的进展。与此同时，已经发表了一些开创性的论文，表明在原则上可以将信息流问题表述为程序逻辑中的证明义务。我们的项目的总体目标是利用这些进展以及我们自己在功能属性的形式化方法方面的经验，以指定和验证安全属性。该项目对优先计划1496“RS3”的三个指导主题，安全属性的形式化和验证，以及确保“总体安全”做出了以下贡献：* 我们为计算机程序的信息流属性定义了规范和程序注释语言的语法和语义。工作的一部分是开发一种共同的子语言，可以通过优先方案内不同项目开发的工具来理解。我们设计并实现了一个系统，允许正式证明程序满足其信息流规范，并满足优先级计划中规定的可靠性，精度，可扩展性和可用性的要求。 技术基础是关键系统。在第三阶段的计划中，重点是通过模块化和程序属性的接口来扩展方法的范围和力量，强调安全的定量概念，整合不同类型的分析，并弥合它们之间的规范差距。

The topic of this project is program-level specification and deductive verification of security properties.In recent years tremendous progress has been achieved in formal verification of functional properties of computer programs. At the same time seminal papers have been published showing that it is in principle possible to formulate information-flow problems as proof obligations in program logics. The overall goal of our project is to leverage these advances together with our own experience in formal methods for functional properties in order to specify and verify security properties.The project makes the following contributions to the three guiding themes of Priority Programme 1496 "RS3", the formalization and verification of security properties, as well as assuring "security in the large":* We define syntax and semantics of a specification and program annotation language for information-flow properties of computer programs. Part of the effort is in developing a common sublanguage that can be understood by tools developed in different projects within the Priority Programme.* We design and implement a system that allows to prove formally that programs satisfy their information-flow specification and that meets the requirements of soundness, precision, scalability, and usability set forth in the Priority Programme. The technological basis is the KeY system.In Phase 3 of the programme, the emphasis is on extending the reach and power of the methods by modularisation and interfacing of program properties, emphasizing quantitative notions of security, integrating different types of analyses, and bridging the specification gaps between them.