High Assurance Cryptography and the Ethics of Disclosure w/ Nadim Kobeissi
Description
Formally verified cryptographic libraries are increasingly deployed in critical systems, marketed as providing the highest level of assurance against implementation defects. But what happens when vulnerabilities are found in code that sits just outside the verified perimeter, and what obligations do vendors and researchers have when they are?
This talk examines both questions through a case study of Cryspen's libcrux and hpke-rs, cryptographic libraries used by Google, Signal, and OpenMLS. We present six vulnerabilities, including missing Diffie-Hellman validation, nonce reuse via integer overflow, signature malleability, and a denial-of-service crash — none of which were caught by formal verification. We introduce a taxonomy of verification boundary failures that explains why: unverified platform abstractions, unverified protocol logic, incomplete specifications, and unverified wrapper code each create attack surface that formal proofs, by construction, cannot reach.
We then turn to the disclosure experience itself. After submitting pull requests with working, tested fixes, we were blocked from the repositories, our fixes were closed unmerged, and we were accused of bad faith — then, the vendor copy-pasted the fixes they had just rejected and merged them four days later. The vendor citing a security policy that, for one of the two affected repositories, did not exist. We contrast this response with the vendor's constructive engagement with a prior public report that did not include fixes, raising questions about when "responsible disclosure" norms are invoked as policy and when as pretext.
We argue that formally verified software creates a heightened ethical obligation for transparent disclosure: users who are told to place extraordinary trust in a library deserve extraordinary candor when that trust is violated. We close with recommendations for verification boundary documentation, honest marketing of formal methods, and disclosure practices proportional to the assurance that was claimed.
Speaker Info
As a Senior Applied Cryptography Auditor at Cure53, Nadim leverages his extensive experience in software security audits to ensure the integrity of critical cryptographic systems. Nadim has contributed to over 250 software security audits, both independently and through partnerships with Cure53. Additionally, he is the Director at Symbolic Software, where he publishes research software for applied cryptographers and indie video game projects. Nadim is passionate about advancing the field of cryptography and making it more accessible to developers and researchers.
Stay in Touch
Everyone around the world depends on open source software. If you’re interested in financially supporting this critical work or are interested in an audit for your project, reach out to [email protected].
Follow us on our social media as well at: