Detailseite
Projekt
Modular verification of security properties in actor implementations
Antragsteller
Professor Dr. Arnd Poetzsch-Heffter
Fachliche Zuordnung
Softwaretechnik und Programmiersprachen
Förderung
Förderung von 2010 bis 2016
Projektkennung
Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 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-Verfahren
Schwerpunktprogramme
