Towards a Verified Range Analysis for Java']JavaScript JITs

被引：8

作者：

Brown, Fraser

Renner, John ^{[1
]}

Notzli, Andres

Lerner, Sorin ^{[1
]}

Shacham, Hovav ^{[2
]}

Stefan, Deian ^{[1
]}

机构：

[1] Univ Calif San Diego, La Jolla, CA USA

[2] UT Austin, Austin, TX USA

来源：

PROCEEDINGS OF THE 41ST ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '20) | 2020年

关键词：

JIT verification; range analysis; !text type='Java']Java[!/text]Script;

D O I：

10.1145/3385412.3385968

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：135 / 150

页数：16