English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
  DetailsSummary

Released
Paper

Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract)

MPS-Authors
/persons/resource/persons144522

Garg,  Deepak
Group D. Garg, Max Planck Institute for Software Systems, Max Planck Society;

/persons/resource/persons145080

Swasey,  David
Group D. Garg, Max Planck Institute for Software Systems, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

arXiv:1710.07309.pdf
(Preprint), 438KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Garg, D., Hritcu, C., Patrignani, M., Stronati, M., & Swasey, D. (2017). Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract). Retrieved from http://arxiv.org/abs/1710.07309.


Cite as: https://hdl.handle.net/21.11116/0000-0000-AC93-8
Abstract
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.