4 ms·

Formal methods are widely used in processor design. It is hard to formalize specs to assert behaviors that bugs we haven't thought about don't exist. At least h

• nextaccountic 3y ago
  I know. I mean applying formal methods to this specific problem of proving side channels don't exist (which seems a very hard thing to do and might even require to modify the whole design to be amenable to this analysis)
  • less_less 3y ago
    As a tidbit, this was part of how one of the teams involved in the original Spectre paper found some of the vulnerabilities. Basically the idea was to design a small CPU that could be formally shown to be free of certain timing attacks. In the process they found a bunch of things that would have to change for the analysis to work... maybe in a small system those wouldn't actually lead to vulnerabilities, but they couldn't prove it (or it would require lots of careful analysis). And in big systems, those features do lead to vulnerabilities.
    • nextaccountic 3y ago
      That's amazing! Do you have some link about the designed CPU?
      • less_less 3y ago
        I'm not sure it ever got built! The Spectre stuff was found during the "how would we even begin to do this" phase. I've seen a fair amount of academic work about formally verifying RISC-V cores though.