Logical Relations and Secure Compilation for Advanced Programming Language Features using Iris

Compilers translate programs written in a high-level programming language (PL) to the low-level machine language which can be executed by the computer hardware. Modern PLs use types, to detect errors in programs, e.g., subtracting a string of characters (a term of string type) from an integer (a term of numeral type). Advanced PLs, e.g., ML, Rust, etc., are usually designed so that well-typed programs have certain desired properties. These properties are often security critical. They range from type-safety (well-typed programs will not crash) to security properties such as non-interference (well-typed programs will not reveal any information about secrets like passwords). An important property of a compiler, known as secure compilation, is that the compiler translating programs preserves these properties.
Logical relations (LR) is a versatile technique to prove properties of typed PLs and programs written in them. Recently, my collaborators and I used the Iris program logic, a state-of-the-art logic for verifying correctness of programs, to construct LR models focusing mainly on safety properties. This demonstrated that using a program logic can significantly simplify construction of LR models.
In this project I will use the LR method to tackle for the first time problems that are important for software security. In particular we will prove correctness of certain compilation strategies for PLs with features that have not been considered before.