GoKawiilAppendix II: A Theory of Semantic Invariants - From C Vulnerabilities to Memory-Safe Language Design
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.
... continue reading