SHF: Small: Random Testing for Language Design

标题：SHF：Small：语言设计的随机测试基于PROPERTY的随机测试(PBRT)是一种黑盒测试，其中使用软件构件的可执行部分规范来检查其相对于大量随机生成的测试用例的行为。PBRT提供了一系列好处，补充了完全、正式验证的传统优势；尤其是，它(1)允许对设计进行更快速的迭代，(2)鼓励及早专注于陈述正确的规范，以及(3)通过允许快速调试不变量来支持后来的证明工作。由Haskell的QuickCheck工具推广的PBRT现在在研究和工业中得到了广泛的应用。然而，当前PBRT方法不太成功的一个领域是，测试中使用的数据值具有复杂的内部结构或复杂的不变量。特别是，在语言设计和相关构件(例如编译器)的测试中就是这种情况，其中测试数据是程序。尽管有一些有希望的初步努力，但事实证明，随机测试很难应用于全面的语言设计。编程语言的许多有趣的属性都是“有条件的”，当随机测试被幼稚地应用时，会导致大量被丢弃的测试用例。这将重点放在构建良好的定制生成策略的能力上，但现有工具既不能很好地理解“有趣的程序”的生成策略，也不能很好地支持它们：需要更好的技术来编写和调试测试数据生成器。该项目旨在显著提高基于属性的随机测试的技术水平，具体应用于测试语言定义和相关构件的基本属性-属性，如类型安全、安全性(例如，“秘密输入不能影响公共输出”)，以及编译器的正确性。智能的优点是：(1)开发用于编写和调试复杂数据的随机生成器的新方法，特别是基于生成被测构件的“突变”的框架；(2)设计用于编写具有复杂不变量的随机测试数据的生成器的领域特定语言；(3)分发完善的实现，既作为标准QuickCheck库的兼容扩展，也作为CoQ证明助手的本地随机测试工具；以及(4)通过将这些工具应用于几个重要的案例研究来评估这些工具的有用性。该项目的更广泛影响是双重的。首先，更好地理解、更安全的语言设计将导致更好、更安全的软件，从而减少日常应用程序和关键基础设施中的错误和漏洞。特别是，该项目的主要案例研究旨在展示随机测试如何通过内置支持来改进新语言的设计过程，以确保基本的安全属性，如机密性、完整性、授权和访问控制。其次，除了语言设计之外，随机测试已被证明对提高软件质量极其有效。设想的工具将通过提供可与现有行业标准平台QuickCheck一起使用的编写和测试随机数据生成器的新工具，以及通过在流行的规范和验证工具Coq内提供对随机测试的本地支持，来显著提高随机测试的能力。项目成果将被纳入宾夕法尼亚大学的“高级编程”课程(该课程已经强调随机测试)，并将成为俄勒冈州编程语言暑期学校语言属性随机测试模块的基础。

Title: SHF:Small:Random Testing for Language DesignPROPERTY-BASED RANDOM TESTING (PBRT) is a form of black-box testing in which executable partial specifications of a software artifact are used to check its behavior with respect to large numbers of randomly generated test cases. PBRT offers a range of benefits that complement the traditional strengths of full, formal verification; in particular, it (1) allows much more rapid iteration on designs, (2) encourages early focus on stating correct specifications, and (3) supports later proof efforts by allowing invariants to be debugged quickly. Popularized by the QuickCheck tool in Haskell, PBRT is now widely used in both research and industry. However, one area where current PBRT methodology has been less successful is where the data values used in testing come with have complex internal structure or intricate invariants. In particular, this is the case in testing of language designs and related artifacts such as compilers, where the test data are programs. Despite some promising preliminary efforts, random testing has proved difficult to apply to full-scale language designs. Many of the interesting properties of programming languages are "conditional," leading to a large number of discarded test cases when random testing is applied naively. This places a premium on the ability to construct good custom generation strategies, but generation strategies for ``interesting programs'' are neither well understood nor well supported by existing tools: better techniques are needed for writing and debugging test-data generators. This project aims to significantly advance the state of the art in property-based random testing, with specific applications to testing fundamental properties of language definitions and related artifacts---properties such as type safety, security (e.g., ``secret inputs cannot influence public outputs''), and compiler correctness. The intellectual merits are: (1) developing new methodology for writing and debugging random generators for complex data, in particular a framework based on generating ``mutants'' of an artifact under test; (2) designing a domain-specific language for writing generators for random test data with complex invariants (3) distributing polished implementations, both as a compatible extension to the standard QuickCheck library and as a native random-testing tool for the Coq proof assistant; and (4) evaluating the usefulness of these tools by applying them to several significant case studies. The broader impacts of the project are twofold. First, better understood, more secure language designs will lead to better and more secure software, and hence to fewer bugs and vulnerabilities in everyday applications and in critical infrastructure. In particular, the project's main case studies aim to show how random testing can improve the design process for new languages with built-in support for guaranteeing fundamental security properties such as confidentiality, integrity, authorization, and access control. Second, beyond language design, random testing has proven extremely effective for improving software quality. The envisaged tools will significantly increase the power of random testing by offering new tools for writing and testing random data generators that can be used with QuickCheck, an existing industry-standard platform, and by offering native support for random testing within Coq, a popular specification and verification tool. Project results will be incorporated into the "Advanced Programming" course at Penn (which already emphasizes random testing) and will form the basis for a module on random testing of language properties at the Oregon Programming Languages Summer School.