Preventing heartbleed bugs with safe programming languages

http://bluishcoder.co.nz/2014/04/11/preventing-heartbleed-bugs-with-safe-languages.html

by cpeterso • 12 years ago

116 112 12 years ago

bluishcoder.co.nz

Scramblejams• 12 years ago

We really need to stop writing network code in unsafe languages, period.

djjaxe10• 12 years ago

Speed or security?... Age old question.

ibotty• 12 years ago

no. read the article.

ohazi• 12 years ago

Both!

http://rust-lang.org/

kilburn• 12 years ago

If you are speaking about execution speed, you got the idea wrong. From a quote in the article:

If you use the high level typing stuff coding is a lot more work and requires more thinking, [...] (but) you can even hope for better performance than C by elision of run time checks otherwise considered mandatory, due to proof of correctness from the type system. Expect over 50% of your code to be such proofs in critical software and probably 90% of your brain power to go into constructing them rather than just implementing the algorithm. It's a paradigm shift.

The idea is to formally prove that the code is not doing unexpected things. The process is relatively simple to understand:

First you define the assumptions you make about the program, its execution environment, and the acceptable/expected results of your program. This is known as "formal specification" of the program. It is a critical part. If your specification is wrong, then the whole approach breaks down. However, this part should be much smaller than your whole codebase, and hence you can be extra careful on it.

Next, using this specification, you write proofs showing that the code can not do anything unintended (such as accessing a buffer out of its valid range). The compiler goes through this proofs and checks that everything is provably correct (according to the specification). Then it can generate code without runtime checks that you would otherwise probably implement, because it is sure that certain things cannot happen. As a result, the code may end up being actually faster.

Although a bit involved, the idea should be pretty intuitive. It is exactly what you are doing in your mind when programming. The main differences are:

1. We humans are pretty comfortable working with inexact and/or incomplete specifications. Then some undefined behavior happens, and our programs bug out. For instance, it is very easy for us to think about the division operator as something that always yields a value, ignoring the "division by zero" edge case. Computers are not, and force you to specify what exactly should happen when you encounter such edge cases.

2. We are also pretty bad at exhaustively checking every possibility, whereas computers excel at it. With the help of human-written proofs, obviously (otherwise verifying a program would involve checking every possible input for it, which is obviously intractable).

TL;DR: The tradeoff here is between development and compilation speed versus correctness, which implies improved security and execution speed.

Dewie10• 12 years ago

No. I think that the article clearly shows:

execution speed, safety, programmer productivity ← pick any two

doublec3• 12 years ago

The type safety shown in the article doesn't come at a speed cost. The times are erased during code generation. The generated C code is much like hand crafted C but with the safety confirmed via the types.

eatfish6• 12 years ago

But even 'safe' languages have unsafe VMs. There is no question that over the years these VMs (or the runtimes) have had equally severe vulnerabilities.

The thing that really sets heartbleed apart is not the details of the bug, it's the scale of the 'infection'. OpenSSL is a core dependency of so many distributions and of so many pieces of software.

I think we could argue for lots of different solutions (diversity of implementations, safe languages, more tests) and all of them might be good in one way or another but none of them are a silver bullet for any possible bug either.

I think the take away is that you need to in a position to upgrade any part of your software stack at a moment's notice not just the obvious top-level (e.g. Rails/Django/Jetty).

iopq• 12 years ago

Rust allows you to write safe code without a VM. It is statically checked to be memory and concurrency safe.

lmm4• 12 years ago

The VM is a much smaller attack surface than all applications and all their libraries.

MichaelGG2• 12 years ago

these VMs (or the runtimes) have had equally severe vulnerabilities

I just looked at all the CVEs for .NET (62 of them). I did not find related to reading outside memory bounds or running arbitrary code. All the executable vulnerabilities were due related to loading code or escaping sandboxing: irrelevant unless you're running untrusted code in the first place.

A handful of them were due to calling out to an unsafe native library, like to render fonts.

The other serious ones were logic errors, for instance, ASP.NET returning file contents when it should not.

So while technically the VMs/runtimes have bugs, they aren't remotely the same severeness.

doublec3• 12 years ago

ATS doesn't have a VM. It compiles directly to C. The example given in the article doesn't use a runtime and the resulting C code has no more overhead than the original C.

Nursie• 12 years ago

So we offload the safety to the people that write the runtimes.

I understand that that centralises the potential problem area and may make it easier to address... but it still means that someone has to do the 'hard' bits, and if they get it wrong then everyone using the runtime is screwed. Just like what happened here (too many people depending on a single implementation).

I don't know about you, but I'm not 100% comfortable with the idea that other, cleverer people will take care of all that for me, so I don't have to worry my pretty little head about the details of what's really going on with the machine.

And look at all the JVM vulnerabilities we've seen recently...

zepolud2• 12 years ago

To take it one step further, it might be a good idea to specify the whole thing in Coq, prove correctness and derive the C code from there. Coq is a theorem prover based on the Martin-Löf type theory like the ATS mentioned in the article. Xavier Leroy (the man behind OCaml) managed to write a whole verified C compiler in Coq[1] so while it's slower than writing C directly it should still be feasible for projects of such critical importance.

On a related note, mathematicians are also finding it increasingly difficult to trust unverified proofs. Papers by Vladimir Voevodsky, a Fields medalist and one of the most prominent in the field, were also discovered to contain errors more than ten years after publication, having been cited hundreds of times and nobody noticing the errors in the proofs. This was one of the principal motivations for him to initiate the project for homotopy type theory, which also has roots in Martin-Löf type theory and is also being developed formally in Coq.

[1]http://compcert.inria.fr/diagram.png

anonymousDan• 12 years ago

It occurs to me that if I was a (black hat) hacker looking for vulnerabilities, I could reimplement critical software in a safe language, leveraging the type checker to search for bugs. Is anyone aware of people doing this already?

chriswarbo2• 12 years ago

Your reimplementation would either be very different from the original, and hence not suffer the same bugs, or the compiler wouldn't get further than a couple of function calls before giving you a cryptic error message since it doesn't understand the control flow.

Static analysis tools are useful for finding bugs in existing code, but safe programming languages won't magically point out all of the errors in some arbitrary code written in another language. They're safe precisely because they do not allow you to write code in the way that an unsafe language would.

As an analogy, if you were looking for use-after-free errors in some C code, it wouldn't do you any good to check a Python version.

fulafel• 12 years ago

You are on your way to reinventing grammar/model/spec based fuzzing. It works pretty well. Eg. it was used to find the Heartbleed bug (Codenomicon's tools at least, don't know how Google fuzzed it).

jude-5• 12 years ago

I've said it before and I'll say it again.

Formalizing the TLS specification and proving that an implementation is consistent with it only shows that the implementation is logically correct. However, it does NOT show that the implementation is secure. Your implementation can be vulnerable to side-channel attacks (particularly timing attacks) while still being logically correct.

Proofs of correctness are a (big) step in the right direction, but they're not a silver bullet for building a secure implementation.

tomp• 12 years ago

You can use mathematics to prove other things as well. You could e.g. use a special bool type for all secure data that you can't branch on, so that no secrets could be exposed by examining the runtime path of execution. Or build a model of your CPU's caching and prefetching behaviour and prove that you're code doesn't expose any secrets by that channel.

lmm4• 12 years ago

Heartbleed was not a side-channel attack. It was not a subtlety of the TLS specification. It was the single most well-known, common C-based security flaw. Better languages may not solve everything but they are absolutely the solution to this class of errors.

midas0072• 12 years ago

TLS has so many features that it factorially increases the attack surface to the size of the Milky Way.

A much simpler nonrepudiated authenticated encryption scheme implemented in a safer language would be an ideal way forward. It also would help to have a reference implementation and reference test suite to lock down behavior.

chotu3• 12 years ago

You can do specification as type in ATS2 too. My biased view is that I find ATS2 to be far more practical than using coq.

jacquesm2• 12 years ago

There will always be a compromise between cost, performance, features, usability and security.

'Safe' programming languages will improve security, presumably at the cost of usability through decreased performance. A bit like how a Ferrari is faster than a Volvo, but not as safe.

Performance has been a major driver in the choices made so far, I'm sure that the heartbleed affair will move the needle towards the 'security' end of the spectrum but I doubt it will move enough to drop C as the main work horse of systems software coding.

Reducing the complexity of the protocols used would seem to me to be a better place to reduce the exposed attack surface. No matter what the language used if you make a system extremely complex bugs are going to be more numerous and due to the interactions between the various parts much harder to detect.

zepolud2• 12 years ago

'Safe' programming languages will improve security, presumably at the cost of usability through decreased performance. A bit like how a Ferrari is faster than a Volvo, but not as safe.

This is fundamentally untrue. Safeness of the kind described in the article does not come at the cost of performance -- all type checks, invariant conditions and general formal proofs of correctness are determined at compile time. The produced code is to be indistinguishable from a correctly written, efficient C program. You are allowed to play as much as you like with direct memory accesses and use all the dirty tricks you like as longs as you can prove that the resulting program is formally correct.

What could be argued is that price you pay for all this is the difficulty of writing such programs. But definitely not their performance.

jacquesm2• 12 years ago

Ok, point taken, if you take the pre-processor or code generator approach such as in the article the performance hit might be manageable, but when I look at that 'memcpy' example I can't help but suspect that that is not a free lunch (as in, that all the extra work is done at compile time). For that you'd need to look at the code generated.

Even if there is a 0 performance hit in this case, the majority of 'safe' languages are neither pre-processors for C or code generators for a C like language (which would presumably also require the linked libraries to be re-written using something safer).

So in the specific case outlined here this may be true but in the more general case there are usually run-time trade-offs involved.

I think the key operative word in your comment is 'correctly', writing correct C is extremely hard and this approach makes it harder to create a certain class of bugs at the expense of making it harder to write the program in the first place. Tough choice, even in the absence of a performance hit!

sitkack2• 12 years ago

For anything operating over internet latencies and bandwidth, writing it in an unsafe language makes no sense. RTT will dominate, that compromise is a false dichotomy for real world scenarios a safe language will be indistinguishable in performance and orders of magnitude closer to the goal of robust encryption.

Speed gets you this, http://www.openssl.org/news/vulnerabilities.html and now where do you stand?

josteink• 12 years ago

In the age where "most" web-servers are idling at 10% load and yaaaawning most of the hours away, it makes no sense that security-critical network-code should be written in unsafe languages which can leak memory, such as C.

Due to improved hardware, we've now reached the point where we can have reasonable security and performance at the same time. We no longer need to sacrifice security by using unsafe languages. So why are we using them?

Yes some companies like Google and Facebook has busy servers, but for the rest of us, for the rest of the entire internet having to redo all our keys and certs and passwords due to a archetypical C-style bug in OpenSSL, the cost using C compared to the potential performance-benefits is absolutely not worth it. Not even close.

TLDR: Stop writing network-code in C unless you bloody well need to

spoiler• 12 years ago

With just a little bit of brain power and abstraction C can be made "safe" (assuming you don't cock up the API).

alkonaut4• 12 years ago

Certainly. But abstract it enough and the abstractions and syntax extensions required become another language. Abstract it to the point where you don't have any pointer arithmetic, a good type checker and so on, and the C code has turned into something else. Just adding wrappers around buffers to prevent overflows etc. doesn't come near the type of safety you can get in languages where you can prove formally what is going to happen when the program executes.

Before you have the kind of security you can reason about like http://www.mitls.org (rather than just abstractions for buffers etc.) it can't look like C any more.

hackerboos• 12 years ago

I think the point of TFA is that we can write this code and it will run as efficiently as C in a language which is safer than C.

pjmlp2• 12 years ago

It was already possible in the 70's with PL/I, Mesa and Modula-2, but alas they though it would be better not to offer bounds checking in the language, instead of a way to disable them if required, like the other languages.

ris• 12 years ago

Is electrical power free for you, then?

coherentpony2• 12 years ago

You can write unsafe code in any language. It's not the language's job to protect you from yourself, that's what tests are supposed to do.

chriswarbo2• 12 years ago

Actually that's what types are supposed to do ;)

Tests are still useful, as sanity checks and for checking empirical properties (eg. wall-clock time usage, timing attacks, etc.)

coherentpony2• 12 years ago

Consider the scenario where my programme is dangerous for values of an unsigned integer less than or equal to 2. As far as I know, there is no such type for unsigned integers equal to 3 or more. Sure, in object oriented languages you can essentially define your own type, but this flexibility is where you are not protected against yourself.

I see your point about types though. That said, both types and testing exist to protect you. I stand by what I said, however; languages do not exist to protect you from yourself.

ASneakyFox2• 12 years ago

I feel like every one is using heartbleed to pitch their products.

mercurial4• 12 years ago

I don't the author makes any claim to have invented ATS. But why not show why an alternative technology would have avoided this issue?

djjaxe10• 12 years ago

Just because this alternative language would have avoided this bug does not mean a much worse but would not have been created with a higher level language or even ATS.

Dewie10• 12 years ago

So Rust has unsafe code blocks that you use when you can't use the type system to enforce that a piece of code is safe. I wonder if would be viable to write those things in ATS with all the proofs to guarantee that the code is safe, compile to C and then call that trusted C code through the FFI?

It might not work in all cases, since I have the impression that unsafe Rust code is even more expressive when it comes to low level code (I guess this also means more unsafe) than C.

kibwen• 12 years ago

Rust code within "unsafe" blocks is still way, way safer than C code, while still being almost uniformly more powerful than C.

chotu3• 12 years ago

There seem to be misconception that safe language implies inefficient and slow code . It is not so in ATS2 , generated code is quite efficient and is safe even when manipulating memory from ATS2 .

pjmlp2• 12 years ago

Since the 70's we had lots of safe programming languages with native compilers to choose from

Ada, Modula-2, Modula-3, Oberon, Oberon-2, Active Oberon, Component Pascal, Delphi, Turbo Pascal, Turbo Basic, Quick Pascal, D, Haskell, OCaml, Eiffel, Go, ...

C only got widespread into the industry as a side effect of UNIX's adoption.

Nowadays we pay the price for it.

Security conscious developers should only use C when there isn't any way around it.

dorfsmay• 12 years ago

I'm trying to learn ATS right now, and indeed I immediately thought of ADA. One of the advantage of ATS is that it is a lot more functional, but far from being anywhere as mature yet.

AnimalMuppet• 12 years ago

OK, help me out here...

If I understand the heartbleed bug correctly, isn't there an RFC that it is implementing? Does the RFC say that you can ask for a length, and you get that length? That is, isn't this really a bug in the RFC?

If the security flaw's in the spec, there's not too much that the programming language can do to help you. The best it could do is point out that you're overrunning a buffer, at which point the programmer has a choice: Proceed to implement the spec in code that is declared to be unsafe (useless), scream about the spec (the right answer, and useful if anybody listens), or find some other way to generate the extra bytes that are supposed to be in the reply (which makes this implementation safe, and still satisfies the flawed spec).

Preventing heartbleed bugs with safe programming languages

Related Stories