Monitoring Security Policies with Metric First-order Temporal Logic

We show the practical feasibility of monitoring complex security properties using a runtime monitoring approach for metric first-order temporal logic. In particular, we show how a wide variety of security policies can be naturally formalized in this expressive logic, ranging from traditional policies like Chinese Wall and separation of duty to more specialized usage-control and compliance requirements. We also explain how these formalizations can be directly used for monitoring and experimentally evaluate the performance of the resulting monitors.