Would like share some cool results. Using a new automated verification tool called Serval we found 15 previously unknown bugs in Linux kernel's bpf jit compilers (9 in riscv and 6 in x86).
-
-
Such bugs have serious security consequences: attackers may craft a bpf program that gets compiled to malicious instructions while passing the in-kernel verifier. As these are semantic bugs, they're hard to find; a tool must have a deep understanding of instruction semantics!
Show this thread -
A few years ago we wrote and manually verified a bpf jit compiler using the Coq interactive theorem prover (Jitk, OSDI'14). We had considered automated verification then but weren't able to make it scale. http://css.csail.mit.edu/jitk/
Show this thread -
This is made possible now by Serval, a new tool we've been developing on top of the Rosette language to scale up symbolic reasoning for systems code. https://emina.github.io/rosette/
Show this thread -
We will release the source code asap - stay tuned. Meanwhile, if you missed Emina's tutorial at CAV'19 last week, attend her keynote at ICFP'19 in August.
@lukenels_ will give a talk at SOSP'19 - feel free to find us if you're at these events.Show this thread
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.