Hacker News Reader

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

> 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.

Is crypt32 supposed to be secure against timing attacks?

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)

>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.

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.

Given the current state of security practices, I'd say we're lucky if they have unit tests.

https://project-everest.github.io/

> how do you prove that the formal spec correctly describes what the software's supposed to do?

This is a valid point. With formal verification, the buck stops with the model. Looking at existing projects like Sel4, though, it's clearly not a knock-down argument against formal methods.

> Your proof that it has no null pointer crashes tells us nothing about whether it has off-by-one errors. For each kind of bug, you need a different proof. Did your proof cover every category of bug? Almost certainly not.

This appears to be a guess at how formal methods work. It is wrong.

Formal methods are able to take an abstract model and 'refine' it into an executable program that implements the formal model. [0] This process is mathematically watertight (ideally at least). There is no room for language-specific bugs (such as buffer overflows) to creep in.

What you don't tend to get from formal methods, is a guarantee against side-channel attacks, such as timing-based attacks. This may be a real security concern. From a quick google search, this seems to be an active area of research.

[0] https://en.wikipedia.org/wiki/Refinement_(computing)

> For each kind of bug, you need a different proof.

Not necessarily; if your definition of security and correctness is sufficiently general and if you can prove that your program conforms to those definitions, you have effectively proven your program to be secure and correct for all bugs. Unless of course your definition of security and correctness was too narrow, which as you note is where the crux of the problem is.

But this is not a hopeless task, there is a lot of active research in building axiomatic definitions of what security and correctness mean, so in theory it could be possible to prove a program 100% correct if the axioms are self-evident.