3 ms·

I think formal methods could help designing of such machine, if you can write a mathematical statement that amounts to "there is no side channel between A and B

I think formal methods could help designing of such machine, if you can write a mathematical statement that amounts to "there is no side channel between A and B" Or at least put a practical bound on how many bits per second at most you can from any such side channel (the reasoning being, if you can get at most a bit for each million years, you probably don't have an attack) Then you verify if a given design meets this constraint

mgaunard 3y ago
A program is itself a formal specification of what an algorithm does.
- kiitos 3y ago
  Programs are implementations of specifications, they're not specifications themselves. Unless you're talking about like Coq or TLA+.
bobim 3y ago
What would be the typical size of such a constraint-based problem, and do we have the compute power to translate the rules into an implementation? And what if one forgot a rule somewhere… Deeply interesting subject.
- less_less 3y ago
  I think you'd want it to be a theorem (in Lean, Coq, Isabelle/HOL or whatever) instead of a constraint problem. So it would be more limited by developer effort than by computational power. Theoretically you can do this from software down to (idealized) gates, but in practice the effort is so great that it's only been done in extremely limited systems.
tsimionescu 3y ago
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 hard while also preserving the property of being a Turing machine.
- 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.

mgaunard 3y ago

A program is itself a formal specification of what an algorithm does.

kiitos 3y ago
Programs are implementations of specifications, they're not specifications themselves. Unless you're talking about like Coq or TLA+.

bobim 3y ago

What would be the typical size of such a constraint-based problem, and do we have the compute power to translate the rules into an implementation? And what if one forgot a rule somewhere… Deeply interesting subject.

less_less 3y ago
I think you'd want it to be a theorem (in Lean, Coq, Isabelle/HOL or whatever) instead of a constraint problem. So it would be more limited by developer effort than by computational power. Theoretically you can do this from software down to (idealized) gates, but in practice the effort is so great that it's only been done in extremely limited systems.

tsimionescu 3y ago

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 hard while also preserving the property of being a Turing machine.

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.