#NullconBerlin2025 | Finding Bugs in V8: A Formal Verification Approach by Simon Gerst
About this talk
In this talk, Simon Gerst explores the intricacies of finding bugs within the V8 JavaScript engine through a formal verification approach. He discusses the security vulnerabilities that have arose from bugs in the engine’s analysis processes, particularly focusing on the type and range analysis of the new Turboshaft JIT engine. Gerst presents the tools and techniques developed, including the application of the ESBMC model checker to scrutinize V8's C++ code. Attendees will learn about the definition of "correctness" for V8's range analysis, the setup for bounded model checking, and the automated generation of JavaScript examples that led to the discovery of a new bug in V8's division operator.
More from this event
See all 16 talks →
#NullconBerlin2025 | Panel: Industrial Systems In The Crosshairs: What It Really Takes To Defend OT
51:53
#NullconBerlin2025 | Stealing All macOS Sensitive Info with a Single Vulnerability by Koh
29:22
#NullconBerlin2025 | Derandomizing Kernel Object Locations w Software Hardware-Induced Side Channels
37:23
#NullconBerlin2025 | Your MCP Server Executes Commands - But From Whom? by Simcha Kosman
35:03