Transfer and enhancement of information-flow control techniques to develop secure systems using the example of workflow systems (MORES2)

MORES 2项目继续发展在前身项目MORES中开始的安全工作流程系统开发框架。MORES致力于工作流系统安全属性的建模和验证，在特定的抽象层次上考虑不同类型的请求安全属性（例如信息流控制，职责分离），提供各种分解技术。现在，MORES 2的目标是为这些工作流规范开发适当的细化技术。特别是，要发展的细化概念必须支持工作流程各个方面（例如活动、数据、用户）的细化，还必须能够将MORES中考虑的安全属性转换为其他细化级别中的相应属性。较高抽象级别的翻译安全保证将作为较低级别安全属性验证的初始构建块。然而，我们不能期望改进的概念将保持一般的安全保证，因为否则所产生的限制将使这种改进不切实际。此外，改变抽象级别还可能导致攻击者观察工作流的能力的改进，这导致所需的安全保证如何被制定的改变。 在MORES 2中，我们将开发技术，以利用更高的抽象级别的安全保证，在较低的抽象级别上验证相应的安全属性。我们将在现有的交互式证明系统的基础上提供相应的验证工具支持，并将MORES 2的结果与MORES中的分解技术相结合，为工作流系统提供一个支持大规模安全性的集成方法。应用分解技术减少了要验证的组件的大小，并提高了验证任务的可扩展性。改进技术允许人们重用更高抽象级别的安全保证来验证较低级别的安全性，从而简化证明任务。将使用优先方案的基于网络的工作流管理系统中的参考方案安全性对这种方法进行评估，方法是在各种抽象层次上对其进行指定，并使用它来解释出现的安全属性沿着细化层次的翻译。

The project MORES2 continues the evolution of a framework for developing secure workflow systems started in the predecessor project MORES. MORES was engaged in the modeling and verification of security properties for workflow systems considering the different types of requested security properties (e.g. information-flow control, separation of duty) at a particular level of abstraction, providing various decomposition techniques. Now, MORES2 aims at the development of appropriate refinement techniques for these workflow specifications. In particular, the notion of refinement to be developed has to support the refinement of the various aspects (e.g. activities, data, users) of workflows and also has to be able to translate the security properties considered in MORES to corresponding properties in other refinement levels. Translated security guarantees of higher abstraction levels will serve as initial building blocks for the verification of security properties on lower levels. However, we cannot expect that the notion of refinement will preserve the security guarantees in general because otherwise the arising restrictions would render such a refinement impracticable. Additionally, changing the abstraction level may also result in a refinement of the abilities of an attacker observing the workflow, which causes a change of how the required security guarantees are formulated. In MORES2 we will develop techniques to make use of security guarantees of higher abstraction levels in verifying the corresponding security properties on lower abstraction levels. We will provide a corresponding verification tool support based on existing interactive proof systems.Combining the upcoming results of MORES2 with the decomposition techniques developed in MORES, we will provide an integrated approach supporting security-in-the-large for workflow systems. Applying the decomposition techniques reduces the size of the components to be verified and improves the scalability of the verification tasks in general. The refinement techniques allow one to reuse the security guarantees of higher abstraction levels to verify the security of lower levels resulting in simpler proof tasks. This approach will be evaluated using the reference scenario Security in Web-based Workflow Management Systems of the priority programme by specifying it on various abstraction levels and using it to exemplify the translation of the arising security properties along the refinement hierarchy.