Modular Verification of Security Properties in Actor Implementations (MoVeSPAcI)
This page describes the project Modular Verification of Security Properties in Actor Implementations (MoVeSPAcI).
Security and, in particular, information flow 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 flow 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 satisfies these specifications. Thus, the project provides a tool-supported framework for bridging the gap between system-level security analysis and distributed implementations.
The project is funded by the DFG.
The project started in September 2010 and was renewed for the second funding period in October 2012.
Homepage of the Priority Programme Reliably Secure Software Systems (RS3)
The homepage can be found here.