Reference:
Fully Abstract Compilation. a little bit
Reference 1 The correctness-security gap in compiler optimization. By Vija D’Silva, Mathias Payer, Dawn Song. LangSec, 2015. ↩
Reference 1 The Next 700 Compiler Correctness Theorems (Functional Pearl). By Daniel Patterson, Amal Ahmed. ICFP, 2019. ↩
Reference 1 CompCert: A realistic, verified compiler. By verified, we mean a compiler that is accompanied by a machine-checked proof of a semantic preservation property: the generated machine code behaves as prescribed by the semantics of the source program. By realistic, we mean a compiler that could realistically be used in the context of production of critical software. Background The first compiler proof in 19672, for the compilation of arithmetic expressions down to stack machine code; and mechanically verified in 19723.
Reference 1 SVA: type checking in LLVM IR, ensure there is no type violation in the binary (IR form) code. However, backdoor style malicious compiler is out of the security model, thus will not be able to be detected. SVA is also designed to ensure that the (relatively complex) safety checking compiler does not need to be a part of the trusted computing base. The compiler can generate code in the SVA virtual instruction set, and a simple type checker can ensure that the code meets the safety requirements of SVA.
Q&A What is the tool used to verify the correctness? A proof of the correctness of a simple compiling algorithm for compiling arithmetic expressions into machine language. The definition of correctness. The formalism used to express the description of source language, object language, and compiler. The methods of proof. Ultimate goal, is to make it possible to use a computer to check proofs that compilers are correct.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?