SAFE: Formal Specification and Implementation of a Scalable Analysis Framework for ECMAScript
SAFE: Formal Specification and Implementation of a Scalable Analysis Framework for ECMAScript
复制标题
SAFE：ECMAScript 可扩展分析框架的正式规范和实现
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Sukyoung Ryu
中科院分区：
文献类型：
--
作者：
Hongki Lee;S. Won;Joonho Jin;Junhee Cho;Sukyoung Ryu
Web编程中JavaScript的普遍使用揭示了JavaScript应用程序的安全漏洞问题，这强调了JavaScript分析器检测此类问题的必要性。近年来，研究人员提出了几种JavaScript程序的分析器，一些Web服务公司开发了各种JavaScript引擎。然而，不幸的是，大多数工具都没有很好的文档化，因此很难理解和修改它们。或者，这些工具通常不对公众开放。在本文中，我们提出了正式规范和实现的安全，可扩展的分析框架ECMAScript，JavaScript研究社区开发。这是第一次尝试为JavaScript提供正式规范及其开源实现，而现有的方法只关注其中之一。为了使它更适合其他研究人员使用我们的框架，我们正式定义了三种中间表示的JavaScript中使用的框架，我们提供正式规范之间的翻译。为了适应冒险的未来研究，包括修改原始JavaScript语法，我们积极使用开源工具来自动生成解析器和一些中间表示。为了支持在不同的编译阶段的各种程序分析，我们设计的框架是灵活的，可扩展的，可插拔的。最后，我们的框架是公开的，一些合作研究使用的框架正在进行中。
The prevalent uses of JavaScript in web programming have revealed security vulnerability issues of JavaScript applications, which emphasizes the need for JavaScript analyzers to detect such issues. Recently, researchers have proposed several analyzers of JavaScript programs and some web service companies have developed various JavaScript engines. However, unfortunately, most of the tools are not documented well, thus it is very hard to understand and modify them. Or, such tools are often not open to the public. In this paper, we present formal specification and implementation of SAFE, a scalable analysis framework for ECMAScript, developed for the JavaScript research community. This is the very first attempt to provide both formal specification and its opensource implementation for JavaScript, compared to the existing approaches focused on only one of them. To make it more amenable for other researchers to use our framework, we formally define three kinds of intermediate representations for JavaScript used in the framework, and we provide formal specifications of translations between them. To be adaptable for adventurous future research including modifications in the original JavaScript syntax, we actively use open-source tools to automatically generate parsers and some intermediate representations. To support a variety of program analyses in various compilation phases, we design the framework to be as flexible, scalable, and pluggable as possible. Finally, our framework is publicly available, and some collaborative research using the framework are in progress.