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

实现我们日常使用的软件系统的可靠性和安全性是现代技术最紧迫的挑战之一。事实证明，用数学方法进行软件验证是迎接这一挑战的重要组成部分。然而，现有的验证项目和工具大多侧重于验证软件的功能正确性。它们不分析软件的重要数量属性，如资源使用、旁通道和概率保证，这些属性对可靠性和安全性至关重要。该项目的创新之处在于设计和实现了一个用于定量验证的通用框架，该框架可用于分析资源使用情况、概率程序(包含随机性)和旁路。该项目的影响是，该框架使软件开发人员能够减少数据中心的能源消耗，减轻严重的安全漏洞，并将统计安全保证连接到具有机器学习组件的软件系统。该项目还为课程开发和外联活动提供了教学机会。该项目中实施的定量验证和分析工具正被整合到卡内基-梅隆大学函数式编程、数据结构和算法的本科课程中，以帮助学生对其代码的复杂性进行推理，并帮助教师和助教通过验证复杂性要求来自动对编程作业评分。作为该项目外展活动的一部分，研究人员正在为高中生设计两个课程模块，这两个模块是通过卡内基梅隆大学现有的项目推出的。目前关于定量分析和验证的研究通常是针对特定问题的，分为手动或自动技术，不同领域之间几乎没有交叉。该项目的目的是开发马林鱼，一个统一的定量核查框架。马林鱼的一个显著特点是交互推理和自动推理的紧密结合。这包括将手动派生的量化属性转换为可由自动化技术使用的约束，以及支持完全推理以外的更轻量级的自动化形式。Marlin基于功能齐全的概率编程语言和支持组合和关系推理的富于表现力的量化程序逻辑。Marlin的具体创新包括对自动化保证成功的子语言的易于理解的描述、最坏情况输入的自动生成、具有更高阶数的尾界分析以及自动关系推理。Marlin的基金会由三个专门的量化分析工具共享：资源感知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.