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: (GMT-07:00) Pacific Time (US & Canada) change
Wed 17 Jun
Times are displayed in time zone: (GMT-07:00) Pacific Time (US & Canada) change
16:00 - 17:00: PLDI Research Papers - Security at PLDI Research Papers live stream Chair(s): Tony HoskingAustralian National University / Data61 | ||||||||||||||||||||||||||||||||||||||||||
| 16:00 - 16:20 Talk | 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 - 16:40 Talk | Gregory J. DuckNational University of Singapore, Singapore, Xiang GaoNational University of Singapore, Singapore, Abhik RoychoudhuryNational University of Singapore, Singapore | |||||||||||||||||||||||||||||||||||||||||
| 16:40 - 17:00 Talk | Chris PorterGeorgia Institute of Technology, USA, Girish MururuGeorgia Institute of Technology, USA, Prithayan BaruaGeorgia Institute of Technology, USA, Santosh PandeGeorgia Institute of Technology, USA | |||||||||||||||||||||||||||||||||||||||||