Syntax-Guided Automated Program Repair for Hyperproperties

TL;DR

The paper studies automatic repair of infinite-state programs against temporal hyperproperties specified in HyperLTL. It introduces HyRep, a constraint-based repair pipeline that uses symbolic execution to generate repair constraints and syntax-guided synthesis (SyGuS) to synthesize patch expressions, augmented by transparent and iterative repair to preserve original behavior. Key contributions include a formal framework for HyperLTL repairs with arbitrary quantifier prefixes, integration of transparency into SyGuS-based repair, and an iterative repair approach demonstrated on a prototype with encouraging results. The work advances regression repair for hyperproperties beyond k-safety, enabling more faithful patches in information-flow and robustness contexts while leveraging existing SyGuS solvers and tooling.

Abstract

We study the problem of automatically repairing infinite-state software programs w.r.t. temporal hyperproperties. As a first step, we present a repair approach for the temporal logic HyperLTL based on symbolic execution, constraint generation, and syntax-guided synthesis of repair expression (SyGuS). To improve the repair quality, we introduce the notation of a transparent repair that aims to find a patch that is as close as possible to the original program. 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.

Figures (3)

• Figure 1: Information leak in EDAS conference management system.
• Figure 2: Repair candidates discovered by our iterative repair.
• Figure 3: Selection of small-step reduction rules. We write $\llbracket e \rrbracket_\sigma \in \mathbb{Z}$ and $\llbracket b \rrbracket_\sigma \in \mathbb{B}$ for the value of expression $e$ and $b$ in store $\sigma$, respectively.