[pqwy]

Aaah, but you can try to do soooo much more!

You can try to confuse the ASN.1 parser, or even the protocol level parser.

You can try to defeat certificate validation logic.

You can try to get handshake state-machine do an illegal transition.

You can try to smash its memory and either read it or get your code into it.

You can try to defeat its RNG.

It doesn't let you do adaptive-plaintext attacks, but everything else is up for grabs. And you don't necessarily have to wait for it to politely send you the bitcoin key - it's somewhere in there, in memory!

[wsxcde]

I think you you guys have formally proven some of this correct? What did you use? Was a proof-assistant like Coq or a model checker or similar? And what properties have been proven correct (so we know what to avoid wasting time on :)?

[pqwy]

No, or at least not yet. :)

You are probably thinking of these guys: http://www.mitls.org.

They have a killer TLS, but it drags the entire CLR in.

We are these guys: http://openmirage.org/blog/introducing-ocaml-tls.

[wsxcde]

You are right, I was thinking of miTLS.