Reports

Most sixgill reports will be false positives. The focus of the sixgill report structure is to make it easy to see in these cases where the tool got confused and which annotation is necessary to correct it. This page describes the layout of reports and how to use them.

Report Layout
Report Usage

The following sections go over complete examples of reports from Firefox.

Example #1
Example #2

Report Layout

There are three main components of a sixgill report: the trace, the dependents, and the model. We will describe each of these through a sample report (we'll revisit this report in Example #2):

arFree

1. The trace can be seen on the left side of the report, and indicates a fragment of the program's execution whose final step is the target program assertion (e.g. a buffer access). sixgill could not check that the assertion is safe within the fragment, and gave up. The trace indicates nesting for any call chains which occur, and makes loop iteration explicit. The *** separator is used when two function calls are disconnected from one another; the second call occurs after the first, but could be much later.

The trace for the above report is shown below. A call to findMemFor executes and calls arReserve, which executes at least four iterations of a loop at line 1581. After findMemFor finishes, freeRsrcOf is executed sometime later and calls arFree, which executes at least one iteration of a loop at line 1505.
findMemFor
- arReserve
-- loop:1581
--- loop:1581
---- loop:1581
----- loop:1581
- arReserve
findMemFor
***
freeRsrcOf
- arFree
-- loop:1505
2. Each point in the trace is associated with a goal, an assertion the tool is trying to prove holds, and a dependent, some other condition the tool has inferred and which it will try to prove in order to prove the goal. The goal and dependent for the selected point in the trace are shown at the top of the report. It is always the case that the dependent implies the goal. Moreover, the goals and dependents interlock; the goal in the last point of the trace is the target program assertion, and each goal at other points in the trace is required by the dependent in the next point of the trace — that goal must be proved in order for that next dependent to hold.

In the report above, the target program assertion is idx < 256 at the point of the write to ar.entry in loop:1505 (the ar.entry field is an array of 256 elements). To prove this goal, the tool inferred a dependent loop invariant initial(idx) < 256. (initial(idx) indicates the value of idx when the loop started). This dependent requires a goal to be proved at the point where arFree first reaches the loop — in order for any loop invariant to hold, it must hold when the loop starts. To prove this new goal, the tool inferred a dependent precondition idx < 256, which requires goals at each call site to arFree, and so forth.

3. The report includes a model, a path through the code for each point in the trace and an assignment of values to variables and heap terms at each point in that path. The path can be navigated by clicking on line numbers or with the step links at the top of the report, and the values assigned to variables at the current point in the path can be seen on the left side of the report. For pointers the buffer offset of the pointer will be shown instead of its actual value (these offsets are primarily for comparing the values of different pointers — offset zero has no special meaning). The value assignment in a model has two important properties: the conditions in all goals and dependents will be false, and the conditions in any annotations will be true.

Report Usage

The main question to ask when looking at a report is whether the dependents are correct — that is, whether the condition in the dependent should hold when the program runs. Starting at the assertion at the end of the report's trace, walk up the trace until the dependent is incorrect (the dependents above this will also be incorrect).

We know that this incorrect dependent implies the goal; an alternate condition (or conditions) needs to be annotated that implies the goal and is also correct. Rather than figure out whether a given annotation really implies the goal (that is the tool's job, after all), it is sufficient to simply add an annotation whose condition is false in the report's model.

Running the tool again may generate another report, but in that report the annotation's condition will be true, and whichever additional annotations are needed can be identified. With some practice an intuition can be developed as to which annotation to add to fix a report, and this iteration will usually not be necessary.

Example #1

The following is a report generated for a buffer access in the Firefox javascript engine. This code is correct, and the report is a false positive; this section shows how to determine the report is false, and how to figure out which annotations to add.

JS_ConvertArguments

The function, in a condensed form, is below. This function does some conversion on an array argv of values according to some string format. argc indicates the length of argv, and sp is used as a cursor into argv.
JS_PUBLIC_API(JSBool)
JS_ConvertArgumentsVA(JSContext *cx, uintN argc, jsval *argv,
                      const char *format, va_list ap)
{
  jsval *sp;
  char c;
  JSObject *obj;

  sp = argv;
  while ((c = *format++) != '\0') {
    if (isspace(c))
      continue;
    if (sp == argv + argc) {
      ...
      break;
    }
    switch (c) {
      ...
      case 'o':
        if (!js_ValueToObject(cx, *sp, &obj))
          return JS_FALSE;
        *sp = OBJECT_TO_JSVAL(obj);
        *va_arg(ap, JSObject **) = obj;
        break;
      ...
      default:
        format--;
        if (!TryArgumentFormatter(cx, &format, JS_TRUE, &sp,
                                  JS_ADDRESSOF_VA_LIST(ap))) {
          return JS_FALSE;
        }
        /* NB: the formatter already updated sp, so we continue here. */
        continue;
    }
    sp++;
  }
  return JS_TRUE;
}
sixgill is trying to show the write to *sp under case 'o' is safe to do, represented as the goal 0 < ubound(sp). (ubound indicates the number of elements allocated for a pointer). Looking at the report generated, the first thing it did was pick as a dependent the loop invariant 0 < ubound(sp). This loop invariant is not correct — sp may be equal to argv + argc at the head of the loop, in which case it is not safe to dereference (the loop will terminate without dereferencing it).

Another loop invariant needs to be annotated, one which is correct but is false in the report's model. A good one is ubound(argv) >= argc. This is false in the model, as can be seen from the values at the point of the write to *sp:
argc: 5
offset(argv): -4
offset(sp): 0
ubound(sp): 0 
In the model sp has an offset four more than argv and has an upper bound of zero, thus the upper bound of argv is four, less than argc. After annotating this loop invariant, the tool generates a new report, similar to the first one:

JS_ConvertArguments #2

Note though that the annotated loop invariant is true in the new report's model — argc is zero, and the upper bound of argv is four. Another loop invariant is needed, again one which is correct but is false in the report's model. A good one is sp <= argv + argc. This is false in the model, which has sp == argv + argc + 4. After annotating this loop invariant, the tool is able to check the assertion.

Of course, having annotated these loop invariants sixgill must check that they are actually true. The first loop invariant we annotated is also a precondition, and can be proved by looking at the callers to JS_ConvertArgumentsVA. The second loop invariant requires checking that TryArgumentFormatter increases sp by at most one. Neither of these should require additional annotations.

Example #2

The following link revisits the sample report we used in Report Layout. As in the first example, this code is correct and the report is a false positive. Fixing the report presents a gray area, however, and from a design standpoint the best solution may be to change the code itself.

arFree

Walking up the points in the trace, all the dependents are correct until the type invariant on Reservation that its arIndex field is less than 256. As can be seen from the rest of the report, it is possible for 256 to flow to the arIndex field so that, strictly speaking, this is not a type invariant.

The design question at hand is whether this should be a type invariant. If so, arReserve and/or findMemFor need to be changed to reflect that. If not, annotations need to be added to findMemFor, freeRsrcOf and their callers to show that a Reservation with an arIndex of 256 cannot reach freeRsrcOf. Either solution will work with sixgill; what this and similar reports provide is a way to expose such design ambiguities, and annotations can be used to clarify and describe the intended design in a checkable fashion.