Maybe off-topic: Is formal verification viable anywhere in CPU logic design? Also, could any existing "CPU static analyzers" have caught the issue that caused Meltdown?
Edit: It looks like the answer to the first is a definite yes.
You can only verify properties you've thought of, and no-one conceived of this particular 'feature' causing issues like this until now. So I don't think formal verification would have helped: if anyone was in a position to realise the issue was worth verifying, they'd have been able to raise it without formal verification too.
Presumably of isolation features. I'm sure everyone knew what side channel attacks were and knew that formal verification could've helped find bugs in isolation. They just chose not to do it, because it's only important for high-assurance, not for your regular insecure linux/bsd/windows. And I'm sure they are not going to bother with verification even after everything.
>You can only verify properties you've thought of, and no-one conceived of this particular 'feature' causing issues like this until now.
I've read for years about supposed insecurities with branch prediction -- it just wasn't shown practically. To say that it wasn't conceived of is a little off.
Spitballing, but you'd have to prove that either no side channels exist, or that the information leaked by side channel(s) is indistinguishable from random noise, which I believe is an area of ongoing research.
CPU design is in a large part an exercise in formal verification. On the other hand it does not help you much when the bug in question is in the specification that you verify against in the first place or, as is almost certainly this case, is based on some behavior that is not specified by the specification at all.
In my mind Meltdown is a failure of implementation due to the choice to violate the logical design. If the logic of your design says "do not access ringX memory if you are not executing in ringX" then don't do it. Intel instead decided that they would access it but thought they could hide the results of that access from the process by never providing the read results. The problem is that actions always leave evidence in the physical world, simply assuming that no one could detect those actions (which was true at the time) is not the same as not committing the action. The benefit for Intel in violating the logical design rule was speed (and probably a reduction in gates) and the optimistic view that there were no consequences to the violation. Unfortunately hubris invited Nemesis to the party, as usual.
Spectre is a different problem in that the very design of speculative execution contains the seeds of its flaws so there really is no way to implement it in such a way as to avoid the intra-process snooping although the inter-process exploit may be avoidable via implementation.
Edit: It looks like the answer to the first is a definite yes.
reply