Publications

Proving Quantum Programs Correct

Abstract

As quantum computing progresses steadily from theory into practice, programmers will face a common problem: How can they be sure that their code does what they intend it to do? This paper presents encouraging results in the application of mechanized proof to the domain of quantum programming in the context of the SQIR development. It verifies the correctness of a range of a quantum algorithms including Grover's algorithm and quantum phase estimation, a key component of Shor's algorithm. In doing so, it aims to highlight both the successes and challenges of formal verification in the quantum context and motivate the theorem proving community to target quantum computing as an application domain.

Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks. "Proving Quantum Programs Correct." Proceedings of the Conference on Interative Theorem Proving (ITP). 2021.

To appear

A Verified Optimizer for Quantum Circuits

Abstract

We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a simple quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. SQIR uses a semantics of matrices of complex numbers, which is the standard for quantum computation, but treats matrices symbolically in order to reason about programs that use an arbitrary number of quantum bits. SQIR's careful design and our provided automation make it possible to write and verify a broad range of optimizations in VOQC, including full-circuit transformations from cutting-edge optimizers.

Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks. "A Verified Optimizer for Quantum Circuits." Proceedings of the ACM Conference on Principles of Programming Languages (POPL). 2021.

Distinguished paper at POPL 2021

Finding Substitutable Binary Code By Synthesizing Adapters

Abstract

Independently developed codebases typically contain many segments of code that perform same or closely related operations (semantic clones). Finding functionally equivalent segments enables applications like replacing a segment by a more efficient or more secure alternative. Such related segments often have different interfaces, so some glue code (an adapter) is needed to replace one with the other. We present an algorithm that searches for replaceable code segments by attempting to synthesize an adapter between them from some finite family of adapters; it terminates if it finds no possible adapter. We implement our technique using concrete adapter enumeration based on Intel's Pin framework and binary symbolic execution, and explore the relation between size of adapter search space and total search time. We present examples of applying adapter synthesis for improving security of binary functions and switching between binary implementations of RC4. We present two large-scale evaluations: (1) we run adapter synthesis on more than 13,000 function pairs from the Linux C library, and (2) we reverse engineer fragments of ARM binary code by running more than a million adapter synthesis tasks. Our results confirm that several instances of adaptably equivalent binary functions exist in real-world code, and suggest that adapter synthesis can be applied for automatically replacing binary code with its adaptably equivalent variants.

Vaibhav Sharma, Kesha Hietala, Stephen McCamant. "Finding Substitutable Binary Code By Synthesizing Adapters." IEEE Transactions on Software Engineering (TSE). 2019.

Formal Verification vs. Quantum Uncertainty

Abstract

Quantum programming is hard: Quantum programs are necessarily probabilistic and impossible to examine without disrupting the execution of a program. In response to this challenge, we and a number of other researchers have written tools to verify quantum programs against their intended semantics. This is not enough. Verifying an idealized semantics against a real world quantum program doesn’t allow you to confidently predict the program’s output. In order to have verification that works, you need both an error semantics related to the hardware at hand (this is necessarily low level) and certified compilation to the that same hardware. Once we have these two things, we can talk about an approach to quantum programming where we start by writing and verifying programs at a high level, attempt to verify properties of the compiled code, and repeat as necessary.

Robert Rand, Kesha Hietala, Michael Hicks. "Formal Verification vs. Quantum Uncertainty." 3rd Summit on Advances in Programming Languages (SNAPL). 2019.

Quantitative Robustness Analysis of Quantum Programs

Abstract

Quantum computation is a topic of significant recent interest, with practical advances coming from both research and industry. A major challenge in quantum programming is dealing with errors (quantum noise) during execution. Because quantum resources (e.g., qubits) are scarce, classical error correction techniques applied at the level of the architecture are currently cost-prohibitive. But while this reality means that quantum programs are almost certain to have errors, there as yet exists no principled means to reason about erroneous behavior. This paper attempts to fill this gap by developing a semantics for erroneous quantum while-programs, as well as a logic for reasoning about them. This logic permits proving a property we have identified, called є-robustness, which characterizes possible “distance” between an ideal program and an erroneous one. We have proved the logic sound, and showed its utility on several case studies, notably: (1) analyzing the robustness of noisy versions of the quantum Bernoulli factory (QBF) and quantum walk (QW); (2) demonstrating the (in)effectiveness of different error correction schemes on single-qubit errors; and (3) analyzing the robustness of a fault-tolerant version of QBF.

Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, Xiaodi Wu. "Quantitative Robustness Analysis of Quantum Programs." Proceedings of the ACM Conference on Principles of Programming Languages (POPL). 2019.

Volume-Based Merge Heuristics for Disjunctive Numeric Domains

Abstract

Static analysis of numeric programs allows proving important properties of programs such as a lack of buffer overflows, division by zero, or integer overflow. By using convex numeric abstractions, such as polyhedra, octagons, or intervals, representations of program states are concise and the analysis operations are efficient. Unfortunately, many sets of program states can only be very imprecisely represented with a single convex numeric abstraction. This means that many important properties cannot be proven using only these abstractions. One solution to this problem is to use powerset abstractions where a set of convex numeric abstractions represents the union rather than the hull of those state sets. This leads to a new challenge: when to merge elements of the powerset and when to keep them separate. We present a new methodology for determining when to merge based on counting and volume arguments. Unlike previous techniques, this heuristic directly represents losses in precision through hull computations. In this paper we develop these techniques and show their utility on a number of programs from the SV-COMP and WCET benchmark suites.

Andrew Ruef, Kesha Hietala, Arlen Cox. "Volume-Based Merge Heuristics for Disjunctive Numeric Domains." International Static Analysis Symposium (SAS). 2018.

Finding Substitutable Binary Code for Reverse Engineering by Synthesizing Adapters

Abstract

Independently developed codebases typically contain many segments of code that perform the same or closely related operations. Being able to detect these related segments is helpful to applications such as reverse engineering. In this paper, we tackle the problem of determining whether two segments of binary code perform the same operation by asking whether one segment can be substituted by the other. A key insight behind our approach is that because these segments often have different interfaces, some glue code (an adapter) will be needed to perform the substitution. Here we present an algorithm that searches for substitutable code segments by attempting to synthesize an adapter between them. We implement our technique using concrete adapter enumeration and binary symbolic execution to explore the relation between size of adapter search space and total search time. Then, using more than 61,000 fragments of binary code extracted from a ARM image built for the iPod Nano 2g device and functions from the VLC media player, we evaluate our adapter synthesis implementation on more than one million synthesis tasks. Our tool finds dozens of instances of VLC functions in the firmware image. These results confirm that instances of adaptably substitutable binary functions exist in real-world code, and suggest that adapter synthesis has promising reverse engineering applications.

Vaibhav Sharma, Kesha Hietala, Stephen McCamant. "Finding Substitutable Binary Code for Reverse Engineering by Synthesizing Adapters." 2018 IEEE 11th International Conference on Software Testing, Verification and Validation (ICST). 2018.