@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 …
-
-
Prikaži ovu nit
-
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!
Prikaži ovu nit -
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/
Prikaži ovu nit -
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/
Prikaži ovu nit -
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.Prikaži ovu nit
Kraj razgovora
Novi razgovor -
-
-
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).
Kraj razgovora
Novi razgovor -
-
-
So impressive.
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi
-
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.