Paper Info
Title
Runtime Verification of k-Safety Hyperproperties in HyperLTL
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.
Year
DOI
Venue
2016
10.1109/CSF.2016.24
2016 IEEE 29th Computer Security Foundations Symposium (CSF)
Keywords
Field
DocType
Security policies,Runtime monitoring,Hyperproperties
Information flow (information theory),Programming language,Computer science,Determinism,Theoretical computer science,Runtime verification,Temporal logic,Security policy,Syntax,Computer security model
Conference
ISSN
ISBN
Citations 
1063-6900
978-1-5090-2608-1
14
PageRank 
References 
Authors
0.58
29
2
Name
Order
Citations
PageRank
Shreya Agrawal1150.95
Borzoo Bonakdarpour249045.02