Program Repair for Hyperproperties

Hyperproperties are system properties that relate multiple computation traces. This class of properties includes popular information-flow security policies as well as consistency requirements in concurrent computing. We study the repair problem for hyperproperties specified in the temporal logic HyperLTL. We first consider finite-state programs and rigorously analyze the complexity of repair for various fragments of HyperLTL and different system types: tree-shaped, acyclic, and general Kripke structures. We then switch to infinite-state programs and propose a repair algorithm based on symbolic execution, constraint generation, and syntax-guided synthesis (SyGuS) of repair expression. As a practical realization, we develop an iterative repair approach. Here, we search for a sequence of repairs that are closer and closer to the original program’s behavior. We implement our method in a prototype and report on encouraging experimental results using off-the-shelf SyGuS solvers.