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. Categories and Subject Descriptors D.2.1 [Software Engineering]: Requirements/Specifications—Languages; D.2.5 [Software Engineering]: Testing and Debugging—Monitors, Tracing; D.4.6 [Operating Systems]: Security and Protection; J.1 [Computer Applications]: Administrative Data Processing—Business, Law General Terms Security, Verification, Legal Aspects Keywords Temporal Logic, Monitoring, Security Policies, Access Control, Separation ...

• Type: Conference
• Year: 2010
• Where: SACMAT
• Authors: David A. Basin, Felix Klaedtke, Samuel Müller
• Keywords: Control Systems, SACMAT 2010, Security Policies, Temporal Logic, first-order Temporal Logic