KomDatIS
Connected Research Areas
- Program Analysis via Dynamic Symbolic Execution
- Automata Model Checking
- Neural Network Verification
The starting point of the research project is the development of a general data escrow concept. Establishing a fiduciary service for data exchange requires a number of processes and mechanisms that can be divided into three main groups: Motivation to participate in the data ecosystem, ensuring data sovereignty, and defining legal and contractual frameworks. Among other things, the project aims at an automated analysis for auditing compliance with terms of service and data usage policies. Compliance with the guidelines for the fiduciary management of data requires continuous checking and logging of access to data and data sets. More information about the whole project can be found here.
This project is funded by the German Federal Ministry of Education and Research (BMBF) within the Data Trust Models Funding Action (16DTM106A).
In the context of KomDatIS, we focus on the automatic verification of information flow properties and usage policies. Intuitively, we are interested in where data ends up and how it is used.
Information flow is also a property of interest in the area of program anaylsis where we develop GDart. We extended GDart and formalized the analysis to show how it relates to other well known properties, noninterference in particular.
Additionally, we are working on techniques to verify properties against register automata, an extention of finite state automata which allows read and write operations to memory cells.
To understand usage policies, we started looking at the structure of neural networks and how we can derive properties about them. In a first step, we explored the path enumeration problem for the program equivalent to neural network.
