Program-level Specification and Deductive Verification of Security Properties

点击翻译按钮获取中文摘要

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.