Interview with Kristina Sojakova & Mihai Codescu (IPDL) – NGI ASSURE BENEFICIARIES
“IPDL” Project
Have you ever wondered how secure our online communications are?
Are you curious about the complexities of cryptographic systems and how we can verify their security?If your answer is yes, then this interview is perfect for you!
Join Kristina Sojakova and Mihai Codescu, proud beneficiaries of NGI Assure, and discover how their project, IPDL (Interactive Probabilistic Dataflow Logic), is revolutionising the security and verification of large cryptographic systems.
Welcome to the world of IPDL!
Are you curious about the complexities of cryptographic systems and how we can verify their security?If your answer is yes, then this interview is perfect for you!
Join Kristina Sojakova and Mihai Codescu, proud beneficiaries of NGI Assure, and discover how their project, IPDL (Interactive Probabilistic Dataflow Logic), is revolutionising the security and verification of large cryptographic systems.
Welcome to the world of IPDL!
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.
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)
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.
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.
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.
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 PROJECT GOALS?
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.
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 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.
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 ANY RECOMMENDATIONS FOR IMPROVING 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.
NGI Assure (NGI GO2S) has received funding from the European Commission, as part of the Horizon 2020 Research and Innovation Programme, under Grant Agreement Nº 957073. This Project is funded under the NGI (Next Generation Internet) Initiative, powered by the Digital Single Market of the European Commission. NGI Assure was previously also referred to as NGI Go2S.