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).
-
Show this thread
-
@lukenels_'s patches to fix these bugs have been upstreamed. https://git.kernel.org/linus/1e692f09e091 … https://git.kernel.org/linus/46dd3d7d287b … https://git.kernel.org/linus/68a8357ec15b … https://git.kernel.org/linus/6fa632e719ee …1 reply 1 retweet 9 likesShow this thread -
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!
2 replies 2 retweets 14 likesShow 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/
1 reply 2 retweets 12 likesShow 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/
1 reply 4 retweets 24 likesShow 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.
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.