CryptoForma Edinburgh

Yesterday and today saw two days of CryptoForma in Edinburgh, discussing topics including voting (where I gave a talk on our Helios work) and the latest approaches to formal verification.
A topic that spanned many talks on different topics was the difficulty of verifying exactly what a protocol does - often a tiny difference down at the bit level between a security model and what the protocol actually does can make all the difference.

A very promising solution to this problem is to verify security properties on the actual source code, as presented in an excellent tutorial by Cédric Fournet today using the F#/F7 languages.
The properties that can be expressed here are not "just" a formal model that would need a computational soundness theorem to link it to the actual code but actual cryptographic properties like IND-CPA or CCA2.

Even MS research can't prove AES to be CCA2 (and as some would no doubt point out, an asymptotic result means only so much for n=256) but one can take a modular approach: assume that the cipher in the System.Cryptography library is CCA2 and then prove an RPC protocol secure under this assumption, using something that looks suspiciously like a game hop. Except that this is all done automatically in visual studio at compile time.

The key ingredient here are refined types, comprising a base type and predicates on these that can be verified by a theorem prover. For example, "block: bytes {length = 8}".
Furthermore, one can set predicates in the execution of a primitive, for example calling MAC(key, msg) sets the implicit predicate auth(msg) and VERIFY(key, msg, mac) has the postcondition "VERIFY(key, msg, mac) = 1 => auth(msg)", which models existential unforgeability.
Where this gets really interesting is when such predicates are set at the protocol level: auth(msg) is set not when MAC is called but when the message msg should logically/semantically be authenticated by a key-holder. The same postcondition on VERIFY can now be checked relative to the whole protocol, say a client-server RPC protocol.

Of course even this technique can't guarantee secure protocols in all settings (timing side-channels are not covered, nor malware that interferes with the checked program at runtime) but it would still be a great step in the right direction if compile-time formal modelling and verification became as natural a step in protocol implementation as unit testing.