The highly dynamic nature and complex semantics of JavaScript make it difficult to understand the behaviors of JavaScript programs correctly. To automatically reason about them, researchers have developed various JavaScript static analyzers that conform to ECMAScript, the standard specification of JavaScript. However, all the existing JavaScript static analyzers are manually designed; thus, the current approach is labor-intensive and error-prone. Moreover, since late 2014, this problem has become more critical because the JavaScript language itself rapidly evolves with a yearly release cadence and open development process. This thesis introduces a novel approach to derive JavaScript static analyzers from any version of ECMAScript automatically. Our approach consists of three steps: 1) mechanized specification extraction, 2) specification validity check, and 3) derivation of static analyzers. First, we present a tool JISET, which automatically extracts a mechanized specification from ECMAScript. We show that it successfully extracts a mechanized specification from the latest ECMAScript. Then, we present two different tools to detect bugs in JavaScript specifications; JEST performs N+1-version differential testing with JavaScript engines, and JSTAR performs a type analysis for the specification. Finally, we present JSAVER, which automatically derives JavaScript static analyzers from mechanized specifications using a meta-level static analysis. For evaluation, we derived a JavaScript static analyzer from the latest ECMAScript (ES12, 2021). The derived analyzer soundly analyzed all applicable 18,556 official conformance tests with 99.0% of precision in 1.59 seconds on average. We believe that the thesis would be the first step towards the co-evolution of specifications, tests, and tools for programming languages.
자바스크립트의 동적인 성질과 복잡한 의미론은 자바스크립트 프로그램들의 행동을 정확하게 이해하기 어렵게 만든다. 연구자들은 이를 해결하고자 다양한 자바스크립트 정적 분석기들을 개발해왔지만, 이들은 모두 수동으로 설계가 되었기에 노동집약적이고 오류에 취약하다. 또한, 2014년 말부터 자바스크립트의 언어 명세가 매년 갱신되기 시작하면서 이 문제는 더 심각해졌다. 본 학위 논문에서는 자바스크립트 언어 명세로부터 자동으로 자바스크립트 정적 분석기를 유도해내는 새로운 방식을 제안한다. 이는 1) 기계화 명세추출,2)명세의유효성검사,그리고3)정적분석기유도의세가지단계로구성된다. 본논문에서는 기계화 명세 추출 기술을 제안하고, 이를 이용해 가장 최신 자바스크립트 명세로부터 기계화 명세를 추출 한다. 또한, 자바스크립트 엔진을 이용한 N+1-버전 차분 테스팅과 기계화 명세의 타입 분석을 제안하고, 이를 통해 명세 및 엔진의 결함을 검출한다. 최종적으로, 메타 정적 분석 기술을 제안하고, 추출한 기계화 명세로부터 자동으로 자바스크립트 정적 분석기를 유도한다. 본 학위 논문에서 제시한 방식은 프로그래밍 언어를 위한 명세, 테스트, 그리고 도구들의 공진화를 위한 연구의 기틀을 마련할 것으로 기대한다.
