Channels ▼

Walter Bright

Dr. Dobb's Bloggers

Memory Safety

March 19, 2008

The software industry is gripped with a plague of malware. Although there are many forms of malware, this article is about malware that gets in by exploiting software bugs that enable specially crafted user data to be executed as code. It seems there's almost a daily alert that some software package or other is vulnerable to some exploit. Whole industries have sprung up to defend our computers from it, but even anti-virus software itself is sometimes a vector for malware.

As software programmers, we have a responsibility to do what we can to make our software invulnerable to exploits. We do our best, but the parade of vulnerabilities continue. We try to be better programmers, and some have even suggested government certification of programmers to try and mitigate the problem. But obviously, something isn't working in the way we write software.

What makes software vulnerable to exploits? The most common weakness seems to be buffer overflows, or something equivalent. Carefully constructed data is fed to the program, it overflows a buffer somewhere, and then the user data is executed as code. How do we stop this? We go through our programs line by line, vetting it, looking for buffer overflows, failure to check for error conditions, wild pointers, etc. There are some automated code scanners like Coverity and Fortify, but while they find many patterns of bugs, they are not capable of guaranteeing the code is memory safe. A further problem is they are expensive and not relatively available.

What if it were possible to mathematically prove a program was not subject to malware? By this I mean it would be impossible for any user data to be executed as code. This property is called memory safety. If we could prove such a thing, we can just mechanically run source code through the prover, and if it got the green light, we're golden. No more line by line vetting, no more praying we didn't miss anything.

Doesn't this sound like a pipe dream? It does to me, how could one possibly prove such a thing? But it turns out it has been done for some languages, languages like Java. Being able to prove memory safety for a language means that proving a program memory safe is as straightforward as successfully running it through the compiler. Java has been mathematically proven to be type safe, for which memory safety is a subset. Java programs cannot have buffer overflow exploits (as long as those Java programs are 100% Java programs, and do not do things like call native DLLs that themselves might be subject to malware, and as long as the Java VM itself doesn't have bugs in it).

But Java isn't for everyone. How do can we prove memory safety in other languages, particularly the D programming language? Being a systems programming language, D has things like arbitrary pointers, so obviously memory safety is impossible. Or maybe it is possible. Bartosz Milewski has suggested that since D is a powerful programming language even without pointers, it may be practical to define a safe D subset. We are examining each feature of D to find the largest possible subset of the language that is memory safe. Then, if this subset is itself a practical language, D can be a major contribution towards eliminating

Obviously some applications will need to use non-memory safe parts of D or call into libraries that are themselves not guaranteed memory safe.  The more of
those applications that utilize the safe subset of D the less code has to under go extra scrutiny for these sorts of problems.

Thanks to Brad Roberts for his insightful comments on this.

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.