Appendix II - Making Memory Safety a Property of the Language

Appendix II: Semantic Invariants and the Vulnerability of C

The missing concept

The central argument of this book can be expressed in a single idea:

A semantic invariant is a property that must remain true about a value, object, or relationship throughout the execution of a program if the program is to continue operating on the intended data and memory.

C is full of such invariants.

A variable called `length` may be intended to represent the number of bytes available in a buffer. A variable called `count` may represent the number of elements in an array. A pointer may be intended to identify the beginning of an allocated object. An offset may be intended to remain within that object. A pointer may be assumed to remain valid until a particular operation has completed. Two pointers may be assumed to refer to distinct regions of memory.

None of these assumptions is merely a comment about the program. They are semantic facts on which the correctness of subsequent operations depends.

The difficulty is that standard C generally does not make these relationships part of the types of the values that carry them.

C can tell us that a value has type `size_t`. It cannot, in the ordinary type system, tell us whether that value represents a number of bytes, a number of elements, an allocation size, a buffer capacity, an offset, or the length of an input.

C can tell us that a value has type `char *`. It cannot generally tell us the extent of the object accessible through that pointer, who owns the object, how long it remains alive, or whether a particular number of bytes may safely be accessed beginning at that address.

The result is not simply that C contains "unsafe operations." The deeper problem is that the semantic relationships required to make those operations safe are frequently maintained as informal obligations in the programmer's reasoning rather than as invariants enforced by the language.

This provides a common theoretical explanation for a remarkably broad family of security vulnerabilities.

Integer overflow, buffer overflow, out-of-bounds access, use-after-free, and double free are not the same bug. They occur at different points in a program and involve different immediate mechanisms. But they can often be understood as different failure manifestations of broken semantic invariants.

The vulnerability is the point at which the program's representation of reality ceases to correspond to reality.

1. What is a semantic invariant?

An invariant is a proposition that is expected to remain true throughout some region of program execution.

Consider:

size_t count;<br>size_t size;<br>char *p;<br>The C type system tells us very little about the relationships between these values.

But the programmer may be relying on a much richer set of propositions:

count represents the number of elements requested

size represents the number of bytes required for count elements

p points to storage of at least size bytes

an access at p + offset remains within that storage

length does not exceed the remaining extent

p remains valid until the access has completed<br>These are semantic invariants.

They are not necessarily visible in the declarations.

The program may nevertheless depend upon every one of them.

This distinction is fundamental.

A type says what a value is permitted to be according to the language. A semantic invariant says what that value means in the particular program and what relationships must remain true for subsequent operations to be valid.

For example:

size_t length;<br>does not mean:

length is a valid length for the buffer p<br>It means only that `length` has the C type `size_t`.

The stronger proposition is something like:

where `extent(p)` represents the amount of memory that may validly be accessed beginning at `p`.

That proposition is what makes:

memcpy(p, source, length);<br>safe.

C does not generally carry the proposition `length The programmer must establish it.

2. The semantic chain

Many memory vulnerabilities can be understood as a chain of dependent propositions.

A simplified example is:

size = count * element_size;<br>p = malloc(size);<br>q = p + offset;<br>memcpy(q, source, length);<br>At first sight, this is simply a sequence of ordinary C operations.

Semantically, however, it represents a chain:

count<br>required size<br>allocated extent<br>object identity<br>offset<br>remaining extent<br>copy length<br>valid memory access<br>Each relationship represents an invariant.

For example:

size = count * element_size<br>depends upon the invariant that `count` really represents the intended number of elements and that the multiplication produces the intended size without overflow.

Then:

p = malloc(size)<br>depends upon the invariant that the allocated size corresponds to the logical object the programmer intends to construct.

Then:

q = p + offset<br>depends upon `offset` being an appropriate position within that object.

Finally:

memcpy(q, source, length)<br>depends...