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 条
  • [1] Towards Specializing Java']JavaScript Programs
    Thiemann, Peter
    PERSPECTIVES OF SYSTEM INFORMATICS, PSI 2014, 2015, 8974 : 320 - 334
  • [2] Towards type inference for Java']JavaScript
    Anderson, C
    Giannini, P
    Drossopoulou, S
    ECOOP 2005 - OBJECT-ORIENTED PROGRAMMING, PROCEEDINGS, 2005, 3586 : 428 - 452
  • [3] Towards a Program Logic for Java']JavaScript
    Gardner, Philippa
    Maffeis, Sergio
    Smith, Gareth
    POPL 12: PROCEEDINGS OF THE 39TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2012, : 31 - 44
  • [4] Towards a Program Logic for Java']JavaScript
    Gardner, Philippa
    Maffeis, Sergio
    Smith, Gareth
    ACM SIGPLAN NOTICES, 2012, 47 (01) : 31 - 44
  • [5] Type Analysis for Java']JavaScript
    Jensen, Simon Holm
    Moller, Anders
    Thiemann, Peter
    STATIC ANALYSIS, 2009, 5673 : 238 - +
  • [6] Towards a type system for analyzing Java']JavaScript programs
    Thiemann, P
    PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2005, 3444 : 408 - 422
  • [7] Dynamic Flow Analysis for Java']JavaScript
    Naus, Nico
    Thiemann, Peter
    TRENDS IN FUNCTIONAL PROGRAMMING (TFP 2016), 2019, 10447 : 75 - 93
  • [8] Jivin' with (Java']Java and) Java']JavaScript
    Beck, CO
    45TH ANNUAL CONFERENCE ON IMAGINATION, INNOVATION AND COMMUNICATION, 1998, : 331 - 333
  • [9] Cyberaide Java']JavaScript: A Java']JavaScript Commodity Grid Kit
    von Laszewski, Gregor
    Wang, Fugang
    Younge, Andrew
    He, Xi
    Guo, Zhenhua
    Pierce, Marlon
    GCE: 2008 GRID COMPUTING ENVIRONMENTS WORKSHOP, 2008, : 89 - +
  • [10] Towards Logic-Based Verification of Java']JavaScript Programs
    Santos, Jose Fragoso
    Gardner, Philippa
    Maksimovic, Petar
    Naudziuniene, Daiva
    AUTOMATED DEDUCTION - CADE 26, 2017, 10395 : 8 - 25
12345