Value analysis tutorial, part 4: one solution to second quiz

This post offers one answer to the second quiz from part 2. For context here are links to part 1 and part 3.

The question was: how should we get rid of the last alarm below and conclude that Skein-256 is indeed safe from run-time errors when used in the conditions previously described?

lib.c:10:[kernel] warning: out of bounds write. assert \valid(tmp);

The alarm appears when using the command-line:

frama-c-gui -val -slevel 100 -slevel-function main:0 *.c

Inspecting values inside function memcpy we can see that the problematic address is again at offset 88 inside structure skein_context. Following the same procedure as in part 3 we identify this context for the alarm inside the analysis log:

...
[value] computing for function Skein_256_Update <-main.
        Called from main.c:40.
[value] computing for function memcpy <-Skein_256_Update <-main.
        Called from skein.c:171.
lib.c:10:[kernel] warning: out of bounds write. assert \valid(tmp);
[value] Recording results for memcpy
[value] Done for function memcpy
...

Several remarks:

1. the problematic Skein_256_Update call is the call inside the while loop (at line main.c:40). This is completely unsurprising.
2. Function memcpy is called several times from Skein_256_Update but the call that results in an alarm is the call at skein.c:171.

Inspecting the incriminated call site in the GUI the address argument to memcpy is &ctx->b[ctx->h.bCnt] and the values that the analysis thinks are taken by ctx->h.bCnt at this point are 16 and 32. The length argument n is always 16. Since the array b inside struct skein_context is only 32 bytes it is normal to get an alarm inside memcpy with such arguments.

Now the reason we originally unrolled a few calls to Skein_256_Update was in order to reverse-engineer what the function was doing much as if we had inserted calls to printf inside the source code except without the need to choose in advance the values to inspect. So let us use the GUI to check the values of skein_context.h.bCnt for the first few calls.

Using "Evaluate expression" on the first call to Skein_256_Update:

Before statement:
skein_context.h.bCnt ∈ {0; }
At next statement:
skein_context.h.bCnt ∈ {16; }

On the second call:

Before statement:
skein_context.h.bCnt ∈ {16; }
At next statement:
skein_context.h.bCnt ∈ {32; }

On the third call:

Before statement:
skein_context.h.bCnt ∈ {32; }
At next statement:
skein_context.h.bCnt ∈ {16; }

On the fourth call:

Before statement:
skein_context.h.bCnt ∈ {16; }
At next statement:
skein_context.h.bCnt ∈ {32; }

On the fifth and last call before entering the loop:

Before statement:
skein_context.h.bCnt ∈ {32; }
At next statement:
skein_context.h.bCnt ∈ {16; 32; }

Do not let yourself be distracted by the last "At next statement:" information: this one is imprecise because the "next statement" is inside the while loop. Apart from that it is rather clear what is happening: each call after the first one changes the bCnt field from 16 to 32 or conversely. Inside the while loop the two values end up amalgamated together. That makes it look like there may be a problem with the memcpy call. To make it clear there is no problem we probably just need to group the calls by two. That leads us for instance to write the following main function to verify the safety of all sequences of an even number of calls to Skein_256_Update.

void main(void)
{
  int i;
  u08b_t hash[HASHLEN];
  Skein_256_Ctxt_t skein_context;
  Skein_256_Init(&skein_context  HASHLEN * 8);
      arbitrarize_msg();
      Skein_256_Update(&skein_context  msg  80);
      arbitrarize_msg();
      Skein_256_Update(&skein_context  msg  80);
  while (Frama_C_interval(0 1))
    {
      arbitrarize_msg();
      Skein_256_Update(&skein_context  msg  80);
      arbitrarize_msg();
      Skein_256_Update(&skein_context  msg  80);
    }
  Skein_256_Final( &skein_context  hash);
}

With the command-line frama-c -val -slevel 100 -slevel-function main:0 *.c the value analysis does not emit any alarm for this main(). The case of one call was already handled in the tutorial chapter of the value analysis documentation. The separate cases of 0 calls and of an odd number of calls larger than three are left to the reader and this time there will not be any further refinement of this solution in a future blog post. Ask on the mailing list if you encounter a problem finishing the verification from here.

In the next episode an alternative and more generalizable solution to the same problem. Or maybe a meta-discussion about the verification methodology being sketched out in this thread.