Modular verification of security properties in actor implementations

参与者实现中安全属性的模块化验证

• 批准号: 183816318
• 负责人: Professor Dr. Arnd Poetzsch-Heffter
• 金额: --
• 依托单位: Universitätsleitung - Präsidium
• 依托单位国家: 德国
• 项目类别: Priority Programmes
• 财政年份: 2010
• 资助国家: 德国
• 起止时间: 2009-12-31 至 2015-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/183816318?language=en
• 关键词: Modular; verification; security; properties; actor

Security and, in particular, information ow properties refer to the behavior of multi-agent distributed systems. Typical examples are privacy aspects in social networks and confidentiality issues in online trading systems. Verification of such properties has to meet the following challenges:•Information ow properties are more complex than safety and liveness properties because they are defined in terms of sets of possible system traces.•The analysis has to take into account malicious agents that try to corrupt the system.•To scale, the verification has to be modular, i.e., the implementation of each (benevolent) agent should be separately analyzable.We will develop a tool-supported, two-tier framework for the verification of security properties in actor implementations of multi-agent systems. The specification tier supports modeling of systems as communicating agents and formalizing their security properties. It will be realized as a generic theory in a higher-order interactive proof assistant. Starting from the model and property definitions, the theory supports the decomposition of global properties into sufficient agent-local properties. The implementation tier assumes that agents are implemented as object-oriented programs following the actor paradigm. From the model, we will generate interface specifications for the actors and verify that the program code satisies these specifications. Thus, the project provides a tool-supported framework for bridging the gap between system-level security analysis and distributed implementations.

安全性，特别是信息和属性指的是多代理分布式系统的行为。典型的例子是社交网络中的隐私问题和在线交易系统中的保密问题。此类属性的验证必须满足以下挑战：·信息流属性比安全和活性属性更复杂，因为它们是根据可能的系统踪迹集定义的。·分析必须考虑试图破坏系统的恶意代理。·为了规模，验证必须是模块化的，即每个(仁慈的)代理的实现应该是可单独分析的。我们将开发一个工具支持的两层框架，用于验证多代理系统的参与者实现中的安全属性。规范层支持将系统建模为通信代理并形式化它们的安全属性。它将作为一个通用理论在一个更高阶的交互证明助手中实现。该理论从模型和属性定义出发，支持将全局属性分解为充分的代理局部属性。实现层假定代理被实现为遵循参与者范例的面向对象的程序。从模型中，我们将为参与者生成接口规范，并验证程序代码是否满足这些规范。因此，该项目提供了一个工具支持的框架，用于弥合系统级安全分析和分布式实施之间的差距。