Modular verification of security properties in actor implementations

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

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.