3 ms·
I feel this is going to be the thing which really boosts automated theory proving. Up until now it's always been a hard sell, people say "Well, I can prove it
by CJefferson 1y ago
I feel this is going to be the thing which really boosts automated theory proving.
Up until now it's always been a hard sell, people say "Well, I can prove it myself, and that's less work than getting the computer to prove it", and they weren't completely wrong.
However, now we have LLMs which can do lots of interesting work, but really can't be trusted for anything important (like an LLVM optimisation pass, for example). If those LLMs can convince a theorem prover the LLVM optimisation pass is correct, then suddenly their output is much more useful.
- tialaramex 1y agoOne concern here is that proofs don't necessarily prove what we intuitively think they do. So we need to be very careful to understand what we actually proved. The TLS 1.3 "Selfie attack" is an example of a gap between what we did prove and what we intuitively understood. The formal proof for TLS 1.3 says Alice talking to Bob gets all the defined benefits of this protocol, and one option is they have a Pre-shared Key (PSK) for that conversation. They both know the same key, in that sense it's symmetric. But the human intuition is that we're talking about an Alice+Bob key, whereas the proof says this is an Alice->Bob conversation key. If we re-use the same PSK for Bob->Alice conversations too we get the Selfie Attack, the formal proof never said we can expect that to work, it was just our intuition which confused us.
- GoblinSlayer 1y agoThe article says the proof only considered session resumption PSK, and overlooked out of band PSK, which was left for future work. Maybe if they could have a list of features, but TLS is too complex for that. Also PSK involves sending a PSK identity, which is supposed to be used to find the PSK, in particular it can be a user name, so the server can check the user name is correct.