Security Type Systems and Deduction

该项目的目的是普遍核查基于web的会议管理系统的信息流安全性。这是一个基于web的工作流管理系统的突出实例，我们的结果原则上适用于所有这样的系统。建模和验证这样一个系统的关键挑战如下。该系统必须是可用的，并在同一时间验证。有一些复杂的条件规定了允许发布的信息。安全属性应系统地处理系统中所有机密信息的来源。验证应该是普遍的，涵盖所有级别，不仅是逻辑内核，还包括web接口。以下方法解决了上述挑战。所有复杂的功能都集中在内核中进行交互验证。通过瘦接口不存在信息泄漏的证明委托给该优先级计划中其他项目开发的全自动工具。系统以这样一种方式分解，即交互式验证和自动程序分析的组合以组合方式产生所需的安全属性。我们还将开发可以通过抽象将无限系统的验证简化为有限状态模型检查问题的方法。我们研究的一个重要成果将是一个可重用的建模和验证框架，它支持基于web的工作流管理系统的组合开发。

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.