Hacker News new | ask | show | jobs
by nickpsecurity 3821 days ago
More interesting than the attack itself is their overall effort of combining formal verification with protocol implementation. Along the way, they've found all these problems in the other protocols because they didn't use such rigorous methods. Quite an argument in favor of using high assurance techniques for at least critical, slow-changing protocols like TLS.

Anyway, I found this paper...

http://www.ieee-security.org/TC/SP2015/papers-archived/6949a...

...that reminds me of older, high assurance designs. The classic way to do it is the so-called abstract or interacting state machine models. Each component is a state-machine where you know every successful or failure state that can happen plus argument security is maintained. Then, you compose these in a semi-functional way to describe overall system. Seems the miTLS people did something similar for theirs that they call "composite, state machines." The result was clean implementation and verification of what got really messy in other protocol engines. Plus, new techniques for handling that of course.

Really good stuff. Worth extending and improving in new projects.
1 comments
tptacek 3821 days ago
Formal verification of protocols like TLS is essentially the research thesis behind this group at INRIA, which was also responsible for Logjam (as well as the paper you linked to).
link
nickpsecurity 3821 days ago
Oh yeah, they're kicking ass on every front of this sub-field. Then, Leroy et al are doing that for compilers and language analysis at INRIA as well. Then Astree is leading it for static analysis of C.

France, esp INRIA, seems to be in the lead on verified software with a real-world focus. It will be great when more elsewhere follow suit.

link
baby 3820 days ago
Galois just gave a talk on high assurance crypto at RWC (they made cryptol and other open sourced tools to give formal proofs of security)
link
nickpsecurity 3819 days ago
Oh yeah, Galois is another one of the greats in the field. They just keep cranking out one practical thing after another. At a higher pace than most it seems. Here are a few good things on their end.

Scrolling their blog is endless insights https://galois.com/blog/

CRYPTOL's open source page http://www.cryptol.net/

SMACCMPilot has things like Ivory language http://smaccmpilot.org/

GitHub site with 8 pages worth of their stuff https://github.com/galoisinc

link