Reply To: Grab bag of questions

– 14) Function signature tags

I know you’ve said in the past that jumping to an attacker-supplied address is very unlikely to be a problem in the Mill, because the bidirectional encoding means arbitrary addresses in executable memory are very unlikely to be valid code; but still, have you considered adding some hardening for dynamic function calls? History has proven that attackers can be a *lot* more imaginative than defenders in building exploits out of seemingly unusable flaws.

Hardening might include checks that the caller function has supplied the right number and shapes of arguments, and that the target of a dynamic function call is indeed a function and not an arbitrary EBB (for instance, it could check that the EBB starts with a stackf instruction).

– 15) Formally proving safety

Have you considered looking into formal proofs of safety?

I don’t know about processors, but the idea of formal proofs for compilers has been picking up steam lately, as exploits keep piling up.

In particular, while you’ve talked a great deal about how the Mill made Spectre-style exploits harder/impossible, do you have an actual model for what information is available to a given user through caches and side-channels, and how you might guarantee that these side-channels can’t be used to extract privileged information?

(My background here is from the Rust language, where the compiler provides guarantees that certain types of exploits can’t happen except when certain escape hatches are used. While these guarantees do hold strong in practice, there has been a major drive to figure out the formal rules the guarantees implicitly rely on, to have a better model of what code is sound and why.)