Show HN: Simple refined types implementation that can prevent Heartbleed | Hacker News Reader

Show HN: Simple refined types implementation that can prevent Heartbleed

github.com

56 pointstomp13 comments

20+ years of insecure code resulting in remote code execution vulnerabilities, lack of authentication and integrity, authorization bypasses and more. Yet a simple out-of-bounds read becomes the straw that breaks the camels back. Don't mistake my comment for criticism, I'm happy to see projects like this and non-security focused developers pay attention to such issues. But if you've spent more than 2 minutes in the security industry you'd be pulling your hair out at this point too.

Not sure if I understand your comment correctly, but I'd say that Heartbleed got noticed simply because it's a vulnerability that (1) affected a very large number of computers (the servers and consequently all the clients who connect to them) and (2) could have very bad consequences (TLS is one of the backbones of the internet).

Regarding this project, I know there are tools that help mitigate such issues, but unfortunately there isn't a single mainstream language that would really support this. I wanted such a language for a long time, so I (finally) decided to experiment with making one.

What's the difference between this work and for instance [1] where they use F7 and F#?

[1] Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub: Implementing TLS with Verified Cryptographic Security. IEEE Symposium on Security and Privacy 2013

Uh, thanks for this. I think I saw this before, but I haven't read it thoroughly. Skimming through it, it looks like a similar idea (but probably much more advanced). Of course, F# wasn't designed with refined types in mind, so the syntax is IMO a bit more awkward.

Can you estimate the complexity of applying this type system to the whole openssl code?

In theory, it would be quite complex, as is every refactoring of existing code. I imagine that if all the primitive functions (e.g. memcpy, malloc, etc.) would be annotated with contracts, the system could pinpoint all the places that need proof. However, most functions would need annotations; refined type inference would help with this (like [1], [2] and [3]), but I'm not sure it's advanced enough already.

In practice, this experiment isn't powerful enough for this. To support C, the refined type-checker would have to know how to reason about mutable state, and unless pointers are severely restricted, they would always enable an escape hatch (for the sloppy or rogue programmer). Projects that would help are Cyclone (an attempt at memory-safe C), Rust and VCC [4] (which, however, is focused at concurrency). Altogether, it would be much easier to start with a safer language and design for memory safety and/or verified contracts from the ground up.

So if I understand correctly, your system can prevent Heartbleed, except that it cannot analyze OpenSSL as written and that Heartbleed is a specific OpenSSL vulnerability.

Does your system prevent Ariane 5 from exploding too?

I can't change the past, I can only change the future.

I hate to be the one to break it to you, but you did not invent the idea of reducing the good behavior of programs to first-order logic properties and to apply an SMT solver to these. You are not even at the point where you might compare your false-positive rate to their false-positive rate, but if someone was going to change the future with that idea, the future of 20 years ago would have been changed.

And perhaps it was. But if SPARK83, to take one system amongst others, did not prevent Heartbleed, I don't see how your system “can prevent Heartbleed”. It can't, because Heartbleed is not written in the language at https://github.com/tomprimozic/type-systems/blob/master/refi...

Describing your github repository with the words “can prevent Heartbleed” is disingenuous and unscientific. You should keep the dramatic hyperbole for the grant proposals.

> you did not invent the idea of reducing the good behavior of programs to first-order logic properties and to apply an SMT solver to these

I know, that's why I cited a bunch of them in the README file.

Maybe this would be one good thing coming out of Heartbleed: It's easier to design (and more importantly, get people to implement) mitigations for actual disasters that have occurred and can be tested against, than do to the same for theoretical problem areas.

If we can get more libraries and implementations to be better engineered with the lessons learned from Heartbleed then that at least reduces the problem surface a bit.

The idea of this project was to (hopefully) include such a type-system in a future mainstream language (that was designed with refined types in mind, not an existing language with refined types added as an afterthought). I'm sure that libraries would follow if the tools became available.

Another problem, of course, is that SMT solvers are only a nascent field; Z3 is fast and supports many theories, but is not free (for commercial use), and other solvers (I tried Alt-Ergo and CVC4) are considerably slower and have much less features.

A lot of good things came out of Heartbleed. First and foremost, public disclosure and subsequent remediation of a serious vulnerability. Heartbleed gave us the LibreSSL project and the Linux Infrastructure Whatchamacallit funding of work on OpenSSL.

Reply on news.ycombinator.com