Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Incorrect simulation when indexing into array using out-of-bounds bitvector #1807

Open
RyanGlScott opened this issue Jan 26, 2023 · 0 comments · May be fixed by #1808
Open

Incorrect simulation when indexing into array using out-of-bounds bitvector #1807

RyanGlScott opened this issue Jan 26, 2023 · 0 comments · May be fixed by #1808
Assignees
@RyanGlScott
Labels
subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem type: bug Issues reporting bugs or unexpected/unwanted behavior unsoundness Issues that can lead to unsoundness or false verification
Milestone
2025T1

Comments

@RyanGlScott
Copy link
Contributor

RyanGlScott commented Jan 26, 2023 •
edited
Loading

Given this C code:

// get_last.c
#include <stdint.h>

uint8_t get_last(uint8_t* array, uint8_t size) {
    return array[size - 1];
}

And this SAW specification:

// get_last.saw
m <- llvm_load_module "get_last.bc";

let ptr_to_fresh_readonly (name : String) (type : LLVMType) = do {
    x <- llvm_fresh_var name type;
    p <- llvm_alloc_readonly type;
    llvm_points_to p (llvm_term x);
    return (x, p);
};

let get_spec size pos = do {
    // Generate a fresh array and pointer to that array
    (x, xp) <- ptr_to_fresh_readonly "x" (llvm_array size (llvm_int 8));
    
    // Call the C function
    llvm_execute_func [xp, llvm_term {{`size : [8]}}];

    // Use Cryptol to access the correct position
    let ret = {{x @ (`pos)}};
    // Return it using llvm_return
    llvm_return (llvm_term ret); 
};

last_100_ov <- llvm_verify m "get_last"  [] true (get_spec 100 99) z3;

Proving this with SAW with succeed, as expected:

$ clang -g -emit-llvm -c get_last.c
$ ~/Software/saw-0.9/bin/saw get_last.saw


[18:24:07.889] Loading file "/home/rscott/Documents/Hacking/SAW/get_last.saw"

[18:24:07.980] Verifying get_last ...
[18:24:07.990] Simulating get_last ...
[18:24:07.991] Checking proof obligations get_last ...
[18:24:08.007] Proof succeeded! get_last

Now what happens if you change the call to get_spec 100 99 to something that performs an out-of-bounds index? If you change it to get_spec 100 100:

// get_last.saw
m <- llvm_load_module "get_last.bc";

let ptr_to_fresh_readonly (name : String) (type : LLVMType) = do {
    x <- llvm_fresh_var name type;
    p <- llvm_alloc_readonly type;
    llvm_points_to p (llvm_term x);
    return (x, p);
};

let get_spec size pos = do {
    // Generate a fresh array and pointer to that array
    (x, xp) <- ptr_to_fresh_readonly "x" (llvm_array size (llvm_int 8));

    // Call the C function
    llvm_execute_func [xp, llvm_term {{`size : [8]}}];

    // Use Cryptol to access the correct position
    let ret = {{x @ (`pos)}};
    // Return it using llvm_return
    llvm_return (llvm_term ret);
};

last_100_ov <- llvm_verify m "get_last"  [] true (get_spec 100 100) z3;

Then you will get an index out of bounds error during simulation, which is also expected:

$ ~/Software/saw-0.9/bin/saw get_last.saw


[18:25:05.880] Loading file "/home/rscott/Documents/Hacking/SAW/get_last.saw"

[18:25:05.976] Verifying get_last ...
[18:25:05.977] Simulating get_last ...
[18:25:05.979] Checking proof obligations get_last ...
[18:25:05.980] Run-time error: at: index out of bounds

Now let's make one last change. Let's change {{x @ (`pos)}} (which indexes into the x array using an integer) to {{x @ (`pos : [8])}} (which indexes into the x array using a bitvector):

// get_last.saw
m <- llvm_load_module "get_last.bc";

let ptr_to_fresh_readonly (name : String) (type : LLVMType) = do {
    x <- llvm_fresh_var name type;
    p <- llvm_alloc_readonly type;
    llvm_points_to p (llvm_term x);
    return (x, p);
};

let get_spec size pos = do {
    // Generate a fresh array and pointer to that array
    (x, xp) <- ptr_to_fresh_readonly "x" (llvm_array size (llvm_int 8));

    // Call the C function
    llvm_execute_func [xp, llvm_term {{`size : [8]}}];

    // Use Cryptol to access the correct position
    let ret = {{x @ (`pos : [8])}};
    // Return it using llvm_return
    llvm_return (llvm_term ret);
};

last_100_ov <- llvm_verify m "get_last"  [] true (get_spec 100 100) z3;

This shouldn't change much, but surprisingly, this causes the prove to succeed (erroneously!):

$ ~/Software/saw-0.9/bin/saw get_last.saw


[18:27:34.472] Loading file "/home/rscott/Documents/Hacking/SAW/get_last.saw"
[18:27:34.560] Verifying get_last ...
[18:27:34.561] Simulating get_last ...
[18:27:34.562] Checking proof obligations get_last ...
[18:27:34.575] Proof succeeded! get_last

Digging into this a bit, the culprit is saw-core's selectV function. I will submit a patch shortly.
@RyanGlScott RyanGlScott added type: bug Issues reporting bugs or unexpected/unwanted behavior subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem labels Jan 26, 2023
@RyanGlScott RyanGlScott self-assigned this Jan 26, 2023
RyanGlScott added a commit that referenced this issue Jan 26, 2023
@RyanGlScott
saw-core: Fix bug involving incorrect maximum values in selectV
761ee4f 
The `selectV` function had a `maxValue` argument that, in principle, was
supposed to represent the largest possible value of the index argument (treated
as a big-endian list of bits). In practice, however, this was always given the
length of the vector being indexed into minus 1! This led to subtle issues
where indexing vectors with seemingly out-of-bounds indices would succeed,
since the index value would be clamped to the length of the vector minus 1,
which is always in bounds.

This patch fixes the bug. Moreover, it turns out that the `maxValue` argument
is not actually needed to do `selectV`'s job, as its implementation always
upholds the invariant that the bitmask that it computes never exceeds the
largest possible value of the index argument. To make the code simpler, I have
removed the `maxValue` argument entirely, and I have added some more comments
in `selectV` in `saw-core`, as well as its cousins in `saw-core-sbv` and
`saw-core-what4`, to explain why this works.

Fixes #1807.
@RyanGlScott RyanGlScott linked a pull request Jan 26, 2023 that will close this issue
Draft
@RyanGlScott RyanGlScott mentioned this issue Feb 9, 2023
Open
@sauclovian-g sauclovian-g added the unsoundness Issues that can lead to unsoundness or false verification label Nov 5, 2024
@sauclovian-g sauclovian-g added this to the 2025T1 milestone Nov 5, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@RyanGlScott RyanGlScott

Labels
subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem type: bug Issues reporting bugs or unexpected/unwanted behavior unsoundness Issues that can lead to unsoundness or false verification
Projects
None yet
Milestone
2025T1
Development

Successfully merging a pull request may close this issue.

saw-core: Fix bug involving incorrect maximum values in selectV GaloisInc/saw-script
2 participants
@RyanGlScott @sauclovian-g