Simon Gerst of Asymmetric Research covers bounded model checking for V8's C++ code, floating-point edge cases in range analysis that create security vulnerabilities, and automated JavaScript proof-of-concept generation from symbolic counterexamples.
JavaScript engines rely on aggressive optimization to achieve performance, with just-in-time compilers applying range analysis and type feedback to eliminate dead code and specialize operations. V8's Turboshaft compiler uses abstract interpretation to determine possible values for variables, yet subtle correctness failures in floating-point edge cases - including negative zero and not-a-number handling - create exploitable vulnerabilities that undermine browser security.
Bounded model checking with SMT solvers enables systematic verification of range analysis operators by translating C++ implementations into mathematical formulas and searching for states that violate correctness assertions.
In this session, Simon Gerst, security researcher at Asymmetric Research, will discuss:
- The setup used to check V8's C++ code with bounded model checking;
- Why floating-point edge cases in range analysis create security vulnerabilities despite extensive hardening;
- Automated generation of JavaScript proof-of-concepts from symbolic counterexamples including handling representation limits in set-to-range conversions.
Here is the course outline:
Finding Bugs in V8: A Formal Verification Approach |
Completion
The following certificates are awarded when the course is completed:
 |
CPE Credit Certificate |
