4 ms·

One might hope you have a formal spec of a cryptographic library.

• msla 7y ago
  > One might hope you have a formal spec of a cryptographic library. Which would be a good first step, but wouldn't protect against timing attacks or Spectre-like hardware frailties. A solid start is better than nothing, but a false sense of security is worse than nothing.
  • mcguire 7y ago
    Is crypt32 supposed to be secure against timing attacks?
• rtpg 7y ago
  While proving code matches a spec is very helpful, it's only as helpful as the spec being "correct" from a "does what we want it to do" angle. For example, you could do a bunch of spec proving on CPUs, but you wouldn't catch something like Spectre if your definition of correctness didn't include "no information leakage can happen through timings on branch prediction". And even then! You need to have the right definition on that front! Having specs and formally proven code helps to make sure your code isn't prone to a certain class of errors (just like bounds checking/lack of raw pointers prevents another class of errors), but it's not a magical catch-all. Especially if you are in a space like cryptography where you're trying to assert negatives (that end up being held up by assumptions around feasibility of certain things)
  • simion314 7y ago
    >but you wouldn't catch something like Spectre i I don't think software should prove that some CPU from the future will have shortcuts that leak information, CPU guys should prove their hardware is also safe.
    • MauranKilom 7y ago
      Sure, but I believe the point was that e.g. timing attacks might not be part of your proof but still be a real threat.
• dmichulke 7y ago
  Given the current state of security practices, I'd say we're lucky if they have unit tests.
• achamayou 7y ago
  https://project-everest.github.io/ https://project-everest.github.io/