search

vbpf / ebpf-verifier

eBPF verifier based on abstract interpretation
MIT License
392 stars 43 forks source link

Pathological BPF program can force long veriifcation times #783

Open Alan-Jowett opened 2 weeks ago

Alan-Jowett commented 2 weeks ago

Test case that causes the verifier to hang

test-case: Found by fuzzing
options: ["termination"]

pre: []

code:
  <start>: |
    r0 = 0
    r1 = 10
  <loop>: |
    w1 -= 1
    if r1 > 0 goto <loop>
    exit

post: []
Alan-Jowett commented 2 weeks ago

Not sure if the time is in fact bounded, but it takes > 10 minutes

elazarg commented 2 weeks ago

We know for a fact that the current implementation of the numeric domain can diverge, due to changes I've introduced, which broke widening in some cases. I don't know if that's the underlying cause here.

Alan-Jowett commented 2 weeks ago

This appears to be related to 32bit ALU ops. If I switch it to r1 -= 1 it converges.

Alan-Jowett commented 2 weeks ago

This is actually a test case generated by DiffSpec