3 ms·
Formal verification of what? You can only verify properties you've thought of, and no-one conceived of this particular 'feature' causing issues like this until
by andrewaylett 9y ago
Formal verification of what?
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.
- zzzcpan 9y agoPresumably 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.
- serf 9y ago>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.