SECURE INFORMATION-FLOW. PRIVACY ENFORCEMENT VIA RUNTIME MONITORING.
Today, many systems contain private data, which should never leak into a public domain. Examples are medical patient data in hospitals and credit card information. We develop techniques to control the information flow in privacy-critical systems. More precisely, we design tools that provide reliable privacy guarantees. To this end, we address core challenges like a precise specification of information flow policies and provably correct verification methods.
Specification Languages for Information-Flow Policies. An essential step to enforce secure information flow is to precisely specify what kind of information leakage is to be prevented. To this end, we develop formal languages for various contexts like distributed systems (e.g. unmanned aircraft systems), networks and web-based systems. Each context poses different requirements concerning the expressivity of the language. Understanding what information-flow policies are expressible in a language and how computationally difficult they are to verify is a key challenge.
Secure Information-Flow in Web-Based Workflows. Lots of private data is shared, on a day-to-day basis, in online collaboration and content management systems. Often, many users interact via a web-based workflow. We work towards automatic verification methods that ensure that secure data is not unwillingly leaked. We identify what kind of policies can be checked in which context and develop efficient techniques to analyze the flow of information in web-based workflows.
Privacy Enforcement via Runtime Monitoring. In many settings, the behaviour of a system is determined by an unpredictable environment. This makes it impossible to verify the privacy of a system in a static way, i.e., before it is executed. We address this problem by developing methods to monitor and enforce privacy policies during runtime. These tasks pose challenging questions such as how to guarantee usability, efficiency, and how to deal with the huge amount of data that accumulates during runtime.
