Modular Modeling of Delegation Security in Software Development (MoDelSec)

本项目的目标是在基于正式的软件开发方法的背景下，制定一种方法来考虑访问控制方面的先进技术(特别是授权用户权限)。该方法将基于从安全信息流方法到安全验证的形式化，这为特别细粒度的安全分析提供了可能性。由于安全信息流的形式化传统上被用于强制访问控制(MAC)的上下文中，而强制访问控制通常不包括用户级权限委派，因此到目前为止对该上下文中的委派的研究一直是有限的。由于安全信息流方法在过去几年中得到了越来越多的使用，因此，该项目的目标之一是通过调查如何支持复杂的访问控制技术(如用户权限委派)的分析来填补这一空白。另一个目标是在分析访问控制机制，特别是用户权限委派的背景下，利用关于安全信息流属性(如[Jü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.