Pitchfork: detect Spectre vulnerabilities using symbolic execution, uses angr

Pitchfork is a static analysis tool, built on angr, which performs speculative symbolic execution. That is, it not only executes the “correct” or “sequential” paths of a program, but also the “mispredicted” or “speculative” paths, subject to some speculation window size. Pitchfork finds paths where secret data is used in either address calculations or branch conditions (and thus leaked), even speculatively – these paths represent Spectre vulnerabilities. Pitchfork covers Spectre v1, Spectre v1.1, and theoretically Spectre v4 (the code for v4 is here, but hasn’t been tested).


Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s