Synthesizing Efficient and Permissive Programmatic Runtime Shields for Neural Policies

TL;DR

Aegis is a new framework that synthesizes lightweight, permissive runtime shields for neural policies, ensuring safety with less overhead and fewer interventions by using a novel program synthesis approach.

Contribution

Aegis introduces a sketch-based synthesis method leveraging counterexample-guided inductive synthesis and Bayesian optimization for efficient shield generation.

Findings

Ensures safety by correcting all unsafe commands.

Reduces time overhead by 2.2× compared to state-of-the-art.

Cuts memory usage by 3.9× and interventions by 1.5×.

Abstract

With the increasing use of neural policies in control systems, ensuring their safety and reliability has become a critical software engineering task. One prevalent approach to ensuring the safety of neural policies is to deploy programmatic runtime shields alongside them to correct their unsafe commands. However, the programmatic runtime shields synthesized by existing methods are either computationally expensive or insufficiently permissive, resulting in high overhead and unnecessary interventions on the system. To address these challenges, we propose Aegis, a novel framework that synthesizes lightweight and permissive programmatic runtime shields for neural policies. Aegis achieves this by formulating the seeking of a runtime shield as a sketch-based program synthesis problem and proposing a novel method that leverages counterexample-guided inductive synthesis and Bayesian optimization to solve it. To evaluate Aegis and its synthesized shields, we use eight representative control systems and compare Aegis with the current state-of-the-art. Our results show that the programmatic runtime shields synthesized by Aegis can correct all unsafe commands from neural policies, ensuring that the systems do not violate any desired safety properties at all times. Compared to the current state-of-the-art, Aegis's shields exhibit a 2.2$\times$ reduction in time overhead and a 3.9$\times$ reduction in memory usage, suggesting that they are much more lightweight. Moreover, Aegis's shields incur an average of 1.5$\times$ fewer interventions than other shields, showing better permissiveness.