UWSpace will be migrating to a new version of its software from July 29th to August 1st. UWSpace will be offline for all UW community members during this time.
Monitoring and Enforcement of Safety Hyperproperties
Abstract
Certain important security policies such as information flow characterize system-wide behaviors and are not properties of individual executions. It is known that such security policies cannot be expressed in trace-based specification languages such as linear-time temporal logic (LTL).
However, formalisms such as hyperproperties and the associated logic HyperLTL
allow us to specify such policies. In this thesis,
we concentrate on the static enforcement and runtime verification of safety hyperproperties expressed in HyperLTL.
For static enforcement of safety hyperproperties, we incorporate
program repair techniques, where an input program is modified to satisfy certain properties while preserving its existing specifications.
Assuming finite state space for the input program, we show that the complexity of program repair for safety hyperproperties is in
general NP-hard. However, there are certain cases in which the problem can be solved in polynomial time. We identify such cases and give polynomial-time algorithms for them.
In the context of runtime verification, we make two contributions: we (1) analyze the complexity of decision procedures for verifying safety hyperproperties, (2) provide a syntactic fragment in HyperLTL to express certain k-safety hyperproperties, and (3) develop a general runtime verification technique for HyperLTL k-safety formulas, for cases where verification at run time can be done in polynomial time. Our technique is based on runtime formula progression as well as on-the-fly monitor synthesis across multiple executions.
Collections
Cite this version of the work
Shreya Agrawal
(2015).
Monitoring and Enforcement of Safety Hyperproperties. UWSpace.
http://hdl.handle.net/10012/9846
Other formats