CyLab Ph.D. student receives honor for “highest quality” thesis

CyLab’s Aymeric Fromherz, a Ph.D. student in Electrical and Computer Engineering (ECE) and a CyLab Presidential Fellow, was recognized with an A.G. Milnes Award, which is awarded to a graduating ECE Ph.D. student for the Ph.D. 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.”

“Aymeric is well versed in formalism, and more than willing to get his hands dirty building systems and proofs to evaluate what happens when programming-language theory encounters practice,” says CyLab’s Bryan Parno, an associate professor of ECE and computer science and Fromherz’s Ph.D. advisor. “He multi-tasks well, keeping multiple projects in the air with apparent ease, and he remains optimistic in the face of setbacks. He was a pleasure to have in our group at CMU, and I’m very glad we have found ways to continue our collaborations even after his graduation.”

Fromherz’s thesis, “A Proof-Oriented Approach to Low-Level, High-Assurance Programming,” proposes a new perspective and approach for developing high-performance code that comes with strong guarantees of security and correctness.

Aymeric is well versed in formalism, and more than willing to get his hands dirty building systems and proofs...

Bryan Parno, Associate Professor, Electrical and Computer Engineering and Computer Science

A large portion of Fromherz’s thesis work arose from his role as the main CMU student representative to Project Everest, a collaboration between CMU, Microsoft Research (MSR), and Inria to develop a fully verified HTTPS ecosystem, which is the foundation on which Internet security is built.

“Unfortunately, this ecosystem is extremely brittle, with headline-grabbing attacks and emergency patches occurring many times a year,” says Parno. “Project Everest aims to replace the current infrastructure with proven-secure software.”

Fromherz’s thesis describes his work on EverCrypt, a comprehensive collection of verified, high-performance cryptographic code. It is the world’s largest collection of verified cryptographic software, and several of its algorithms outperform state-of-the-art unverified implementations. Code from EverCrypt has made its way into the Linux kernel, Mozilla’s Firefox browser, various Microsoft products, and several blockchains.

The A.G. Milnes Award honors the late Dr. Arthur Milnes, who was a prolific ECE professor at CMU starting in 1957. During his tenure, Professor Milnes and his students produced hundreds of papers. He also authored several books and a groundbreaking paper that was included in Citation Classics as one of the most cited items in its field. Professor Milnes received numerous awards, including the Ebers Award from the Electron Devices Society and the Van der Ziel Award for outstanding, sustained semiconductor device research.