In this thesis, we present $SAFE_{WApp}$ , an open-source static analysis framework for JavaScript web applications. It provides a faithful (partial) model of web application execution environments of browsers, based on empirical data from the main web pages of the 9,465 most popular websites. A main feature of $SAFE_{WApp}$ is the configurability of DOM tree abstraction levels to allow users to adjust a trade-off between analysis performance and precision depending on their applications. We also present the Loop-Sensitive Analysis (LSA) technique that improves the analysis scalability of $SAFE_{WApp}$ by enhancing the analysis precision in loops. LSA distinguishes loop iterations as many as needed by automatically choosing loop unrolling numbers during analysis. We formalize LSA in the abstract interpretation framework and prove its soundness and precision theorems using the proof assistant tool, Coq. Our evaluation of LSA implemented on top of $SAFE_{WApp}$ shows that $SAFE_{WApp}$ with LSA outperforms the state-of-the-art JavaScript static analyzers in terms of analysis scalability. We also evaluate our framework with the 5 most popular JavaScript libraries and the main web pages of the 10 most popular websites on the effect of DOM tree abstraction levels and modeling coverage. Additionally, using a bug detector that has been built as an application of $SAFE_{WApp}$, we present previously undiscovered bugs in the main web pages of wikipedia.org and amazon.com. Finally, to further improve analysis precision of $SAFE_{WApp}$, we suggest a new string domain that uses simple regular expressions, which is expressive enough to represent prefix, infix, and postfix substrings of a string and even their sets. We formalize the domain in abstract interpretation and present inclusion decision rules between our regular expressions, which are necessary to implement the domain. We prove that the rules exactly check inclusion relation between regular expressions in our domain.
본 학위 논문에서는 자바스크립트 웹 어플리케이션의 안전하고 실용적인 정적 분석을 지원하는 오픈 소스 프레임워크 개발을 목표로 한다. 이를 위해 인기 있는 웹사이트의 메인 웹 페이지에서 조사한 자료들을 기반으로 한 브라우저 환경 분석 모델을 지원하는 $SAFE_{WApp}$ 프레임워크를 제작하였다. 해당 프레임워크의 분석 속도와 정확도 향상을 위한 루프 민감 분석 기술도 제안하는 데, 이 기술은 분석 도중 루프를 얼마나 펼쳐야 하는 지 자동으로 찾아 필요한 만큼 루프의 각 반복 절차를 구분하여 분석 정확도 향상을 통해 분석 속도도 향상 시킬 수 있는 기법이다. 요약 해석 틀을 이용하여 해당 기술을 정형화 하였으며 안전성과 정확성을 증명하였다. 마지막으로 $SAFE_{WApp}$ 의 정확도를 더 향상시키기 위한 방법으로 정규식을 활용한 새로운 문자열 도메인을 제안하였다. 요약 해석 틀을 이용하여 안전하게 정의하였고, 구현이 가능하도록 정규식들의 포함관계를 정확하게 결정하기 위한 규칙들을 정의하였다.
