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 JunDisplayed time zone: Pacific Time (US & Canada) change
Wed 17 Jun
Displayed time zone: Pacific Time (US & Canada) change
16:00 - 17:00 | SecurityPLDI Research Papers at PLDI Research Papers live stream Chair(s): Tony Hosking Australian National University / Data61 | ||
16:00 20mTalk | Towards a Verified Range Analysis for JavaScript JITs PLDI Research Papers Fraser Brown Stanford University, USA, John Renner University of California at San Diego, USA, Andres Nötzli Stanford University, USA, Sorin Lerner University of California at San Diego, USA, Hovav Shacham University of Texas at Austin, USA, Deian Stefan University of California at San Diego, USA | ||
16:20 20mTalk | Binary Rewriting without Control Flow Recovery PLDI Research Papers Gregory J. Duck National University of Singapore, Singapore, Xiang Gao National University of Singapore, Singapore, Abhik Roychoudhury National 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 Porter Georgia Institute of Technology, USA, Girish Mururu Georgia Institute of Technology, USA, Prithayan Barua Georgia Institute of Technology, USA, Santosh Pande Georgia Institute of Technology, USA | ||