A journey to the Best Paper Award
When a group of Lincoln Laboratory staff began a project exploring how to construct a new protocol language to protect information from adversaries, they had no idea it would lead to three years of work, multiple paper revisions, and eventually a Lincoln Laboratory Best Paper Award.
Keeping information — especially information that could compromise the security of the nation — from adversaries is crucial. At the same time, designing and implementing systems that prevent information leakage to our adversaries is no easy task. Even if a protocol is carefully developed and tested, attackers may spot weaknesses that the designers did not anticipate.
In 2018, a team consisting of previous Laboratory employees Robert Cunningham, Benjamin Kaiser, and Alice Lee; summer students Daniel Park and Andrew Wagner; and Martine Kalke, the associate leader of the Secure Resilient Systems and Technology Group, and Timothy Braje, technical staff in the Cyber Operations and Analysis Technology Group, were funded by the Air Force Cyber Resiliency Office for Weapons Systems to make systems, specifically satellites, more resilient to cyberattacks. Their goal was to use formal verification to help ensure that vulnerabilities in the software did not exist.
As the team set out to build a software updater for satellites, they began discussions with Adam Chlipala, a computer science professor at MIT, who suggested creating a protocol verification system. The goal soon became to develop a domain-specific cryptographic protocol language that would make developing secure protocols accessible to users with a wide variety of skill sets.
The initial team began by attending Chlipala's course Formal Reasoning About Programs to learn the techniques needed for the project. After the semester was finished, the team continued to meet on campus weekly with Chlipala. In those meetings, the team worked through difficult issues such as the intricacies of machine-checked proofs in the Coq proof management system, the design of formal program semantics, and strategies for structuring the "Strong Preservation Theorem," the main result from the paper.
"I learned a lot collaborating with Adam. My background is mainly in astrophysics, and this was the first time I had ever done a project like this," Braje says. "Each week, we would go up to the whiteboard and discuss the current state of the protocol language and how we could move forward on the project. It was frustrating at times and very difficult, but it was also fun."
Through years of work and meetings with Chlipala, the team developed Secure Protocols Implemented CorrectlY (SPICY), a set of programming tools that enables software developers unfamiliar with formal methods or cryptography to design secure protocols with a high degree of assurance. The language they developed enforces mechanisms that guarantee that adversaries cannot interfere with honest party communication. This language is one of the first of its kind, and makes creating a secure channel for messages accessible, which was one of the team's main goals.
"Protocol verification has been the focus of many research projects. It is notoriously difficult and time-consuming. We took a different approach than most groups, focusing on how to simplify and automate the process," Braje says. "Our main result demonstrates that you can reduce the protocol verification problem, with certain assumptions, down to very simple rules checking. This was a monumental effort, and showed how crucial the Laboratory's connection with MIT is; without the back-and-forth with Adam and the team, none of this would have been possible."
The team decided that their work was significant enough to be published, so they started drafting a paper. The journey that would lead to the Laboratory's Best Paper Award was longer and more tedious than any of them expected. When they first submitted it to Institute of Electrical and Electronics Engineers (IEEE)'s Security and Privacy conference, the comments they received from the first round of peer review proved to them that they needed a full overhaul of the introduction in order to emphasize the importance of this project and clarify the motivation. Several months and many revisions later, they submitted it to the IEEE Computer Security Foundations symposium and it was accepted.
"I found it very educational to go through writing the paper and getting it published because it really forced us to motivate and clearly explain our results," Braje says. "We did have to iterate a few times with reviewers and rather than getting frustrated with how long the process took, we continued to edit and ultimately produce a paper we are really proud of."
Adversary Safety by Construction in a Language of Cryptographic Protocols was published in the proceedings of the 2022 IEEE 35th Computer Security Foundations Symposium in August of 2022 and earned the team the Laboratory's 2022 Best Paper Award. The award "recognizes the Lincoln Laboratory authors of the most outstanding published paper appearing in a peer-reviewed journal or peer-selected conference publication" and comes with a plaque and a monetary award of $1,000 per author.
"The paper is exceptionally well written in a way that makes it accessible to the non-specialist yet also delves deeply into a significant advancement to the state of the art in cryptographic tools," says Robert Bond, who served on the Best Paper Award selection committee. "We were struck by how skillfully the authors lead the reader through a series of lucidly explained and progressively more complex examples to make the paper's main points abundantly clear; this is quite a feat for such a complex topic."