Fromherz wins ACM SIGSAC Doctoral Dissertation Award

In today’s technology-driven world, software plays an increasingly important role in ensuring the safety and security of the products and tools we use. From autonomous vehicles to online banking, the complexity and size of software continues to grow, and reliability has become more critical than ever.

To ensure the dependability of real-world critical software, Aymeric Fromherz, a former CyLab Presidential Fellow who earned his Ph.D. from Carnegie Mellon’s Department of Electrical and Computer Engineering (ECE) in 2022, advocates for the adoption of a proof-oriented programming paradigm in high-assurance software development, providing mathematical guarantees about various aspects of a program’s behavior.

In his thesis, “A Proof-Oriented Approach to Low-Level, High-Assurance Programming,” which was awarded the 2022 ACM Special Interest Group on Security, Audit and Control’s (SIGSAC) Doctoral Dissertation Award, Fromherz argues that co-developing programs and proofs alongside of one another can not only simplify the programming and proving processes, but also improve software quality by eliminating unneeded checks and cases.

“You should have proofs about your programs and code from day one,” says Fromherz. “Proofs bring a lot of value to both the safety and security of the software and can help programmers close any openings that could lead to potential attacks.”

Fromherz and fellow researchers rely on two case studies to validate this argument.

The first targets high-performance cryptography, a secure communications technique with a wide variety of uses, including digital signatures, electronic money, and time stamping, that protects digital data by transforming it into formats that unauthorized users cannot read or modify.

Relying on the proof-oriented programming concept, Fromherz and several collaborators developed EverCrypt, a comprehensive collection of verified, high-performance cryptographic functionalities, some of which have since been deployed in several high-profile open-source projects such as Mozilla Firefox and the Linux Kernel. With this, the group demonstrates how abstraction and zero-cost generic programming simplify verification without sacrificing performance, leading to verified cryptographic code whose performance matches or exceeds the best-unverified implementation.

In the second case study, researchers investigate the use of proof-oriented programming to develop concurrent, low-level systems. To do this, they created Steel, a novel verification framework based on a higher-order, impredicative concurrent separation logic. Here, the group shows how designing with proofs in mind allows for the ability to automatically separate verification conditions between separation logic predicates and first-order logic encodable predicates. The group also demonstrates Steel’s expressiveness and programmability in a variety of examples.

Earlier this year, Fromherz received an A.G. Milnes Award for his dissertation. The award recognizes a graduating Ph.D. student for thesis work “judged to be of the highest quality and which has had, or is likely to have, significant impact in his or her field.”