Translation Validation for Security Properties
This work tackles the problem of ensuring secure compilation for software developers and security practitioners, but it appears incremental as it builds on existing principles without claiming major breakthroughs.
The paper addresses the lack of effective procedures to verify if compilation chains meet secure compilation principles, proposing an approach based on translation validation to check one such principle.
Secure compilation aims to build compilation chains that preserve security properties when translating programs from a source to a target language. Recent research led to the definition of secure compilation principles that, if met, guarantee that the compilation chain in hand never violates specific families of security properties. Still, to the best of our knowledge, no effective procedure is available to check if a compilation chain meets such requirements. Here, we outline our ongoing research inspired by translation validation, to effectively check one of those principles.