CAREER: Fuzzing Formal Specifications

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

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.