Security Type Systems and Deduction

安全类型系统和推导

• 批准号: 183816297
• 负责人: Professor Dr. Tobias Nipkow, Ph.D.
• 金额: --
• 依托单位: Lehrstuhl für Informatik XXI: Logik und Verifikation
• 依托单位国家: 德国
• 项目类别: Priority Programmes
• 财政年份: 2010
• 资助国家: 德国
• 起止时间: 2009-12-31 至 2014-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/183816297?language=en
• 关键词: Security; Type; Systems; 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.

该项目的目的是全面核查基于网络的会议管理系统的信息流安全。这是一个突出的基于Web的工作流管理系统的实例，我们的结果将在原则上适用于所有这样的system.The建模和验证这样的系统的关键挑战如下。系统必须同时可用和验证。有复杂的条件规定允许发布信息。安全属性应该系统地处理系统中所有机密信息的来源。验证应该是普遍的，覆盖所有级别，不仅是逻辑内核，还包括Web接口。所有复杂的功能都集中在交互式验证的内核中。没有通过薄接口的信息泄漏的证据委托给在这个优先程序中的其他项目开发的全自动工具。该系统被分解的方式，交互式验证和自动程序分析的组合产生所需的安全特性的组合方式。我们还将开发的方法，可以减少验证的无限系统的有限状态模型checkingproblems的抽象。我们的研究的一个重要成果将是一个可重用的建模和验证框架，支持基于Web的工作流管理系统的组合开发。