Finding Bugs in V8: A Formal Verification Approach
summary
Formal verification of V8 Turboshaft range analysis using ESBMC bounded model checking targets the abstract addition/division operators and models IEEE floats with minus zero and NaN. The system builds a C++ verification harness, extracts counterexamples, and produces automatic JS PoC generation that reproduces the bug in the interpreter–JIT pipeline. Evaluation finds a new division bug (confirmed by V8), reproduces three historical bugs, and locates solver/timeout limits when proving full correctness.
AI-written summary · about
chapters (12)
- 0:00Introduction and motivation
- 3:59JavaScript and V8 engine basics
- 7:35Doubles and floating-point quirks
- 12:55Range analysis in V8
- 15:10Formal verification with BMC
- 20:13Verification harness design
- 22:01Automatic test case generation
- 25:33Formal verification of test generator
- 27:00Evaluation and findings
- 32:06Research conclusions and takeaways
- 33:52Technical contributions and impact
- 35:20Q&A session
related talks
32mV8 by example: A journey through the compilation pipeline
23mJoin the super secret V8 club & become a JavaScriptbender
01h 07mThe V8 Sandbox: From Compiler Correctness to Runtime Containment
28mPerformance Profiling for V8
52mStructure aware fuzzing
23mV8 Internals for JS Developers
37mReviving JIT Vulnerabilities: Unleashing the Power of Maglev Compiler Bugs on Chrome Browser
01mFrom Bugs to Breaches