On September 16, 2024, I was invited to give a talk at Google headquarters in Mountain View, California. One of the topics that I spoke about, was computer-checked proofs for papers on symmetric-key cryptography. (It s really difficult to get these
A wide range of practical problems can easily be solved by SMT solvers such as z3, cvc5, and STP. The idea is to write out the problem as a system of equations and let the solver automatically find a solution
Following up on the SHA-3 buffer overflow in the official SHA-3 implementation, many people have been asking me how the vulnerability was found As I explain in an upcoming paper at ACISP 2023, the vulnerability was found using the KLEE
Update: This result appeared in the proceedings of CT-RSA 2023. A preprint is available. Over the past few months, I ve been coordinating the disclosure of a new vulnerability that I ve found. Today is the disclosure date, so I am excited
This is the second post on buffer overflow attacks! Feel free to check out Buffer Overflow Attacks (Part 1) as well. In this post, we ll have to deal with undefined behavior in the C programming language. It cannot be stressed
This is my very first blog post! More will follow At least for this few post, I m writing for an audience of one, which is my future self. I ll be covering topics that may be covered elsewhere, however, I personally