JavaScript is the de facto language of the Web, but is notoriously error-prone to use. 65% of common bugs like undefined/null_variable_usage are DOM-related. Besides DOM, JS APIs are also expected to manipulate graphic hardware and asynchronous I/O, which makes the condition even worse. Although WebIDL provides a formal contract between JS developers and platform implementation, its expressivity is too limited to support deep checking of API misuses. We propose the eXtended WebIDL (xWIDL) language and a modular API misuses checking framework based on xWIDL. We discuss how to handle the data exchange between JS analyzer and SMT-based verifier. Finally, we test our implementation in a case study manner and report our findings on its efficiency and modularity.

Zhen Zhang is a final-year undergraduate (expected: June 2017) in USTC, who is preparing to apply for PhD program this winter. He has general interests in PL and specifically interested in topics including formal methods, concurrency verification, static analysis, software engineering, system and security. He finished a 3-month research internship during summer of 2016 in MPI-SWS working with Derek Dreyer, and also worked with Prof. Yu Zhang and Prof. Xinyu Feng in USTC-Yale Joint Research Center for High-Confidence Software in USTC.