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.

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

Out of bounds memory load and stores verified by PREVAIL #492

Closed
m-tolstrup opened this issue May 17, 2023 · 3 comments
Closed

Out of bounds memory load and stores verified by PREVAIL #492

m-tolstrup opened this issue May 17, 2023 · 3 comments
Labels
invalid This doesn't seem right

Comments

@m-tolstrup
Copy link

Through fuzzing, we have generated the following programs:

mov64 r0, 0x0
arsh64 r0, r5
ldxw r3, [r1+0x1]
mov64 r4, r1
exit

Using ./ebpf-verifier/check we get:

1,0.000503,4452

Using ./ubpf/vm/test -j we get:

uBPF error: out of bounds memory load at PC 2, addr 0x1, size 4
mem (nil)/0 stack 0x7ffc14fc9870/512
0xffffffffffffffff

Similarly for store operations:

mov64 r0, 0x0
lddw r0, 0x7fffffffffffffff
stw [r1+0x4], 0x1
exit

Verified by PREVAIL, but results in:

uBPF error: out of bounds memory store at PC 3, addr 0x4, size 4
mem (nil)/0 stack 0x7fff23211110/512
0xffffffffffffffff
@m-tolstrup
Copy link
Author

The first program listed in bytecode:

7f45 4c46 0201 0100 0000 0000 0000 0000
0100 f700 0100 0000 0000 0000 0000 0000
0000 0000 0000 0000 e800 0000 0000 0000
0000 0000 4000 3800 0000 4000 0500 0100
b700 0000 0000 0000 cf50 0000 0000 0000
6113 0100 0000 0000 bf14 0000 0000 0000
9500 0000 0000 0000 002e 7374 7274 6162
002e 7379 6d74 6162 006f 626a 2d66 696c
6573 2f64 6174 612e 6f00 2e74 6578 7400
2e6e 6f74 652e 474e 552d 7374 6163 6b00
0000 0000 0000 0000 0000 0000 0000 0000
0000 0000 0000 0000 1100 0000 0400 f1ff
0000 0000 0000 0000 0000 0000 0000 0000
0000 0000 0300 0300 0000 0000 0000 0000
0000 0000 0000 0000 0000 0000 0000 0000
0000 0000 0000 0000 0000 0000 0000 0000
0000 0000 0000 0000 0000 0000 0000 0000
0000 0000 0000 0000 0000 0000 0000 0000
0000 0000 0000 0000 0100 0000 0300 0000
0000 0000 0000 0000 0000 0000 0000 0000
6800 0000 0000 0000 3800 0000 0000 0000
0000 0000 0000 0000 0100 0000 0000 0000
0000 0000 0000 0000 0900 0000 0200 0000
0000 0000 0000 0000 0000 0000 0000 0000
a000 0000 0000 0000 4800 0000 0000 0000
0100 0000 0300 0000 0800 0000 0000 0000
1800 0000 0000 0000 2200 0000 0100 0000
0600 0000 0000 0000 0000 0000 0000 0000
4000 0000 0000 0000 2800 0000 0000 0000
0000 0000 0000 0000 1000 0000 0000 0000
0000 0000 0000 0000 2800 0000 0100 0000
0000 0000 0000 0000 0000 0000 0000 0000
0000 0000 0000 0000 0000 0000 0000 0000
0000 0000 0000 0000 0100 0000 0000 0000
0000 0000 0000 0000 

@dthaler
Copy link
Contributor

dthaler commented Jun 6, 2023

Today PREVAIL assumes the context (r1) is always non-null.
https://github.com/vbpf/ebpf-verifier/blob/main/src/crab_verifier.cpp#L181 passes true as init_r1, and https://github.com/vbpf/ebpf-verifier/blob/main/src/crab/ebpf_domain.cpp#L2728 thus assumes r1 >= 1.

To my knowledge, neither Linux nor Windows defines any hooks which allow a null ctx argument to the program.

The program above uses ".text" as its code section, which is an unspecified program type. If there are program types on some platform that permit null ctx pointers, then PREVAIL could add an option to check to permit that. But otherwise, I would say it's an issue for ./ubpf/vm/test (not PREVAIL) that it is setting ctx to null.

@dthaler
Copy link
Contributor

dthaler commented Jan 4, 2024

@elazarg I believe this issue can be closed with label "invalid"

@elazarg elazarg added the invalid This doesn't seem right label Jan 5, 2024
@elazarg elazarg closed this as completed Jan 5, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
invalid This doesn't seem right
Projects
None yet
Development

No branches or pull requests

3 participants