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

点击翻译按钮获取中文摘要

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.