Runtime Policy Monitoring and Enforcement
It is a growing concern for companies, administrations, and end users alike whether IT systems comply with policies regulating the usage of sensitive data. Checking their compliance is particularly acute as many of our modern infrastructures (communication, entertainment, finance and banking, social networks, etc.) are based on IT systems that collect, process, and share data.
A prominent approach to compliance checking is runtime monitoring. Here, system actions are observed and automatically checked for compliance against a policy. Our research project is concerned with developing efficient and scalabale runtime monitoring techniques for expressive policy specification languages. Most of our results have focused on a safety fragment of metric first-order temporal logic (MFOTL). We are also interested in policy enforcement, that is, preventing policy violations instead of only detecting them.
Project Members
- Prof. Dr. David Basin
- external page François Hublet
- external page Dr. Srđan Krstić
- Joshua Schneider
- external page Dr. Dmitriy Traytel (University of Copenhagen)
Former Members
- Dr. Matúš Harvan
- Dr. Felix Klaedtke
- Dr. Samuel Müller
- Dr. Martin Raszyk
- Dr. Eugen Zălinescu
- Bhargav Bhatt
Software
- external page MonPoly is a monitoring tool that checks compliance of log files with respect to policies in metric first-order temporal logic (MFOTL) with aggregation operators.
- external page VeriMon is a formally verified and optimized online monitoring tool for metric first-order dynamic logic (MFODL) with aggregation operators and recursion. The source code of Verimon’s core algorithm is automatically generated from the external page Isabelle/HOL formalization, whereas formula and log parsing code is re-used from MonPoly.
- external page Hydra is an offline montoring tool for metric temporal logic (MTL) and metric dynamic logic (MDL) that exploits multiple reading heads to significantly reduce its memory consumption. Hydra's core algorithm for MDL has been formally verified in external page Isabelle/HOL and the automatically generated source code is part of a monitoring tool external page Vydra. The formula and log parsing code in Vydra has not been formally verified.
- The external page Scalable Online Monitoring Framework parallelizes existing first-order monitoring tools in a black-box manner. We have used the framework to parallelize MonPoly and DejaVu.
- external page AERIAL is an almost event-rate independent monitoring tool that checks compliance of log files with respect to policies in metric temporal logic (MTL) and metric dynamic logic (MDL).
Publications
Monitoring Algorithms
- MFODL: IJCAR'20
- MFOTL: FSTTCS'08, CAV'10, JACM'15, RV'19
- Multi-head monitoring: ATVA'19, ATVA'20
- MTL and MDL: TACAS'17, RV'17, FMSD'19
- Past-time MTL: RV'11, Acta Informatica '17
- Sliding window: IPL'15
Monitoring Extensions
- Recursive rules: external page TACAS'22
- Out-of-order monitoring: FSTCCS'15, CAV'17, TOCL'19
- Aggregations: RV'13, FMSD'15
- Imprecise timestamps: RV'14
- Interleaving logs: TIME'11, TSE'13
- Incomplete and disagreeing logs: RV'12
- Hashing: external page RV'22
- Arbitrary first-order queries: external page ICDT'22, LMCS'23
- Verified algorithms: RV'19, IJCAR'20, external page TACAS'22, external page ICTAC'22
Scalable Monitoring
Applications
- Internet computer: external page FM'23
- GDPR: ESORICS'19
- Network security: FMSD'16
- Distributed systems: TSE'13
- Security policies: SACMAT'10
Tool papers
- MonPoly: RV'11, RV-CuBES'17
- AERIAL: external page RV-CuBES'17
- Verimon: external page ICTAC'22
- Benchmark generator: Download RV'20 (PDF, 640 KB)
- Monitoring tools taxonomy: external page RV'18, external page STTT'21
Enforcement
- Enforceable security policies: POST'12, ACM TOPS (formerly known as TISSEC) '13
- Enforcing MFOTL: ESORICS'22