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

职业：Marlin：自动和交互式定量程序分析的统一框架

• 批准号: 1845514
• 负责人: Jan Hoffmann
• 金额: $ 51.88万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-07-01 至 2024-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1845514&HistoricalAwards=false
• 关键词: CAREER; Marlin; Unified; Framework; Automatic

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.

实现我们日常使用的软件系统的可靠性和安全性是现代技术最紧迫的挑战之一。事实证明，使用数学方法进行软件验证是应对这一挑战的重要组成部分。然而，大多数现有的验证项目和工具都侧重于证明软件功能的正确性。他们不分析软件的重要定量属性，例如资源使用、侧通道和概率保证，而这些属性对于可靠性和安全性至关重要。该项目的新颖之处在于设计和实现了定量验证的通用框架，该框架可用于分析资源使用情况、概率程序（包含随机性）和侧通道。该项目的影响在于，该框架使软件开发人员能够减少数据中心的能源消耗，减少严重的安全漏洞，并将统计安全保证连接到具有机器学习组件的软件系统。该项目还为课程开发和推广活动提供了教学机会。该项目中实现的定量验证和分析工具正在被集成到卡内基梅隆大学函数式编程和数据结构与算法的本科课程中，以帮助学生推理代码的复杂性，并帮助教师和助教自动对编程作业进行评分验证复杂性要求。作为该项目推广活动的一部分，研究人员正在为高中生设计两个课程模块，这些模块将通过卡内基梅隆大学的现有项目推出。当前定量分析和验证的研究通常是针对特定问题的，分为手动或自动技术上，不同地区之间很少有交叉施肥。该项目的目的是开发 Marlin，一个用于定量验证的统一框架。 Marlin 的一个显着特点是交互式和自动推理的紧密结合。这包括将手动导出的定量属性转换为可由自动技术使用的约束，并支持超越完全推理的更轻量级的自动化形式。 Marlin 基于功能齐全的概率编程语言和支持组合推理和关系推理的富有表现力的定量程序逻辑。 Marlin 的具体创新包括易于理解的子语言描述（保证自动化成功）、自动生成最坏情况输入、具有更高矩的尾部绑定分析以及自动关系推理。 Marlin 的基础由三个专门的定量分析工具共享：Resource Aware ML (RaML)，一种用于静态资源分析的语言； ParML，一种用于侧通道自由编程的新语言；该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Resource-Aware Session Types for Digital Contracts

数字合约的资源感知会话类型

• DOI: 10.1109/csf51468.2021.00004
• 发表时间: 2021
• 期刊: 2021 IEEE 34th Computer Security Foundations Symposium (CSF
• 作者: Das, Ankush;Balzer, Stephanie;Hoffmann, Jan;Pfenning, Frank;Santurkar, Ishani
• 通讯作者: Santurkar, Ishani

Probabilistic Resource-Aware Session Types

• DOI: 10.1145/3571259
• 发表时间: 2020-11
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Ankush Das;Di Wang;Jan Hoffmann

Raising expectations: automating expected cost analysis with types

• DOI: 10.1145/3408992
• 发表时间: 2020-06
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Di Wang;David M. Kahn;Jan Hoffmann

Central moment analysis for cost accumulators in probabilistic programs

• DOI: 10.1145/3453483.3454062
• 发表时间: 2021-06
• 期刊: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
• 作者: Di Wang;Jan Hoffmann;T. Reps

A Denotational Semantics for Low-Level Probabilistic Programs with Nondeterminism

• DOI: 10.1016/j.entcs.2019.09.016
• 发表时间: 2019-11
• 作者: Di Wang;Jan Hoffmann;T. Reps