Detecting information disclosure caused by uninitialized struct members or padding areas?

[xx24678]

A very typical problem is something like this:

typedef struct {
    int a;
    int b;
    int c;
} foo_t;

int bar() {
   foo_t f;
   f.a = 0x1234;
   f.b = 0x56;

   return write(1, &f, sizeof(f));
}

In the above case, structure f is not fully initialized, the uninitialized value will be written to file or socket, causing information disclosure.

Another similar case would be due to uninitialized padding bytes:

typedef struct {
   int a;
   char b;
   int c;
} foo_t;

int bar() {
   foo_t f = {
        .a = 0x1234,
        .b = 0x56,
        .c = 0x7890
    }

   return write(1, &f, sizeof(f));
}

For this case the structure is explicitly initialized, however, there might be a couple padding bytes between field b and c depending on alignment. Those bytes are not initialized and will leak information.

I'm wondering if CBMC has any way to detect this kind of usages.

Thanks

[martin-cs]

CBMC does model padding data and tried to get it correct for the architecture so this is possible. Uninitialised variables are treated as non-deterministic rather than an error, so there isn't a direct flag for this. You could do something like...

foo_t test;
memset(&test, 0, sizeof(foo_t));
test = f;

uint8_t *a = (uint8_t *)&f;
uint8_t *b = (uint8_t *)&test;
for (size_t i = 0; i < sizeof(foo_t); ++i) {
  assert(a[i] == b[i]);
}
assert( *((uint64_t *)&f) == 0x1234);

Alternatively it could be possible to add a flag for this use-case.

[tautschnig]

In addition to what @martin-cs said: information leakage analysis (which includes leaking via padding) can be done via self-composition. See https://doi.org/10.1007/978-3-319-47166-2_63 for how we did this in one particular example, or consider various information-flow publications by Vladimir Klebanov.