[oldnews193]

> I am personally interested in this, as a cryptography PhD student, because the state of “provable security” is an absolute dumpster fire. In my opinion this is one particular application where machine-checkable proofs need to be established as a baseline standard.

As a non-cryptographer and generally a layman, I wonder how useful machine-checked proofs about crypto are in security. What do they tell you?

The underlying reason for my skepticism is best illustrated with Spectre: it made architecture people sweat bullets, but also rendered previous applications of formal methods less useful. What good is a formal proof that a crypto algorithm is constant-time, if it assumed a model of computation that is a research toy? You can only verify properties that you can formulate within a given semantic model. I suppose, for hardware those are way less understood than for programming languages.

(Which is not to say that formal verification is hopeless of useless as it is. Just really curious what kind of proofs a crypto person would benefit from machine-checking, and how.)

[shoemakersteve]

Wasn't Spectre a hardware-level vulnerability and not at all related to cryptography? I remember it being something along the lines of, the way the CPU cache worked could be exploited and allow an attacker to read the data it contained. Correct me if I'm wrong.

[oldnews193]

You are absolutely right! I brought up Spectre not meaning to say it's an issue for cryptography (although maybe it is? it's above my paygrade :) ), but to illustrate one issue with formal proofs in security that I am trying to resolve for myself.

Spectre is a hardware-level vulnerability, which is based on how the code executed under misspeculation (the processor makes a branch prediction, executes stuff and then figures out the prediction was wrong) leaves detectable traces in cache. Technically, that is not specified, because caches and speculative execution are not a part of architecture. This renders security proofs at higher level of abstraction not necessarily correct or simply non-applicable (think properties like whether a program executes in constant time or if it is sandboxed), if they rely on the ISA being all that there is to know about hardware. Now, Spectre specifically might be "solved" as a problem, but the proof-minded people would be concerned with how to prove that. How to prove that things like this are not a security issue: https://asplos-conference.org/abstracts/asplos21-paper148-ex...

And to do that, it turns out they need to extend the models under the hood of their proofs with speculation semantics. A non-trivial task by itself, I bet it would trigger non-trivial conceptual changes to mechanized proofs too, so this all might be a labor-intensive game of catch. Alternatively, one could raise a question about what fully formal security proofs we want. Formal proofs make explicit assumptions about the underlying model of computation. Some of those assumptions might not hold because we (incorrectly) thought we could abstract some complexities of hardware away. Is that alright for the kind of security properties we want to have proven? It might be for some, but not others.

So with this in mind, I am curious how crypto experts think about properties they want to prove for their work. What value would the crypto community seek to extract from formal proofs? Are leaky abstractions an issue for them? It's all very interesting.

[afiori]

one thing where proofs are invaluable is the security of distributed systems where you need to exhaustively consider many uncoordinated actors.