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

在过去的几十年里，在构建程序分析工具以在软件开发过程的早期检测错误方面取得了巨大的进步。不幸的是，现有的工具忽略了一个越来越重要的软件系统类别：那些使用动态语言框架编写的软件系统。这样的框架今天非常流行，例如，网络上许多最流行的站点都是使用它们构建的。虽然动态语言框架的表现力、灵活性和强大功能鼓励了它们的快速和广泛采用，但这些特性也击败了现有的程序分析技术。本研究旨在通过开发实用的工具和技术来解决这个问题，用于在使用动态语言框架的软件开发过程中早期检测和预防错误。这项研究将提高我们正确和快速地构建许多重要软件系统的能力，包括那些每天都要依赖的软件系统。首先，本研究将开发规范来描述感兴趣的高级语义属性。目标动态语言框架将是Ruby on Rails，它是当今最流行的Web开发框架之一。要探索的规范包括Ruby on Rails对类型和内存安全的类似物;支持特定于域的语言的规范;以及可扩展到特定于应用程序的属性的规范。其次，本研究将发展一个新颖的执行时包装与检查系统，以在程式执行时执行程式分析。 由此产生的系统将检查程序属性晚于典型的静态分析，但明显早于最后时刻的动态检查，这是今天的唯一选择。最后，本研究将探讨如何部署符号执行，以进一步扩大运行时属性检查。开发的技术将在开源Ruby on Rails应用程序上进行评估。预计开发的技术也可以应用于许多其他动态语言框架。

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.