SHF: Small: Random Testing for Language Design

职务名称：基于属性的随机测试（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.