Security Type Systems and Deduction

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

The aim of this project is the pervasive verification of the information-flow security of a web-based conference management system. This is a prominent instance of a web-based workflow management system and our results will in principle apply to all such systems.The key challenges in modelling and verifying such a system are the following. The system must be usable and verified at the same time. There are complex conditions prescribing the permitted release of information. The security propertie should address systematically all sources of confidential information in the system. The verification should be pervasive, covering all levels, not just the logical kernel but also the web interface.The following methods address the above challenges. All complex functionality is concentrated in the kernel which is verified interactively. The proof of absence of information leakage through the thin interface is delegated to fully automatic tools developed by other projects in this priority program.The system is decomposed in such a manner that the combination of interactive verification and automatic program analysis yields the desired security properties in a compositional manner. We will also develop methods that can reduce the verification of infinite systems to finite-state model checkingproblems by abstraction.An important outcome of our research will be a reusable modelling and verification framework that supports the compositional development of web-based workflow management systems.