BPF and formal verification

https://www.sccs.swarthmore.edu/users/16/mmcconv1/pl-reflection.html [www.sccs.swarthmore.edu]

2017-01-12 04:29

Intro to BPF (specifically the OpenBSD flavor, though without loss of generality) and verification.

> BPF is also a fantastic target for formal verification because it can only jump forward. This avoids the halting problem – BPF programs have a finite set of possible states and must terminate. We can therefore model BPF and analyze its programs completely rather than resorting to heuristics that give false positives.

source: L