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. This provides a robust implementation strategy for enforcing the safety properties of SVA. Furthermore, higher-level security properties (e.g. information flow, or security automata, expressible as types can be encoded compactly in SVA code, enabling robust implementations of sophisticated security-checking strategies.)
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?