Modular verification of security properties in actor implementations

• Applicant: Professor Dr. Arnd Poetzsch-Heffter
• Subject Area: Software Engineering and Programming Languages
• Term: from 2010 to 2016
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 183816318

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.

• DFG Programme: Priority Programmes
• Subproject of: SPP 1496: Reliably Secure Software Systems