CAREER: Marlin: A Unified Framework for Automatic and Interactive Quantitative Program Analysis

实现我们日常使用的软件系统的可靠性和安全性是现代技术最紧迫的挑战之一。它已被证明，软件验证的数学方法是在满足这一挑战的一个重要组成部分。然而，大多数现存的验证项目和工具集中在证明软件的功能正确性。它们不分析软件的重要定量属性，如资源使用、边信道和概率保证，这些对于可靠性和安全性至关重要。该项目的新奇在于设计和实现了一个通用的定量验证框架，该框架可用于分析资源使用情况、概率程序（包含随机性）和侧通道。该项目的影响是，该框架使软件开发人员能够减少数据中心的能源消耗，减轻严重的安全漏洞，并将统计安全保证与具有机器学习组件的软件系统连接起来。该项目还为课程编制和外联活动提供了一个教学机会。在该项目中实现的定量验证和分析工具正在整合到Functional-Mellon的函数式编程和数据结构和算法本科课程中，以帮助学生推理代码的复杂性，并帮助教师和助教通过验证复杂性要求自动评分编程作业。作为该项目推广活动的一部分，研究人员正在为高中生设计两个课程模块，并通过现有的项目在梅勒基-梅隆大学推出。目前关于定量分析和验证的研究通常是针对具体问题的，分为手动或自动技术，不同领域之间几乎没有交叉。该项目的目的是开发马林，一个统一的定量验证框架。马林的一个显著特点是交互式推理和自动推理的紧密集成。这包括将手动导出的定量属性转换为可由自动技术使用的约束，并支持超越完全推理的更轻量级的自动化形式。马林是基于一个全功能的概率编程语言和表达的定量程序逻辑，支持组合和关系推理。马林的具体创新包括易于理解的子语言描述，保证自动化成功，自动生成最坏情况的输入，尾边界分析与更高的时刻，自动关系推理。 马林的基金会由三个专门的定量分析工具共享：资源感知ML（RaML），一种用于静态资源分析的语言; ParML，一种用于侧通道自由编程的新语言;和Borel，一种用于概率推理的工具。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估来支持。

Achieving reliability and security of software systems that we use on a daily basis is one of the most pressing challenges of modern technology. It has been demonstrated that software verification with mathematical methods is an important component in meeting this challenge. However, most extant verification projects and tools focus on demonstrating the functional correctness of software. They do not analyze important quantitative properties of software such as resource usage, side channels, and probabilistic guarantees, which are crucial for reliability and security. The project's novelty is the design and implementation of a general framework for quantitative verification that can be applied to analyze resource usage, probabilistic programs (that incorporate randomness), and side channels. The project's impact is that this framework enables software developers to reduce the energy consumption of data centers, to mitigate serious security vulnerabilities, and to connect statistical safety guarantees to software systems that have machine-learning components. The project also provides a pedagogical opportunity for curriculum development and outreach activities. Quantitative verification and analysis tools implemented in the project are being integrated in Carnegie-Mellon's undergraduate courses on functional programming and data structures and algorithms, to both help students reason about the complexity of their code, and help instructors and teaching assistants automatically grade programming assignments by verifying complexity requirements. As part of the project's outreach activities, the investigator is designing two course modules for high-school students that are rolled out through existing programs at Carnegie-Mellon.Current research on quantitative analysis and verification is often problem-specific, separated into manual or automatic techniques, and there is little cross-fertilization between different areas. The aim of this project is to develop Marlin, a unified framework for quantitative verification. A distinctive feature of Marlin is the tight integration of interactive and automatic reasoning. This includes converting manually derived quantitative properties into constraints that can be consumed by automatic techniques and supporting more lightweight forms of automation beyond full inference. Marlin is based on a full-featured probabilistic programming language and an expressive quantitative program logic that supports compositional and relational reasoning. Specific innovations of Marlin include easily-understood descriptions of sub-languages for which the automation is guaranteed to succeed, the automatic generation of worst-case inputs, tail-bound analysis with higher moments, and automatic relational reasoning. Marlin's foundation is shared by three specialized quantitative analysis tools: Resource Aware ML (RaML), a language for static resource analysis; ParML, a new language for side-channel free programming; and Borel, a tool for probabilistic inference.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.