Marlin
Automatic and interactive quantitative analysis
Collaborators
Overview
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.
News Coverage
Support
Supported by an NSF CAREER Award.
Publications
-
Typable Fragments of Polynomial Automatic Amortized Resource Analysis In 29th EACSL Annual Conference on Computer Science Logic (CSL’21). 2021 [pdf]
-
Raising Expectations: Automating Expected Cost Analysis with Types In 25th International Conference on Functional Programming (ICFP’20). 2020 [pdf]
-
Liquid Resource Types In 25th International Conference on Functional Programming (ICFP’20). 2020 [pdf]
-
Exponential Automatic Amortized Resource Analysis In 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’20). 2020 [pdf]
-
Automatic Space Bound Analysis for Functional Programs with Garbage Collection In 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR’18). 2018 [pdf]