Modular Modeling of Delegation Security in Software Development (MoDelSec)

该项目的目标是开发一种方法，在基于正式的软件开发方法的上下文中考虑访问控制（特别是用户权限授权）中的高级技术。该方法将基于从安全信息流方法到安全验证的形式化，这为特别细粒度的安全分析提供了可能性。由于安全信息流形式化传统上是在强制访问控制（MAC）上下文中使用的，通常不包括用户级权限委托，因此在这种上下文中对委托的研究迄今为止是有限的。由于安全信息流方法在过去几年中得到了越来越多的使用，因此本项目的目标之一就是通过研究如何支持对复杂的访问控制技术（如用户权限委托）的分析来填补这一空白。进一步的目标是在访问控制机制分析的上下文中利用安全信息流属性（如[j<e:1> r00, Man02]）的模块化分析结果，特别是用户权限的授权。要取得的科学进展将被转移到基于正式验证工具支持的安全软件开发方法的上下文中。它们将使用电子卫生部门的应用程序进行验证（与Fraunhofer ISST在该领域的现有项目合作，该项目的首席研究员担任次要职位）。项目的主要成果将包括以下内容：•支持安全信息流模型背景下用户权限授权的模块化分析的理论。•集成到基于正式验证工具支持的安全软件开发方法的环境中。•基于SMT求解器的形式化验证的自动化工具（如Z3 [dMB08]）。•通过电子医疗系统中的应用程序进行验证，包括委托访问控制。

The objective of this project is to develop an approach for considering advanced techniques in access control (in particular delegation of user permissions) in the context of a formally-based software development methodology. The approach will be based on formalizations from the Secure Information Flow approach to security verification, which offer the possibility for a particularly finegrained security analysis. Since secure information flow formalizations have traditionally been used in the context of mandatory access control (MAC) which does not usually include user-level permission delegation, investigation of delegation in this context has so far been limited. Since the Secure Information Flow approach has found increasing use over the last few years, one of the goals of this project is therefore to fill this gap by investigating how to support the analysis of sophisticated access control techniques such as delegation of user permissions. A further objective is to exploit results on modular analysis of Secure Information Flow properties (such as [Jür00, Man02]) in the context of the analysis of access control mechanisms and in particular the delegation of user permissions. The scientific progress to be made will be transferred into the context of a secure software development approach based on formal verification tool support. They will be validated using an application from the e-health sector (in collaboration with existing projects in this domain at Fraunhofer ISST, where the Principal Investigator of this project holds a secondary position).Main results of the project will include the following:• A theory supporting the modular analysis of user permission delegation in the context of secure information flow models.• Integration into the context of a secure software development approach based on formal verification tool support.• Automated tools for formal verification based on SMT solvers (such as Z3 [dMB08]).• Validation through an application in an e-health system including access control with delegation.