CAREER: Fuzzing Formal Specifications

通过精确地描述程序的行为，形式化规范可以作为强大的安全性和安全性保证的基础。然而，在实践中，它们没有得到充分利用，被认为是复杂和成本低的。这个项目的目标是使用随机测试（模糊测试）来使编写、调试和推理规范变得更容易。该项目的新颖之处在于：研究传统上在高度结构化和高度约束的数据上操作的高级规范的模糊理论和实践；发展以反馈为基础的数据生成理论；并简化这些（以及未来的）技术在实践中的表现评估。该项目的影响是提高开发人员的生产力和软件质量，通过联合研究和教育努力，使更多的程序员可以访问规范的好处。该项目的目标是生成具有语义约束的随机结构化测试数据的问题，特别关注两个协同推进：(1)如何通过收集额外信息和揭示哪些测试导致了以前未见过的或其他有趣的行为，从而最大限度地利用每次测试运行；(2)如何在不受结构和语义约束的情况下改变这些测试，最大限度地提高发现错误的机会。本项目中开发的技术将通过构建具有基础真理的功能程序的基准套件以及对其在教育环境中的有效性进行扩展的经验评估来进行评估。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Formal specifications can serve as the foundation of strong safety and security guarantees by precisely describing the behavior of a program. However, they are underutilized in practice, being perceived as complex and cost-ineffective. The goal of this project is to use randomized testing (fuzzing) to make it easier to write, debug, and reason about specifications. The project's novelties are: studying the theory and practice of fuzzing with high-level specifications that traditionally operate on highly structured and highly constrained data; developing a theory of feedback-based generation of such data; and streamlining the evaluation of how these (and future) techniques perform in practice. The project's impacts are increased developer productivity and software quality, rendering the benefits of specifications accessible to more programmers through a combined research and educational effort.The project targets the problem of generating random structured test data with semantic constraints, with a particular focus on two synergistic thrusts: (1) how to make the most out of every test run by gathering additional information and revealing which tests led to previously unseen or otherwise interesting behavior; and (2) how to mutate such tests while staying within the structural and semantic constraints imposed, maximizing the chance to uncover errors. Techniques developed in this project will be evaluated by constructing a benchmark suite of functional programs with ground truth, as well as by carrying out an extended empirical evaluation of their effectiveness in an educational setting.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.