Channels ▼
RSS

Open Source

After Heartbleed: A Look at Languages that Support Provability


It seems like every week or so, we are reading about some new software disaster (often described as a "glitch" in the press) caused by a bug in a program. Recently publicized incidents include recalls of cars due to a significant error in the control software, and shortly before that, the security hole in many Apple operating systems. The "glitch du jour" is a little more spectacular: the Heartbleed bug has caused a security hole in literally tens of millions of devices from dozens of manufacturers. This is a particularly disturbing defect because there is no way to tell if some malevolent intruder has taken advantage of it.

These and other similar bugs have been the subject of extended discussions in the technical software community, with a particular focus on how they might be prevented in future. We will consider one narrow question in this article: Can the use of a more appropriate programming language prevent or at least reduce the chance of such errors?

The specific bug in Heartbleed is a typical mistake in C code: the failure to perform a bounds check. C has no notion of bounds checking, so unless the programmer is careful to insert explicit checking code, the result can be undefined. Most programming languages (since the introduction of Fortran) have had some notion of "undefined," meaning that the language just doesn't say what happens. There was an entertaining discussion of this subject in the Algol-68 community back in the 1960s. Gerhardt Goos asked what "undefined" meant, and Charles Lindsay replied that "it could be anything, perhaps unimaginable chaos," to which Gerhardt asked, "and how do I implement unimaginable chaos in my compiler." Typically, the answer is that compilers steam ahead assuming nothing is undefined. If they assume wrong, then the generated code can indeed result in arbitrary chaos. In the case at hand, the arbitrary chaos came to be known as the "Heartbleed" bug, allowing confidential memory contents to be read by unauthorized users.

Built-in Bounds Checking

Could the use of some other programming language have helped? Definitely yes. In many languages, out-of-bounds references simply cannot happen: References are checked at compile time or, if necessary, with runtime code. The program is not allowed to proceed if an out-of-bounds situation is detected. Interestingly, such languages have been around for decades. Pascal introduced a notion of checked subtypes in the early 1970s and, a decade later, Ada extended this concept to cover many other runtime checks. Ada also included the notion of user-defined exceptions to handle runtime errors resulting from the violation of these and other checks. (Readers familiar with programming language history may know that both these notions have been around even longer.)

If the OpenSSL code had been written in Ada, for example, using the normal default mode with the compiler generating bounds checks, then there would have been no security vulnerability. Instead, an intruder could have at worst caused the code to terminate, requiring perhaps a restart of the affected process — but that's much better than allowing an undetected system intrusion.

Going Beyond Ada's Checks

It has now been more than 30 years since the first Ada compiler was validated, so we can reasonably ask whether we can do even better in designing languages that help avoid the occurrence of errors in programs. There are two weaknesses in the Ada approach. First, Ada's predefined exceptions cover only a subset of things that can go wrong. True, we can avoid integer overflow and buffer overrun errors, two of the most common sources of vulnerabilities in C programs, but that's hardly the whole world of possible errors. Suppose for example, we decide to encode a month and day in an integer as a single value so that 621 means June 21. In Ada we could write:

    type MonthDay is range 101 .. 1231;

This range would catch some invalid values such as 1301, but it would not detect in-between values such as 1095. In an article in Dr. Dobb's on the latest version of Ada, Ada 2012, we discussed the use of contracts — including predicates, preconditions, post-conditions, and other kinds of assertions — to extend the kinds of conditions that will be checked. As an example of a predicate in Ada 2012, we can write:

  type MonthDay is new Integer with
     Static_Predicate => MonthDay in 101 .. 131 | 201 .. 229 …. | 1201 .. 1231;

Now, an attempt to assign a value of 1095 to a variable of this type will cause a runtime exception. The use of preconditions and postconditions for subprograms allows arbitrary conditions to be specified that are required to be met on the call to a subprogram and, respectively, guaranteed to be true on the return.

That's a big step forward, and indeed the contracts feature makes Ada 2012 a major advance over previous versions of the language. But it's not enough, and that brings us to the second issue. Although the use of Ada could have reduced the seriousness of Heartbleed, it's really not satisfactory to let intruders cause your program to abort. It's one thing if it means you have to reboot your server, but it's quite another if the system in question is the critical software controlling a car or a plane. In such situations, it doesn't do much good to detect the problem at runtime. If you are driving along at 70 miles an hour, and you suddenly lose steering control, you are hardly going to be satisfied by seeing a message on your console saying that an out-of-bounds index has been detected.

So how can we do better still? The obvious point is that we want to know in advance, as we build and compile the program, that it is impossible for such errors to occur at runtime. Looking at the declaration above, we don't want to think of this as "please check at runtime that any assignment to a MonthDay variable meets this predicate." Instead, we want to think of this as meaning "please guarantee that the program cannot possibly attempt an assignment of an invalid value." Our focus shifts from checking for errors at runtime to proving at compile time that no errors can occur.


Related Reading


More Insights






Currently we allow the following HTML tags in comments:

Single tags

These tags can be used alone and don't need an ending tag.

<br> Defines a single line break

<hr> Defines a horizontal line

Matching tags

These require an ending tag - e.g. <i>italic text</i>

<a> Defines an anchor

<b> Defines bold text

<big> Defines big text

<blockquote> Defines a long quotation

<caption> Defines a table caption

<cite> Defines a citation

<code> Defines computer code text

<em> Defines emphasized text

<fieldset> Defines a border around elements in a form

<h1> This is heading 1

<h2> This is heading 2

<h3> This is heading 3

<h4> This is heading 4

<h5> This is heading 5

<h6> This is heading 6

<i> Defines italic text

<p> Defines a paragraph

<pre> Defines preformatted text

<q> Defines a short quotation

<samp> Defines sample computer code text

<small> Defines small text

<span> Defines a section in a document

<s> Defines strikethrough text

<strike> Defines strikethrough text

<strong> Defines strong text

<sub> Defines subscripted text

<sup> Defines superscripted text

<u> Defines underlined text

Dr. Dobb's encourages readers to engage in spirited, healthy debate, including taking us to task. However, Dr. Dobb's moderates all comments posted to our site, and reserves the right to modify or remove any content that it determines to be derogatory, offensive, inflammatory, vulgar, irrelevant/off-topic, racist or obvious marketing or spam. Dr. Dobb's further reserves the right to disable the profile of any commenter participating in said activities.

 
Disqus Tips To upload an avatar photo, first complete your Disqus profile. | View the list of supported HTML tags you can use to style comments. | Please read our commenting policy.
 

Comments:

ubm_techweb_disqus_sso_-bc51dc074fc355126d80914dd4f6d27d
2014-07-01T01:39:44

You can do contracts and invariants in any language.. just like you can have full automatic unit testing. People in general would love to have the time and money to do it.. meanwhile in the real world, projects are out sourced to developing countries for promise of cost savings and testing and conformance to specs, becomes a nightmare of horsetrading and politics


Permalink
ubm_techweb_disqus_sso_-bc51dc074fc355126d80914dd4f6d27d
2014-07-01T01:37:18

Fraid any Turing complete language will let any given developer do something stupid, that leads to "un safe". Folk said the same thing 30 years ago, before C really took off (about other languages), it's a pipe dream. Rush to deadlines and over stretched developers struggling with thorny problems, lead to problems.. always have and always will.


Permalink
ubm_techweb_disqus_sso_-bc51dc074fc355126d80914dd4f6d27d
2014-07-01T01:33:51

I think C (and C++) gets deployed where maximum portabiity and a low level efficiency to the wire/hardware are requried. When you don't mind bloat or slow execution, Java, Go, Python and others are possibilities. Efficient programs, can be clear and beautiful.. it's developer time that is lacking and the problems caused by huge software monoliths, with library piled on library in complicated threading schemes which addes to the fragility


Permalink
ubm_techweb_disqus_sso_-bc51dc074fc355126d80914dd4f6d27d
2014-07-01T01:27:46

Programmers tend to love having more time.. but ppl want everything yesterday and don't want to pay for quality


Permalink
ubm_techweb_disqus_sso_-bc51dc074fc355126d80914dd4f6d27d
2014-07-01T01:26:14

So what critical infrastructure libraries are widely deployed implemented in Eiffel?


Permalink
ubm_techweb_disqus_sso_-a3846323831671122a3bd6320325f582
2014-06-23T10:20:54

I'd beg to differ. C has poor support for ensuring that programmers use this stuff, and not great support for it in the first place.

For the software stack to be fixed, we really need to move away from languages like C to languages that have better support for safe programming.


Permalink
ubm_techweb_disqus_sso_-a3846323831671122a3bd6320325f582
2014-06-23T10:19:04

Its not really a look at *languages* that support provability. Its a look at one language that supports contracts. Further, these are not really related to "provability", rather related to verification that certain types of bugs can occur.

For other languages with similar facilities, consider Eiffel, Spec#, and D. I'm sure there are others, but those are three I'm familiar with.


Permalink
ubm_techweb_disqus_sso_-fe042295b49d46f0b32ff62dab56420c
2014-06-14T23:44:25

"If it was the actual size, then the index-to-each-byte in the buffer would exceed to array bounds and raise an error."

Actually, I thought Heartbleed was slightly different. I thought Heartbleed was like an echo test, where I give you a message, and then ask you to copy the message and send it back to me.

If an attacker declares the message to be 64kb, but only provides a source message that is 10 bytes long, then if the server allocates 64kb, but only copies the 10 bytes into 64kb buffer, then the attacker gets to see the other 63+kb of data in the buffer. So there is no bounds overflow at all.

What would have stopped Heartbleed is if memory was cleared upon malloc and/or free. But this was not done in OpenSSL. In fact, I imagine Heartbleed could be recreated in just about any language, no matter how strict, if that language was used to implement non-standard memory management routines, as was (and still is) done in OpenSSL.

So one problem is that OpenSSL did not clear memory.

Another "problem" is in the SSL protocol itself. It allows the length of the echo test message to be specified twice. One time is explicit (64kb, in the above example), the other time is implicit, due to the shorter length of the parent Heartbleed message that contains the incoming heartbeat request.

Heatbeat messages with length mismatches are malformed, and should be ignored (or responded to as an error). But this requires that the programmer compare the two lengths. Again, bounds checking and provability will not help.

If OpenSSL were written in a bound-checked language, and if it tried to copy 64kb from a 10 byte buffer, then this would cause a detectable error. But this is not how OpenSSL was implemented, so no bounds violations occurred.


Permalink
ubm_techweb_disqus_sso_-5fb97bf9cf35c3a5fab79ed34db3894a
2014-06-09T02:23:06

Chris, I totally agree, but the issues the statement where they say "In these cases, we can combine traditional testing approaches" as we all know that most software is not under rigid testing, heck even unit tests are still dark ages to many (sorry) C programmers. The article was making reference to the Heartbleed exploit, using the above would mean it would not have been found, because the Spark side, would have linked to the "classic" C program using the traditional testing methods, and most likely would not have been exposed any sooner because most people treat those "other" parts as a black box and rely on the "traditional testing" of those parts to the other side. Thus, making the Spark side, insignificant and not really a help at all.


Permalink
ubm_techweb_disqus_sso_-f818c04c206a158721044b93e4068006
2014-06-07T04:44:37

I would expect "a look at languages that support provability" to be a bit more comprehensive. There was no mention of the L4.verified microkernel project, written in Haskell and translated into a subset of C using a process proven to preserve semantics - see http://ertos.nicta.com.au/rese...

Given the pace with which software is "eating the world" (pardon the cliché), one of the most interesting questions today is how to make formal verification more affordable. A diversity of approaches helps such efforts tremendously. Publicity encourages diversity.

A broader question is whether verification will ever beat the adaptive/fault-tolerant/self-healing software paradigm (granted, they're not strictly exclusive).


Permalink
ubm_techweb_disqus_sso_-17d343bc0327a58c8d783fedd39eb094
2014-06-05T12:28:21

The advantage is that you can (and should) write the "critical" parts of the system in SPARK and less-critical parts of the system in other languages. (Classic example: A system uses SPARK to perform all algorithm implementation, data processing and management, which interfaces to a GUI written in C.) The interface requirements at the SPARK boundary force the interface to perform full checking to achieve full compliance with SPARK contracts and Ada type checks.
Or, to put it another way: yes the chain is only as strong as the weakest link. But you know where the weak link in the chain is (outside the SPARK boundary) - so you can design your system to protect the critical parts from error/attack.


Permalink
ubm_techweb_disqus_sso_-4c554988e44d7a8b602e84befb972b98
2014-06-04T21:36:53

C is fine, but the culture is not. We C programmers have a poor man mentality. We still think in therms of memory and cpu cycles economy and don't realize that modern hardware is most of the time waiting for input and has resources to spare. Besides, there is among us a competition of who writes the code with less lines that accomplishes more, or who writes the most incomprehensible one with seven operators in the same expression.


Permalink
ubm_techweb_disqus_sso_-5fb97bf9cf35c3a5fab79ed34db3894a
2014-06-04T14:20:11

Nice article, however, it dies at the end! You establish the need and desire to have a complete system understanding but then make the point that while Spark 2014 has all these great things... it does not matter because "A very important part of the SPARK 2014 approach is to accommodate programs written in multiple languages (SPARK 2014 mixed with C and full Ada, for example). In these cases, we can combine traditional testing approaches for the non-SPARK parts of the program with proof of contracts applying to the SPARK sections. " The chain is only as strong as the weakest link, thus once you mix with legacy all advantages of SPARK 2014 go away. Mixing with non-bounds, contract based software is where the bugs most likely exists, so your side could be perfect but the multiple languages side is still in an unknown state, thus you now have the same situation... invalid code and implementation.


Permalink
ubm_techweb_disqus_sso_-27ce9d23fa2734ed26247bfc71e75b29
2014-06-04T08:02:46

Let's not forget Eiffel, which combines elements of formal specification using assertions with an elegant, modern and practical object-oriented language. It embodies Bertrand Meyer's principle of Design by Contract, which falls short of proof but has a significant advantage - feasibility.


Permalink
ubm_techweb_disqus_sso_-e5eebafecfe25fbbfc1d6710902ef695
2014-06-04T06:37:26

Agreed it is not the usual buffer overflow trick of overwriting memory beyond your buffer, but it is reading memory beyond your buffer.

The server had to allocate a buffer for the incoming message (to send it back) either it would be the size of the declared size or the actual size of the message.
If it was the declared size, then no overflow would occur and no secret data would be returned.
If it was the actual size, then the index-to-each-byte in the buffer would exceed to array bounds and raise an error.

I am not sure how SPARK would help (over Ada's array bounds checking) at compile time with a run-time sized array, however a safer Heartbeat might have a fixed sized buffer limited to say 100 bytes, then SPARK could help.


Permalink
ubm_techweb_disqus_sso_-74dfca801e98d3556f3812995dc74d2f
2014-06-03T20:43:30

Only, as I understand it (which may not be very well...), the HeartBeat bug wasn't a failure to do a bounds check. It was a failure to provide a limit (a bound) to the data structure. Not quite the same thing. And it isn't clear that a 'bounds checking' language would have caught this logic problem.


Permalink

Video