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
Easily Solving Hard SMT Queries
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
SHA-3 Buffer Overflow (Part 2)
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
SHA-3 Buffer Overflow
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
Buffer Overflow Attacks (Part 2)
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
Buffer Overflow Attacks (Part 1)
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