Towards a verified range analysis for JavaScript JITs
Fraser Brown, John W. Renner, Andres Nötzli, Sorin Lerner, Hovav Shacham, Deian Stefan
Abstract
We present VeRA, a system for verifying the range analysis pass in browser just-in-time (JIT) compilers. Browser developers write range analysis routines in a subset of C++, and verification developers write infrastructure to verify custom analysis properties. Then, VeRA automatically verifies the range analysis routines, which browser developers can integrate directly into the JIT. We use VeRA to translate and verify Firefox range analysis routines, and it detects a new, confirmed bug that has existed in the browser for six years.
Topics & Concepts
JavaScriptComputer scienceCompilerRange (aeronautics)Operating systemWeb browserProgramming languageDatabaseSoftware engineeringThe InternetEngineeringAerospace engineeringSecurity and Verification in ComputingAdvanced Malware Detection TechniquesSoftware Testing and Debugging Techniques