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.