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

SHF：小型：指定、检查和分析使用动态语言框架构建的应用程序

• 批准号: 1319666
• 负责人: Jeffrey Foster
• 金额: $ 41.27万
• 依托单位: University of Maryland, College Park
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-09-01 至 2017-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1319666&HistoricalAwards=false
• 关键词: SHF; Small; Specifying; Checking; Analyzing

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.

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