Eau Claire

Eau Claire is a tool designed to find errors in C programs that could result in security breaches. It uses a theorem prover, Simplify (version for linux here), to perform a static analysis of each function in the program being analyzed. This page gives an overview of Eau Claire in action. If you'd like to read more, please visit my publications page.

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.

The basics
Static checking vs. software testing
Using specifications
Finding buffer overflow errors (Specifications for common string functions are here.)

Although Eau Claire makes use of techniques that are often used by verification tools, Eau Claire IS NOT a program verifier. Just because Eau Claire doesn't report any errors doesn't mean that a program is correct or even secure. Throwing off the yoke of soundness allows the tool to focus on it's true purpose: finding security flaws.

The basics

Eau Claire automatically checks for array bounds errors and null pointer dereferences. Given the function

int GetValue(int index)
{
  static int array[10];
  int returnMe = 0;

  returnMe = array[index];
  return returnMe;
}

Eau Claire reports

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.

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:

int GetValue(int index)
{
  static int array[10];
  int returnMe = 0;

  if (index < 10)
    returnMe = array[index];
  return returnMe;
}

to which Eau Claire responds

processing 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.

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 yield

int GetValue(int index)
{
  static int array[10];
  int returnMe = 0;

  if (index < 10 && index >= 0)
    returnMe = array[index];
  return returnMe;
}

to which Eau Claire says

processing function "GetValue"
1: Valid.

There are no more array bounds problems.

Static checking vs. software testing

The most common method for validating a program is by testing it--stimulating a running program and evaluating its response. Testing is a necessary part of creating good software, but it is often insufficient, especially when security is an issue. One particularly troublesome topic is determining when to stop testing: how much is enough? Code coverage metrics attempt to address this problem by associating a measure of completeness with a program and a set of tests.

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.

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();
}

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.

Now consider a very similar function:

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();
}

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 ViolateSecurityPolicybeing 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.

Eau Claire, on the other hand, readily discerns between the two functions.

processing 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.

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 yields

a == b
a + 1 + c == 0
a + a + c != 0
a != c
c != 1

The only solution to this set of equations is a = 0, b = 0, and c = -1.

Using specifications

In the previous example, Eau Claire objected when the function ViolateSecurityPolicy could potentially be invoked. How did it know to do that? In order to explain to Eau Claire that ViolateSecurityPolicy is verboten, the function requires a specification. In Eau Claire, a function specification is made up of three components:

requires: a condition that must be true before the function is called (the precondition),
modifies: a list of variables that may be modified by the function, and
ensures: a condition that must be true after the function returns (the postcondition).

The specification for ViolateSecurityPolicy is simple:

/* spec ViolateSecurityPolicy()
{
  requires 0 // this function should never be called
}
*/

By requiring 0 to be true, the specification causes EauClaire to flag every potential invocation of ViolateSecurityPolicy.

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:

/*

spec Add(a,b)

{

  ensures $return == a + b : "the return value is the sum of the arguments"

}

*/

int Add(int a, int b);

When Eau Claire processes the following (poorly implemented) function definition,

#include "Add.h"
int Add(int a, int b)
{
  int c=2;
  return a + b + c;
}

it objects because the function does not meet its specification:

processing function "Add"
Counterexample labels (|ensures: "the return value is the sum of the arguements"|

1: Invalid.

Changing the function definition to

#include "Add.h"
int Add(int a, int b)
{
  int c=0;
  return a + b + c;
}

appeases the tool:

processing function "Add"
1: Valid.

When Add is called, Eau Claire assumes that the ensures condition is met regardless of Add's implementation:

#include "Add.h"
void AddClient()
{
  int x, y;

  if (Add(x,y) != x + y)
    ViolateSecurityPolicy();
}

processing function "AddClient"
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.

Finding buffer overflow errors (string problems)

One of the most common methods used to break into computers involves overflowing a fixed-size string buffer. Once Eau Claire has specifications for common string manipulation functions, it can identify potential buffer overflow errors. Specifications for strcpy, strlen, and strcmp are here.

The following example also makes use of another function, assert, which requires only that its single argument be non-zero.

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);
}

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.

Eau Claire's counterexample for this function is long because it treats every character in the string as a separate value.

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.

Changing buffer to be large enough to hold all of message solves the problem.

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.