4 ms·
There is a formally verified implementation of TLS in F# (comes from Microsoft Research, if anybody cares): http://www.mitls.org http://www.mitls.org However,
by oggy 13y ago
There is a formally verified implementation of TLS in F# (comes from Microsoft Research, if anybody cares):
http://www.mitls.org http://www.mitls.org
However, there are gotchas. At this point the TLS protocol has gotten pretty complex. Even the act of just stating what the desired security property are is not simple. Furthermore, understanding what their proof means requires you to go through at least two of their papers (and probably both of their tech reports to grok it fully). Then you need to look at the code itself and the different assertions/assumptions spread throughout, and make sure that those conform to the properties you expect. Even if you are familiar with the field, starting from scratch would probably take you a couple of weeks, just to gain confidence that what they prove is correct. And it might be possible that there are some features of TLS that they don't implement (as you can tell, I haven't taken the couple of weeks to fully understand their stuff).
- JabavuAdams 13y agoSounds complicated. Let's just build an AI that can program, and trust it when it says it's not spying on us.
- kyllo 13y agoMy assumption would be that this formally verified implementation is not optimized, and therefore runs rather slowly compared to the C implementations. Plus it requires the .NET framework or Mono to run it. Am I off base?
- chriswarbo 13y agoI would imagine it is 'optimised for verification' rather than for speed, ie. the code will be written to follow the structure of the specification. However, the nice thing about having a verified implementation is that it can be used as the specification (reference implementation) for any other optimisations you want to make. Such a two-step process is usually much more tractable than trying to verify optimised code directly. This is used extensively by BedRock ( http://plv.csail.mit.edu/bedrock/ http://plv.csail.mit.edu/bedrock/ ) which uses functional programs as specifications and an assembly-like language for the "real"/optimised implementation. The resulting verification problems are straightforward enough to be mostly automated.
- oggy 13y agoNo, you're right on target. They are using non-optimized data structures, and rely on (Bouncy Castle's) managed code for encryption. From their paper, the throughput is around 10x slower than OpenSSL (but much closer to JSSE). My guess is that one could probably speed this up significantly, while still retaining the guarantees, but that's probably less interesting to these guys. As for Mono or .NET, I assume so (AFAIK that's the only way to run F# applications).
- jude- 13y agoAs I said in a similar post, their proofs show that their implementation is logically correct--their implementation will behave according to their formalization of the RFCs. This says nothing about how secure it is with respect to side-channel attacks. For example, they admit that they did not model time in their proofs, so they have NOT proved that they are immune to timing attacks. Moreover, F# runs on top of the unverified CLI--bugs in the CLI can be used to break miTLS.