Building a sound and practical static analysis framework for JavaScript web applications in the wild자바스크립트 웹 어플리케이션의 안전하고 실용적인 정적 분석을 위한 프레임워크 개발 연구

Cited 0 time in webofscience Cited 0 time in scopus
  • Hit : 529
  • Download : 0
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.
Advisors
Ryu, Sukyoungresearcher류석영researcher
Description
한국과학기술원 :전산학부,
Publisher
한국과학기술원
Issue Date
2016
Identifier
325007
Language
eng
Description

학위논문(박사) - 한국과학기술원 : 전산학부, 2016.8 ,[v, 65 p. :]

Keywords

JavaScript; static analysis; analysis framework; analysis scalability improvement; analysis precision improvement; 자바스크립트; 정적 분석; 분석 프레임워크; 분석 속도 향상; 분석 정확도 향상

URI
http://hdl.handle.net/10203/222393
Link
http://library.kaist.ac.kr/search/detail/view.do?bibCtrlNo=663207&flag=dissertation
Appears in Collection
CS-Theses_Ph.D.(박사논문)
Files in This Item
There are no files associated with this item.

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0