@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 …
-
-
Show 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!
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 -
-
-
This sounds great. I assume the language is Racket based given you use Rosette. Is there a paper on Serval in the works?
-
Yes it’s in Racket. We are working on the camera ready for SOSP and will post it once it’s done (end of August).
End of conversation
New conversation -
-
-
So impressive.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.