Hi,
I was looking up everywhere and could not find any mitigations for Spectre attack by the OCaml compiler! Does anyone know if there are any mitigations for different kinds of Spectre attacks Specter v1 (Spectre-PHT), v2 (Spectre-BTB), v4 (Spectre-STL) and v5 (Spectre-RSB) at the compiler level for OCaml?
Looking forward to hearing from you guys 
I have not heard of any, and I’m actually a bit confused about why you would add some to OCaml. That is, what’s your threat model?
In my understanding, the risks from Spectre are that running untrusted code that’s otherwise completely sandboxed can access memory through side-channel leaks. On Linux you can use kernel-level mitigations to defend against this for delivered binaries run by third party users. For code that runs in web browsers, the Javascript VMs implements these mitigations (so js_of_ocaml is covered).
Don’t get me wrong, defense in depth is great, just wondering if I’m missing an obvious attack surface for OCaml.
Thanks. I honestly haven’t got a specific threat model in my mind now. I just noticed that we’ve got some mitigations implemented in other compilers such as MSVC and was wondering if it’s the same case for OCaml as well.
@sahnaseredini are you perhaps thinking of the “retpoline” mitigations that were put into GCC?
I don’t understand them well enough to say if they even make sense for a language like OCaml.
They certainly do. A Spectre attack against an OCaml program would look as follows. Suppose the program calls Option.map (non-inlined) and the passed value is secret. Suppose the attacker is able to trigger a call to Option.map and pass it a function over which they have a bit of control (e.g., embedded interpreted language). Then the attacker will be able to recover the secret by polluting the branch predictor. To prevent this attack, you need the body of Option.map to be compiled using a retpoline (or some other countermeasure).
Due to the ubiquity of closures and higher-order functions in OCaml, the language is especially prone to Spectre attacks. Whether there exist some OCaml programs worth attacking that way is a different question. MirageOS perhaps?
1 Like
I remember “retpolines” were considered for inclusion in ocamlopt a while ago (@mshinwell , do you remember that?), but we thought that 1- they don’t mitigate all Spectre-like attacks, just a handful of them, and 2- they cost a lot in performance for a functional language like OCaml.