Trace-Length Independent Runtime Monitoring of Quantitative Policies

Abstract

Metric linear-time logic (MTL) has been widely used to specify runtime policies. Traditionally this use of MTL is to capture the qualitative aspects of the monitored systems, but recent developments in its extensions with aggregate operators allow some quantitative policies to be specified. Our interest in MTL-based policy languages is driven by applications in runtime malware or intrusion detection in platforms like Android and autonomous vehicles, which requires the monitoring algorithm to be independent of the length of the system event traces so that its performance does not degrade as the traces grow. We propose a policy language based on a past-time variant of MTL, extended with an aggregate operator called the metric temporal counting quantifier to specify a policy based on the number of times some sub-policies are satisfied in the specified past time interval. We show that a broad class of policies, but not all policies, specified with our language can be monitored in a trace-length independent way, and provide a concrete algorithm to do so. We implement and test our algorithm in both an existing Android monitoring framework and an autonomous vehicle simulation platform, and show that our approach can effectively specify and monitor quantitative policies drawn from real-world studies.