SHF: Small: Specifying, Checking, and Analyzing Applications Built with Dynamic Language Frameworks

点击翻译按钮获取中文摘要

The last several decades have seen tremendous progress in building program analysis tools to detect bugs early in the software development process. Unfortunately, existing tools neglect an increasingly important category of software systems: those written using frameworks in dynamic languages. Such frameworks are very popular today, e.g., many of the most popular sites on the web are built using them. While the expressiveness, flexibility, and power of dynamic language frameworks have encouraged their rapid and widespread adoption, those features also defeat existing program analysis techniques. This research aims to address this problem by developing practical tools and techniques for detecting and preventing errors early during software development that uses dynamic language frameworks. This research will improve our ability to correctly and rapidly build many important software systems, including those relied upon every day.There are three main components of the project. First, this research will develop specifications to describe the high-level semantic properties of interest. The target dynamic language framework will be Ruby on Rails, one of the most popular web development frameworks today. Specifications to be explored include the Ruby on Rails analogs to type- and memory-safety; specifications supporting domain-specific languages; and specifications that are extensible to application-specific properties. Second, this research will develop a novel run-time wrapping and checking system to perform program analysis while a program is executing. The resulting system will check program properties later than a typical static analysis, but significantly earlier than the last-moment dynamic checks that are the only option today. Finally, this research will explore ways to deploy symbolic execution to amplify run-time property checking even further. The developed technology will be evaluated on open-source Ruby on Rails applications. It is expected that the techniques developed can be applied to many other dynamic language frameworks as well.