Kristina Sojakova & Mihai Codescu - IPDL
Equational Proofs for Distributed Cryptographic Protocols
Software engineering, protocols, cryptography
Can you introduce yourself and your project?
We are Kristina Sojakova and Mihai Codescu, researchers in formal methods with security applications. In our NGI Assure project, IPDL (Interactive Probabilistic Dataflow Logic), we are developing a framework for constructing formal proofs of large message-passing cryptographic systems such as Multi-Party Computation (MPC).
The project stems from a theoretical line of work begun by Kristina and her collaborators from Cornell University, which has recently appeared at the Symposium on Principles of Programming Languages. Our project is a software tool that implements the aforementioned theoretical approach, and we have recently used it to formally verify the passive security of a large MPC protocol – the GMW protocol with an arbitrary number of parties and an arbitrary Boolean circuit. Mihai is responsible for all aspects of the implementation work.
What are the key issues you see with the state of the internet today?
The internet’s role in our lives has grown to an unprecedented dimension. We use the internet for essential communication, shopping, finances, control of home appliances, social interaction, and access to medical information. In this setting, protecting private information is of utmost importance. This is the focus of our project.
Most cryptographic algorithms we use nowadays to secure sensitive data are too complex for humans to verify using pen-and-paper methods, as subtle vulnerabilities often go unnoticed despite numerous security audits (for example, researchers at Verichains developed attacks that break several modern MPC protocols).
How does your project contribute to correcting some of those issues?
We aim to give cryptographic researchers the tools for constructing formal security proofs for large message-passing cryptographic protocols. Having a computer-checked mathematical proof that certifies the protocol as secure will significantly increase the trustworthiness of the cryptographic design and contribute to the trustworthiness of the internet as a whole.
What do you like most about (working on) your project?
We are excited to be making progress in an important direction. We very much appreciate the high degree of freedom we have in setting our goals and our timetable. Our successes so far—the formal verification of a very large and complex case study, the proof of which is very fast — make us especially optimistic about future developments.
Where will you take your project next?
Our current focus is on enhancing usability. Any user familiar with the core logic of IPDL should be able to use our tool seamlessly without being exposed to the implementation-specific internals. We hope this will lead to adopting our tool outside of academia.
How did NGI Assure help you reach your goals for your project?
Given its very applied nature, this project would be challenging to finance via a research grant. NGI Assure provided the perfect venue for this. The reviewing process has helped us see things from a non-specialist’s perspective, and the feedback we have received so far has influenced our design decisions.
We are also very grateful for being able to propose several extensions to the original working plan that will help transition our tool from a prototype into mature software.
Do you have advice for people who are considering applying for NGI funding?
If your project aligns well with the goals of an NGI call, you should absolutely apply. The review process contains an interactive part, which we found particularly helpful; the questions posed by the reviewers were particularly relevant and helped us better frame our project in the greater scheme of the NGI initiative.
Do you have any recommendations to improve future NGI programmes or the wider NGI initiative?
Participating in the NGI initiative has been a great opportunity and a very good experience for us. We can only hope that these initiatives continue.
Acknowledgements
Images: courtesy of Kristina Sojakova & Mihai Codescu.
Published on October 29, 2024
IPDL received funding through the NGI Assure Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 957073.
