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 pageFrançois Hubletcall_made
- external pageDr. Srđan Krstićcall_made
- Joshua Schneider
- external pageDr. Dmitriy Traytelcall_made (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 pageMonPolycall_made 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 pageVeriMoncall_made 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 pageIsabelle/HOL formalizationcall_made, whereas formula and log parsing code is re-used from MonPoly.
- external pageHydracall_made 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 pageIsabelle/HOLcall_made and the automatically generated source code is part of a monitoring tool external pageVydracall_made. The formula and log parsing code in Vydra has not been formally verified.
- The external pageScalable Online Monitoring Frameworkcall_made parallelizes existing first-order monitoring tools in a black-box manner. We have used the framework to parallelize MonPoly and DejaVu.
- external pageAERIALcall_made 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 pageTACAS'22call_made
- 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 pageRV'22call_made
- Arbitrary first-order queries: external pageICDT'22call_made, LMCS'23
- Verified algorithms: RV'19, IJCAR'20, external pageTACAS'22call_made, external pageICTAC'22call_made
Scalable Monitoring
Applications
- Internet computer: external pageFM'23call_made
- 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 pageRV-CuBES'17call_made
- Verimon: external pageICTAC'22call_made
- Benchmark generator: DownloadRV'20 (PDF, 640 KB)vertical_align_bottom
- Monitoring tools taxonomy: external pageRV'18call_made, external pageSTTT'21call_made
Enforcement
- Enforceable security policies: POST'12, ACM TOPS (formerly known as TISSEC) '13
- Enforcing MFOTL: ESORICS'22