Skip to main content

Runtime Verification of k-Safety Hyperproperties in HyperLTL

Publication Type
Year of Publication
2016
Conference/Journal Name
IEEE Computer Security Foundations Symposium (CSF)
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 differentperformance 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.