Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract)
This work addresses secure compilation for systems requiring robust security guarantees, but it appears incremental as it builds on existing context back-translation methods.
The paper tackles the problem of defining soundness criteria for secure compilation by mapping robust hyperproperty preservation across adversarial contexts, and shows that even the strongest criteria can be achieved for simple transformations using context back-translation techniques.
We map the space of soundness criteria for secure compilation based on the preservation of hyperproperties in arbitrary adversarial contexts, which we call robust hyperproperty preservation. For this, we study the preservation of several classes of hyperproperties and for each class we propose an equivalent "property-free" characterization of secure compilation that is generally better tailored for proofs. Even the strongest of our soundness criteria, the robust preservation of all hyperproperties, seems achievable for simple transformations and provable using context back-translation techniques previously developed for showing fully abstract compilation. While proving the robust preservation of hyperproperties that are not safety requires such powerful context back-translation techniques, for preserving safety hyperproperties robustly, translating each finite trace prefix back to a source context seems to suffice.