Runtime Policy Monitoring and Enforcement

Compliance policies specify allowed system behaviour and are ubiquitous in today's IT systems, ranging from access-​control and security policies to regulations of medical and financial IT services. We develop techniques and tool support for offline and online monitoring of system behaviours with respect to compliance policies specified in a first-​order temporal logic. We are also interested in policy enforcement, that is, preventing policy violations instead of only detecting them. Examples of our previous case studies include monitoring network security policies, monitoring database usage control policies, monitoring subledger accounting policies, monitoring GDPR privacy policies, etc.

We offer Bachelor and Master projects to motivated students who are interested in one or more of the following areas: automata theory, first-​order or temporal logics, algorithms and data structures, interactive theorem proving, or data stream processing.

Possible projects include:

• develop and implement techniques not only to detect violations, but also to identify the cause of violations
• improve our tools’ performance by carefully adapting data structures and query evaluation techniques from databases and stream processing
• increase the trust in the tools by formally proving them correct
• apply, adapt, and extend the already developed monitoring techniques to real-​world case studies in domains such as intrusion detection or run-​time verification

Desirable Prerequisites for Student Projects

Familiarity with temporal logics (e.g. from the FMFP course) and

• for formal verification projects:
  • strong skills in functional programming (e.g. from the FMFP course)
  • some familiarity with Isabelle/HOL (e.g. from self-study)
• for projects involving stream processing:
  • familiarity with SQL and databases
  • some familiarity with stream processing frameworks (e.g. Apache Flink) is helpful

Previous Theses (Selection)

• Sheila Zingg's master's thesis: adding recursive operators to the formally verified VeriMon tool
• protected pageSarah Plocher's master's thesislock: automated translation from StreamingSQL to Metric First-​order Temporal Logic
• protected pageFrederik Brix' master's thesislock: rescaling and state redistribution for the Scalable Online Monitoring Framework
  
• protected pageEmanuele Marsicano's bachelor thesislock: verified performance optimizations for aggregations in VeriMon
• protected pageMarc Bolliger's bachelor thesislock: improved monitoring complexity for Metric Dynamic Logic
  
• Simon Yuan's bachelor thesis: explaining monitoring verdicts for Metric Dynamic Logic
  

Further Information

Please contact  or see group's project page.