[langsec-discuss] cross-posting a bit on Heartbleed

William Sargent will.sargent at gmail.com
Fri Apr 11 15:40:05 UTC 2014

> Actually the protocol *did* specify that:
> https://tools.ietf.org/html/rfc6520#section-4
> #   If the payload_length of a received HeartbeatMessage is too large,
> #   the received HeartbeatMessage MUST be discarded silently.

There is a formally verified version of TLS, miTLS.  I’d be curious to see how it measures up against the attack tools.


miTLS is a verified reference implementation of the TLS protocol. Our code fully supports its wire formats, ciphersuites, sessions and connections, re-handshakes and resumptions, alerts and errors, and data fragmentation, as prescribed in the RFCs; it interoperates with mainstream web browsers and servers. At the same time, our code is carefully structured to enable its modular, automated verification, from its main API down to computational assumptions on its cryptographic algorithms.

Our implementation is written in F# and specified in F7. We present security specifications for its main components, such as authenticated stream encryption for the record layer and key establishment for the handshake. We describe their verification using the F7 refinement typechecker. To this end, we equip each cryptographic primitive and construction of TLS with a new typed interface that captures its security properties, and we gradually replace concrete implementations with ideal functionalities. We finally typecheck the protocol state machine, and thus obtain precise security theorems for TLS, as it is implemented and deployed. We also revisit classic attacks and report a few new ones.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.langsec.org/pipermail/langsec-discuss/attachments/20140411/7775a30a/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <https://mail.langsec.org/pipermail/langsec-discuss/attachments/20140411/7775a30a/attachment.pgp>

More information about the langsec-discuss mailing list