Runtime Verification of k-Safety Hyperproperties in HyperLTL

Citations Over TimeTop 10% of 2016 papers

Abstract

This paper introduces a novel runtime verification technique for a rich sub-class of Clarkson and Schneider's hyperproperties. The primary application of such properties is in expressing security policies (e.g., information flow) that cannot be expressed in trace-based specification languages (e.g., LTL). First, to incorporate syntactic means, we draw connections between safety and co-safety hyperproperties and the temporal logic HYPERLTL, which allows explicit quantification over multiple executions. We also define the notion of monitorability in HYPERLTL and identify classes of monitorable HYPERLTL formulas. Then, we introduce an algorithm for monitoring k-safety and co-k-safety hyperproperties expressed in HYPERLTL. Our technique is based on runtime formula progression as well as on-the-fly monitor synthesis across multiple executions. We analyze different performance aspects of our technique by conducting thorough experiments on monitoring security policies for information flow and observational determinism on a real-world location-based service dataset as well as synthetic trace sets.

Related Papers

• → What Is a Trace? A Runtime Verification Perspective(2016)22 cited
• → Model Check What You Can, Runtime Verify the Rest(2018)9 cited
• → Verification Runtime Analysis: Get the Most Out of Partial Verification(2020)2 cited
• → Introduction to the special issue on runtime verification(2018)1 cited
• Runtime Verification of Linear Temporal Specifications with Degradation(2014)