We introduce a novel approach to secure compilation based on maps of distributive laws. We demonstrate through four examples that the coherence criterion for maps of distributive laws can potentially be a viable alternative for compiler security instead of full abstraction, which is the preservation and reflection of contextual equivalence. To that end, we also make use of the well-behavedness properties of distributive laws to construct a categorical argument for the contextual connotations of bisimilarity.
@article{arxiv.2004.03557,
title = {A categorical approach to secure compilation},
author = {Stelios Tsampas and Andreas Nuyts and Dominique Devriese and Frank Piessens},
journal= {arXiv preprint arXiv:2004.03557},
year = {2020}
}
Comments
Accepted in Coalgebraic Methods in Computer Science, ver. 2020