By default, Eau Claire finds array bounds errors and null pointer dereferences. In addition to the built-in checks, Eau Claire allows users to specify and check their own security properties. The following examples demonstrate some of the tool's features and capabilities.
Eau Claire reportsint GetValue(int index) { static int array[10]; int returnMe = 0; returnMe = array[index]; return returnMe; }
It identifies the array access on line 5 as a potential array bounds error because the variable index may be larger than the array bounds allow. A simple-minded fix might result in the following:processing function "GetValue" Counterexample labels (|array_bounds_overflow 6|) counterexample context (AND (NEQ |elems int| |elems int*|) (EQ (len (select |elems int*| array)) 10) (<= 10 index) (< array 0) ) 1: Invalid.
to which Eau Claire respondsint GetValue(int index) { static int array[10]; int returnMe = 0; if (index < 10) returnMe = array[index]; return returnMe; }
The modified function prevents array from being accessed with too great a value but not with too small a value (less than zero). A second fix could yieldprocessing function "GetValue" Counterexample labels (|array_bounds_underflow_7|) counterexample context (AND (NEQ |elems int| |elems int*|) (EQ (len (select |elems int*| array)) 10) (< index 0) (< array 0) ) 1: Invalid.
to which Eau Claire saysint GetValue(int index) { static int array[10]; int returnMe = 0; if (index < 10 && index >= 0) returnMe = array[index]; return returnMe; }
There are no more array bounds problems.processing function "GetValue" 1: Valid.
The metric used in this example is path coverage: the percentage of paths through the program that are exercised by the tests. Because the number of paths through a program can grow exponentially with the program's size, path coverage in its purest form isn't practical in real-world testing situations. Still, path coverage is a straightforward and rigorous metric ideal for illustrating the following problem.
The maximum path coverage obtainable for OnTheEdge is 41.2% (only 7 of the 17 possible paths are testable). The first and third assignments will never be executed in the same function invocation, and the function ViolateSecurityPolicy can never be called.void OnTheEdge(int a, int b, int c) { if (a + b + c == 0) return; if (a == b) c = 1; if (b == c) a = 3; if (a == c) b = -1; if (a + b + c == 0) ViolateSecurityPolicy(); }
Now consider a very similar function:
It's relatively easy to obtain 47.1% path coverage for OnTheEdge2 (8 of 17 possible paths), but in this function a ninth path is also possible. The invocations OnTheEdge2(0,0,-1) and OnTheEdge2(-3,0,0)are the only two calls that exercise a ninth path: one that results in ViolateSecurityPolicy being called. A tester who knew that the function OnTheEdge has a maximum coverage of 41.2% might feel justified in terminating the testing of OnTheEdge2 after obtaining the same or higher coverage and before discovering the security flaw.void OnTheEdge2(int a, int b, int c) { if (a + b + c == 0) return; if (a == b) a = 1; if (b == c) c = 3; if (a == c) b = -1; if (a + b + c == 0) ViolateSecurityPolicy(); }
Eau Claire, on the other hand, readily discerns between the two functions.
Eau Claire's output shows that OnTheEdge is safe: ViolateSecurityPolicy can never be called. For OnTheEdge2, however, ViolateSecurityPolicy can be called, and Eau Claire gives a set of conditions under which the call will take place. Eau Claire's output currently comes directly from the theorem prover and can be somewhat difficult to interpret. Translating the counterexample context into a C-like notation yieldsprocessing function "OnTheEdge" 1: Valid.processing function "OnTheEdge2" Counterexample labels (|Line 12: ViolateSecurityPolicy requires|) counterexample context (AND (EQ a b) (EQ (+ (+ 1 a) c) 0) (EQ (C_EQUAL (+ (+ a a) c) 0) 0) (EQ (C_EQUAL a c) 0) (EQ (C_EQUAL 1 c) 0) ) 1: Invalid.
The only solution to this set of equations is a = 0, b = 0, and c = -1.a == b a + 1 + c == 0 a + a + c != 0 a != c c != 1
By requiring 0 to be true, the specification causes EauClaire to flag every potential invocation of ViolateSecurityPolicy./* spec ViolateSecurityPolicy() { requires 0 // this function should never be called } */
In the more general case, a specification can be used in two ways. When Eau Claire is processing a function definition, it assumes that the requires condition for the function is true and attempts to show that the ensures condition is always true when the function returns. (It should also check that variables not on the modifies list aren't modified, but Eau Claire omits this check in its current implementation.) When Eau Claire is processing a function call, it checks to make sure that the function's requires condition is met before the call and assumes that the function's ensures condition is true after the call.
Consider the following function specification and prototype:
When Eau Claire processes the following (poorly implemented) function definition,/*
spec Add(a,b)
{
ensures $return == a + b : "the return value is the sum of the arguments"
}
*/
int Add(int a, int b);
it objects because the function does not meet its specification:#include "Add.h" int Add(int a, int b) { int c=2; return a + b + c; }
Changing the function definition toprocessing function "Add" Counterexample labels (|ensures: "the return value is the sum of the arguements"| 1: Invalid.
appeases the tool:#include "Add.h" int Add(int a, int b) { int c=0; return a + b + c; }
When Add is called, Eau Claire assumes that the ensures condition is met regardless of Add's implementation:processing function "Add" 1: Valid.
Note that Eau Claire doesn't require that a definition for every specified function. This allows for modular program checking and library-based checking. Rather than have programmers write all of their own specifications, the specifications for standard system-provided functions can simply be placed in the appropriate system header files.#include "Add.h" void AddClient() { int x, y; if (Add(x,y) != x + y) ViolateSecurityPolicy(); }processing function "AddClient" 1: Valid.
The following example also makes use of another function, assert, which requires only that its single argument be non-zero.
StringClient copies a static string into a buffer, asserts that the copy and the original are the same, modifies one of the characters in the copy, and then asserts that the two strings differ at the changed position.void StringClient() { char buffer[10]; char *message = "not a long string"; strcpy(buffer, message); assert(strcmp(buffer, message) == 0); buffer[3] = 'X'; assert(strcmp(buffer, message) == 4); }
Eau Claire's counterexample for this function is long because it treats every character in the string as a separate value.
Changing buffer to be large enough to hold all of message solves the problem.processing function "StringClient" Counterexample labels (|Line 9: StringCopy requires "the array must be large enough to hold the entire string"|) counterexample context (AND (EQ (select (select |elems char*| |$tmp0|) 10) 32) (EQ (select (select |elems char*| |$tmp0|) 13) 114) (EQ (select (select |elems char*| |$tmp0|) 1) 111) (EQ (select (select |elems char*| |$tmp0|) 14) 105) (EQ (select (select |elems char*| |$tmp0|) 2) 116) (EQ (select (select |elems char*| |$tmp0|) 15) 110) (EQ (select (select |elems char*| |$tmp0|) 3) 32) (EQ (select (select |elems char*| |$tmp0|) 4) 97) (EQ (select (select |elems char*| |$tmp0|) 5) 32) (EQ (select (select |elems char*| |$tmp0|) 8) 110) (EQ (select (select |elems char*| |$tmp0|) 11) 115) (EQ (str_len (select |elems char*| |$tmp0|)) 17) (EQ (select (select |elems char*| |$tmp0|) 12) 116) (EQ (select (select |elems char*| |$tmp0|) 0) 110) (EQ (len (select |elems char*| buffer)) 10) (EQ (select (select |elems char*| |$tmp0|) 16) 103) (EQ (C_VALID_STR |elems char*| |$tmp0|) 1) (EQ (select (store (store |elems char*| buffer |$tmp2|) buffer (store |$tmp2| 3 88)) |$tmp0|) (select |elems char*| |$tmp0|)) (EQ (len (select |elems char*| |$tmp0|)) 18) (EQ (select (select |elems char*| |$tmp0|) 6) 108) (EQ (select (select |elems char*| |$tmp0|) 9) 103) (EQ (select (select |elems char*| |$tmp0|) 7) 111) (EQ (select (store |elems char*| buffer |$tmp2|) |$tmp0|) (select |elems char*| |$tmp0|)) (EQ (C_VALID_PTR |elems char*| buffer) 1) (< |$tmp0| 0) (< buffer 0) ) 1: Invalid.
void StringClient() { char buffer[20]; char *message = "not a long string"; strcpy(buffer, message); assert(strcmp(buffer, message) == 0); buffer[3] = 'X'; assert(strcmp(buffer, message) == 4); }processing function "StringClient" 1: Valid.