Look into binary correctness verification

[sbellem]

Problem

How can we be sure that the trusted source code was correctly compiled? How can we be sure that the enclave binary is a correct compilation of the source code, and thus preserves the properties which are trusted?

Remote attestation allows a user to gain trust that a remote computer is running the expected source code, on genuine and up-to-date hardware. When an enclave binary is loaded in the protected memory region, a measurement is performed, which yields a cryptographic hash, known as MRENCLAVE. This hash uniquely identifies the loaded code, and is included in the remote attestation report. A verifier can consequently compare the MRENCLAVE in the report with the trusted MRENCLAVE. The trusted MRENCLAVE can be established by using a toolchain to build the enclave binary from the trusted source code, and simulating the measurement with Intel's sgx sign tool which will yield a data structure known as SIGSTRUCT, which contains the MRENCLAVE. The verifier and enclave developer must agree on the toolchain in the sense that the toolchain must yield reproducible builds, meaning that building the enclave binary from the same source code should yield the exact same MRENCLAVE.

The toolchain proposed by linux-sgx and auditee use nix as it provides strong reproducibility guarantees. However, the fact that a build is reproducible does not guarantee that it was correctly compiled, meaning that the compiler did not introduce some kind of deviations from the source code such that although one may trust the source code, one would not trust its "faulty" binary
representation.

Hence, the question: "How can we make sure that the compiler used was not faulty?"

For a somewhat detailed idea of what this is about see section 3.1 and more particularly subsection Translation validation in https://sel4.systems/About/seL4-whitepaper.pdf: