About the Speaker
< Talk Title />
< Talk Category />
< Talk Abstract />
Ever wondered how JavaScript engines like V8 make your code run super fast? One of their tricks is to use a lot of clever analysis to simplify the code. However, there have been a lot of security issues in V8, and many of them stem from bugs in this analysis.
This talk dives into how we used formal methods – a fancy way of saying "super thorough bug checking" – to poke around in V8's C++ code. We wanted to see if we could formally verify the type analysis/range analysis of the new Turboshaft JIT engine.
We'll show you the tools and techniques we built, including how we used the ESBMC model checker to put V8's range analysis functions under the microscope.
**What you'll learn:**
- How we defined "correctness" for V8's range analysis.
- The setup we used to check V8's C++ code with bounded model checking.
- How we automatically create JavaScript examples to prove a bug exists.
- Spoiler: We found a new bug in V8's division operator!
< Speaker Bio />
Simon Gerst is a computer science student, security researcher, and GitHub (Security Ambassador | Star) with multiple CVEs to his name. He uses CodeQL to find bugs and he is a proud member of the KITCTF team. When not using CodeQL, he is breaking GitHub Actions and has found instances in repositories from GitHub, Microsoft and others.