Verifpal: a new effort to make it easy to verify the security of Internet protocols
By Dr Nadim Kobeissi, Professor at NYU Paris and Director of Symbolic Software
Secure protocols are critical to a secure Internet. During my Ph.D. studies, I worked on formally proving the security of vital Internet protocols such as HTTPS, Signal and Let’s Encrypt. However, I also quickly realized that the methods I had used to produce my security assurances required highly specialized knowledge and were not accessible to a more general audience of students and engineers. Therefore, I have wanted for many years to work on a project that would allow any computer science student, engineer or security enthusiast to also better reason about and understand the security of their designs.
Since the second or third year of my Ph.D. studies, I was already envisioning ‘Verifpal’, a software framework for the automated analysis of cryptographic protocols that would focus first and foremost on being fun and accessible. I also imagined Verifpal personified as a heroic Japanese-anime-style cryptographer that uses her great determination and resilience to formally verify the Internet’s security and, therefore, undo the evil plans of insidious villains (I admittedly watch too much Dragon Ball and read too much Nietzsche for my own good).
When I applied to NGI Zero/NLNet for funding, I had the experience, motivation and inspiration to realize my idea, but not the necessary freedom: I wanted to design a cryptographic analysis framework on my own terms, in a way that was original and that dared to break with academic tradition in order to focus as much as possible on usability and helpfulness to the average student, engineer or enthusiast. I was incredibly pleased to quickly learn that working with Michiel and Joost from NGI Zero/NLNet meant working with people who not only appreciated my somewhat unorthodox ideas, but also were ready to lend me their trust and confidence.
The NGI Zero/NLNet process was fair and simple: I was initially asked to write a short, four-page research proposal describing my idea, my promised deliverables, timeline, related research work and applications to the real world. NGI Zero/NLNet then got back to me a few months later with a suggested timetable, and I was free to work for four months on building the initial working prototype of Verifpal, complete with documentation and example models.
Verifpal has allowed my students to model sophisticated cryptographic protocols, such as Signal and Scuttlebutt, in less than two hours. These protocols would take days to model properly in existing tools. I believe that what makes Verifpal special is the following:
- Verifpal’s intuitive protocol modeling language allows the user to illustrate protocols close to how one may describe them in an informal conversation, while still being precise and expressive enough for formal modeling.
- Verifpal’s modeling language also avoids user error. Verifpal comes with built-in cryptographic functions – this is meant to remove the potential for users to define fundamental cryptographic operations incorrectly.
- Verifpal’s analysis results are easy to understand. When a security issue is found in a protocol, the result is related in a readable format that ties the attack to a real-world scenario.
- Verifpal software and documentation focuses on friendliness and integration. In the future, we plan to have Verifpal integrated into popular software development frameworks, such as Visual Studio Code, such that live feedback can be provided as the user is describing their protocol.
Currently, Verifpal is still experimental software and we are still ironing out the kinks such that we have strong guarantees on its analysis results. Once that is done, we plan to make Verifpal generate functional software implementations directly from the protocol models, which would allow the user to directly prototype their protocol in the real world!
A major part of Verifpal is the Verifpal User Manual, which combines an easy-to-understand, illustrated guidebook to the Verifpal software with… a full-blown Japanese manga where Verifpal battles ‘Mayor N. D. Middle’ in a quest for truth and justice (‘man in the middle’ is a term frequently used by cryptographers and engineers to describe a type of interception attack that can weaken the security of Internet protocols).
While the manga admittedly is a bit of a strange move for a research project (and was funded by me personally, not by NGI Zero/NLNet!), I found it to not only be incredibly useful in communicating the interest and usefulness of formal verification to my undergraduate students, but also to be really cool. I worked with Collateral Damage Studios, a team of anime-style illustrators from Singapore to bring Verifpal to life. I provided the team at Collateral Damage Studios with pages and pages in which I specified Verifpal’s general look, inspiration, critical notes on Verifpal’s personality and appearance, and also mentioned which anime artists I found most appropriate in terms of style (chiefly Akira Toriyama). I worked with Collateral Damage Studios for three months, and you can see their documentation of their process on their Behance page.
Verifpal and the Verifpal User Manual in their current state are already a promising start for the project. Independent users from all over the world have shared with me their models and results, and the Verifpal Mailing List has already seen serious discussion on how to improve the software’s analysis. In my classroom, Verifpal has already been used by my students to model examples for e-voting protocols, and to then spot mistakes and corrections in each other’s models, in a collaborative learning and discovery process. I plan to continue on moving Verifpal forward as free and open source software, as we bolster the soundness of the analysis and add new features.
I consider NLNet, NGI and the NGI community to be lifelong partners in the development of Verifpal and thank them very much for their support and their confidence. The NGI ecosystem has the right priorities, the right values, and offers independent researchers and developers the chance to realize their ideas without delays, setbacks or unnecessary complications.
To learn more about Verifpal, go to the project website at: https://verifpal.com/
The Who’s NGI Blog series features members of the NGI community and highlights their achievements.