Gray-box Runtime Enforcement of Hyperproperties

Enforcement of information-flow policies has been extensively studied by language-based approaches over the past few decades. In this paper, we propose an alternative, novel, general, and effective approach using enforcement of hyperproperties – a powerful formalism for expressing and reasoning about a wide range of information-flow security policies. We study black- vs. gray- vs. white-box enforcement of hyperproperties expressed by nondeterministic finite-word hyperautomata (NFH), where the enforcer has null, some, or complete information about the implementation of the system under scrutiny. Given an NFH, in order to generate a runtime enforcer, we reduce the problem to controller synthesis for hyperproperties and subsequently to the satisfiability problem for quantified Boolean formulas (QBFs). The resulting enforcers are transferable with lowoverhead. We conduct a rich set of case studies, including information-flow control
for JavaScript code, as well as synthesizing obfuscators for control plants.