|
@pchaigno | |||||
|
And a third (proof-of-concept) BPF verifier! In this paper, @lukenels_ et al. explain how they automatically transform a BPF interpreter into a BPF verifier using symbolic execution. They then use it to find 15 bugs in Linux's JIT compilers! unsat.cs.washington.edu/papers/nelson-… pic.twitter.com/3M38wie0Y8
|
||||||
|
||||||
|
Paul Chaignon
@pchaigno
|
9. lis |
|
The code for the BPF interpreter is available at github.com/uw-unsat/serva… and written in Rosette, an extension of the Racket language. unsat.cs.washington.edu/projects/serval has lots of other references and details.
|
||
|
|
||