We present VeRA, a system for verifying the \emph{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.
%
Wed 17 Jun Times are displayed in time zone: Pacific Time (US & Canada) change
Wed 17 Jun
Times are displayed in time zone: Pacific Time (US & Canada) change
16:00 - 17:00 | SecurityPLDI Research Papers at PLDI Research Papers live stream Chair(s): Tony HoskingAustralian National University / Data61 | ||
16:00 20mTalk | Towards a Verified Range Analysis for JavaScript JITs PLDI Research Papers Fraser BrownStanford University, USA, John RennerUniversity of California at San Diego, USA, Andres NötzliStanford University, USA, Sorin LernerUniversity of California at San Diego, USA, Hovav ShachamUniversity of Texas at Austin, USA, Deian StefanUniversity of California at San Diego, USA | ||
16:20 20mTalk | Binary Rewriting without Control Flow Recovery PLDI Research Papers Gregory J. DuckNational University of Singapore, Singapore, Xiang GaoNational University of Singapore, Singapore, Abhik RoychoudhuryNational University of Singapore, Singapore | ||
16:40 20mTalk | BlankIt Library Debloating: Getting What You Want Instead of Cutting What You Don’t PLDI Research Papers Chris PorterGeorgia Institute of Technology, USA, Girish MururuGeorgia Institute of Technology, USA, Prithayan BaruaGeorgia Institute of Technology, USA, Santosh PandeGeorgia Institute of Technology, USA | ||