I know everyone likes to cite that paper whenever they can, but it's not really relevant here. In this hypothetical, they give you the source but they compile it to binary. They do not provide you with the compiler or its source. The compiler can be malicious, but there's no need to hide its maliciousness - they don't even prove that the software running is in any way derived from the source they've given you! It would be a giant leap forward to have to design against KT-level shenanigans. The whole process can currently be subverted with CS 101-level jiggery pokery.