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
相关论文
共 50 条
  • [21] Java']JavaScript.
    Gillespie, T
    LIBRARY JOURNAL, 2000, 125 (13) : 146 - 146
  • [22] Java']Javanni: A Verifier for Java']JavaScript
    Nordio, Martin
    Calcagno, Cristiano
    Furia, Carlo Alberto
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, FASE 2013, 2013, 7793 : 231 - 234
  • [23] Java与Javascript
    张光业
    微电脑世界, 1996, (11) : 62 - 65
  • [24] Static Typing & Java']JavaScript Libraries: Towards a More Considerate Relationship
    Canou, Benjamin
    Chailloux, Emmanuel
    Botbol, Vincent
    PROCEEDINGS OF THE 22ND INTERNATIONAL CONFERENCE ON WORLD WIDE WEB (WWW'13 COMPANION), 2013, : 15 - 17
  • [25] Towards Fine-Grained Access Control in Java']JavaScript Contexts
    Patil, Kailas
    Dong, Xinshu
    Li, Xiaolei
    Liang, Zhenkai
    Jiang, Xuxian
    31ST INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING SYSTEMS (ICDCS 2011), 2011, : 720 - 729
  • [26] Java']JavaScript adventures
    Baldazo, R
    BYTE, 1996, 21 (08): : 117 - &
  • [27] Java']JavaScript fix
    Burge, MH
    DR DOBBS JOURNAL, 1996, 21 (08): : 12 - 12
  • [28] Java']JavaScript cookies
    Tichenor, CB
    DR DOBBS JOURNAL, 1997, 22 (05): : 42 - 45
  • [29] Java']Javascript complete
    DeLoach, S
    TECHNICAL COMMUNICATION, 1999, 46 (03) : 400 - 403
  • [30] Java']JavaScript fix
    McKenzie, N
    DR DOBBS JOURNAL, 2001, 26 (10): : 10 - 10
12345