search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
198 stars 41 forks source link

lack of padding model for unpacked structs leads to soundness issues #417

Open invd opened 5 years ago

invd commented 5 years ago

After some short tests and discussion with @danieldietsch, I have the impression that Ultimate currently has no model in place to calculate the actual memory contents and memory footprint of structs that have elements which mandate padding within the struct memory area. (In-depth background).

Compilers will add unused memory bytes within or at the end of a subset of structs to improve the alignment to address boundaries, which will directly influence both the memory contents at a certain memory offset as well as the reported size of the struct.

Although not all struct configurations will trigger padding, those that do have some unexpected properties:

This can lead to unexpected behavior and real-world vulnerabilities.

One subset of the possible issues is explained here, but there are other potential bugs, e.g. simply overwriting more memory in a buffer than expected or copying data in the wrong position when using manually calculated offsets that fail to take the padding into account.

Code-wise, declaring the struct as __attribute__((packed)) prohibits packing and guarantees the expected "simple" behavior. (I also recommended clearing newly allocated structs with zeros before usage to prevent information leaks, but this is not an issue limited to structs that contain padding).

Ultimate will likely need a reworked memory model for structs as well as some parameters to adjust the default behavior for special architectures/compiler behavior. (Behavioral differences on 32<>64 bit?)

Although getting this "perfectly" right could become a complex task, I think there could be significant improvements with moderate efforts. Related topics likely include bit fields and other special memory behavior.

Code to illustrate the issue (feel free to modify and include this as a test case):

//#Unsafe
#include <stdio.h>
#include <stdint.h>
#define INIT_NONCE_SIZE         8

typedef struct __attribute__((__packed__))
{
    uint8_t nonce[INIT_NONCE_SIZE];
    uint32_t cid;
    uint8_t versionInterface;
    uint8_t versionMajor;
    uint8_t versionMinor;
    uint8_t versionBuild;
    uint8_t capFlags;
} U2FHID_INIT_RESP_PACKED;

typedef struct
{
    uint8_t nonce[INIT_NONCE_SIZE];
    uint32_t cid;
    uint8_t versionInterface;
    uint8_t versionMajor;
    uint8_t versionMinor;
    uint8_t versionBuild;
    uint8_t capFlags;
} U2FHID_INIT_RESP;

int main() {
    // "safe" variant, sizeof() == 17
    // printf("packed size: %d\n", sizeof(U2FHID_INIT_RESP_PACKED));
    // padded variant, sizeof() == 20 (!)
    // printf("unpacked size: %d\n", sizeof(U2FHID_INIT_RESP));

    // simple artificial issue: out of bounds read access if sizeof() is 20
    // Ultimate currently does not (!) detect this
    char buffer[18];
    return buffer[sizeof(U2FHID_INIT_RESP)];
}

Behavior with gcc -fsanitize=address:

ERROR: AddressSanitizer: stack-buffer-overflow on [...]
READ of size 1 at 0x7ffd8adbe824 thread T0
[...]
  This frame has 1 object(s):
    [32, 50) 'buffer' <== Memory access at offset 52 overflows this variable
[...]

Ultimate fb97592a96caa87b7399b3d23bc1b5c6c992d430 on the preprocessed (gcc -E) version of the target program:

  - PositiveResult [Line: 822]: pointer dereference always succeeds
    For all program executions holds that pointer dereference always succeeds at this location
  - PositiveResult [Line: 813]: all allocated memory was freed
    For all program executions holds that all allocated memory was freed at this location
  - PositiveResult [Line: 822]: pointer dereference always succeeds
    For all program executions holds that pointer dereference always succeeds at this location
  - AllSpecificationsHoldResult: All specifications hold
[...]
RESULT: Ultimate proved your program to be correct!

This is the case for

On the upside, at least the calculation is fast (< 8s), which makes debugging this less painful.

danieldietsch commented 5 years ago

Thank you for the in-depth report. This is definitely an open issue.

danieldietsch commented 5 years ago

Some additional reading: