SHF: Medium: Collaborative Research: Semantics Engineering for Scripting Languages

在过去的十年里，脚本语言扮演了重要的角色。最初，Web开发人员使用Perl和Python来丰富Web服务器的内容;后来Ruby on Rails席卷了整个场景。在同一时期，JavaScript已经成为Web客户端的主导语言。此外，脚本语言的流行激发了开发人员使用它们来构建许多其他类型的系统，包括关键任务实时系统。虽然脚本语言是探索设计思想的有效工具，但它们的使用也给软件周期带来了一些新的问题。最基本的是，脚本语言往往缺乏类型系统，这往往会增加系统的调试和维护成本。更糟糕的是，尽管脚本语言往往是安全的，但它们灵活的原始操作会导致程序中难以预测的行为，从而产生新型的安全漏洞。与此同时，脚本语言没有一个定义良好的语义，使得它几乎不可能验证的安全性或安全property.In响应这些观察程序分析的可靠性，这个建议承诺重新设计脚本语言的语义。具体来说，PI建议研究三种脚本语言的可执行语义的构造：JavaScript，Python和Racket。他们将使用语言级别的测试套件来检查语义是否对实现进行了充分的建模。此外，PI将使用语义来设计和验证这些脚本语言的类型系统和程序分析。从长远来看，该提案将在三个方面对整个世界产生影响。首先，脚本语言的类型系统和分析应该帮助软件开发人员提高他们的软件的安全性和降低他们的维护成本。其次，脚本语言的语义将帮助研究人员验证他们关于程序分析的想法。最后，PI将开发一个语义重新设计的过程，这对许多其他脚本语言社区来说应该是有用的。

Over the last decade, scripting languages have assumed a huge role. Initially web developers used Perl and Python to enrich the content of web servers; later Ruby on Rails took the scene by storm. Over the same period, JavaScript has become the dominant language on the client side of the web. Additionally, the popularity of scripting language has inspired developers to use them for the construction of many other kinds of systems, including mission-critical real-time systems. While scripting languages are productive tools for the exploration of design ideas, their use also introduces several new kinds of problems into the software cycle. Most basically, scripting languages tend to lack a type system, which tends to raise the debugging and maintenance costs for systems. Worse, even though scripting languages tend to be safe, their flexible primitive operations induce difficult-to-predict behavior in programs and thus creates novel kinds of security holes. At the same time, scripting languages do not come with a well-defined semantics, making it nearly impossible to validate the soundness of a program analysis for safety or security properties.In response to these observations, this proposal promises to re-engineer the semantics of scripting languages. Specifically, the PIs propose to investigate the construction of executable semantics for three scripting languages: JavaScript, Python, and Racket. They will use the language-level test suites to check that the semantics model the implementations adequately. In addition, the PIs will use the semantics to design and validate type systems and program analyses for these scripting languages. Over the long run, the proposal should impact the world at large in three ways. First, the type systems and analyses for scripting languages should help software developers improve the safety of their software and reduce their maintenance cost. Second, the semantics for the scripting languages will help researchers validate their ideas concerning program analyses. Finally, the PIs will develop a process for semantic re-engineering that should be useful to many additional scripting language communities.