3 ms·

Why? You should be able to mathematically prove lack of timing channels instead over whole negotiation... (For a specific CPU implementation or a set of them at

Why? You should be able to mathematically prove lack of timing channels instead over whole negotiation... (For a specific CPU implementation or a set of them at least.) It's just that even encryption library authors are not mathy enough and it takes effort to model CPUs enough. PKCS#1 RSA is likely possible to be proven broken by design...

hombre_fatal 8y ago
> It's just that even encryption library authors are not mathy enough I rest my case.
- AstralStorm 8y ago
  They can implement an algorithm. It is not the same as writing tons of pages of a machine code level automated theorem prover. Except someone wrote a library for timing proofs (including cache and memory) in Isabelle/HOL already, but it has to be combined with the recompile prover from SeL4 project. That would take some time and work.
kccqzy 8y ago
And with Intel releasing new micro-architectures all the time invalidating your proof?
- AstralStorm 8y ago
  Which is why you should use RISC-V Ariane instead which is already being timing modelled by ETH. Or work on the ARM Cortex M5 verification then run it on AMD-SP which is one. Presuming they allow you to run your own code. Likewise Intel ME... But that processor is some weird architecture. Or other external hardware - smart card or the fancy U2F.
  - detaro 8y ago
    Different RISC-V and ARM cores also have differing timing?
    - AstralStorm 8y ago
      Yes, which is why I mentioned the specific Ariane in-order application processor and specific ARM processor. If the encryption algorithm validates in SeL4 Ariane environment, it is algorithmically side channel free. However, this does not say anything about it being side channel free on x86 Linux - out of order execution, more caches, HT - all Spectre vectors. Of course the proof can be easily extended to handle other RISC-V in order cores. Proving out of order execution is hairier, a lot of work to be done. Oh, and you get to freeze the code to given validated compilation FIPS style. Any random C compiler revision can mess you up. Or rerun the prover.
      - detaro 8y ago
        Huh, I could have sworn your comment said you should use RISC-V instead. Apologies.
opportune 8y ago
yeah next time I deploy a web backend lemme figure out if I can implement timing channels in my framework and also make sure the framework authors modelled the encryption suite so that's even possible, it's not like I'm an actual software engineer getting paid to ship features instead of thinking mathematically about the encryption libraries I'm using

hombre_fatal 8y ago

> It's just that even encryption library authors are not mathy enough I rest my case.

AstralStorm 8y ago
They can implement an algorithm. It is not the same as writing tons of pages of a machine code level automated theorem prover. Except someone wrote a library for timing proofs (including cache and memory) in Isabelle/HOL already, but it has to be combined with the recompile prover from SeL4 project. That would take some time and work.

kccqzy 8y ago

And with Intel releasing new micro-architectures all the time invalidating your proof?

AstralStorm 8y ago
Which is why you should use RISC-V Ariane instead which is already being timing modelled by ETH. Or work on the ARM Cortex M5 verification then run it on AMD-SP which is one. Presuming they allow you to run your own code. Likewise Intel ME... But that processor is some weird architecture. Or other external hardware - smart card or the fancy U2F.
- detaro 8y ago
  Different RISC-V and ARM cores also have differing timing?
  - AstralStorm 8y ago
    Yes, which is why I mentioned the specific Ariane in-order application processor and specific ARM processor. If the encryption algorithm validates in SeL4 Ariane environment, it is algorithmically side channel free. However, this does not say anything about it being side channel free on x86 Linux - out of order execution, more caches, HT - all Spectre vectors. Of course the proof can be easily extended to handle other RISC-V in order cores. Proving out of order execution is hairier, a lot of work to be done. Oh, and you get to freeze the code to given validated compilation FIPS style. Any random C compiler revision can mess you up. Or rerun the prover.
    - detaro 8y ago
      Huh, I could have sworn your comment said you should use RISC-V instead. Apologies.

opportune 8y ago

yeah next time I deploy a web backend lemme figure out if I can implement timing channels in my framework and also make sure the framework authors modelled the encryption suite so that's even possible, it's not like I'm an actual software engineer getting paid to ship features instead of thinking mathematically about the encryption libraries I'm using