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
-
Replying to @bipartite
This sounds great. I assume the language is Racket based given you use Rosette. Is there a paper on Serval in the works?
1 reply 0 retweets 2 likes
Replying to @pocmatos
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).
2:27 PM - 24 Jul 2019
0 replies
0 retweets
9 likes
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.