Google Information Security Engineering (Seattle)
Aeneas is a toolchain for verifying Rust programs, relying on a functional translation to Lean. Aeneas is now nearly five years old, and many excellent improvements have landed recently, thanks to the work of Son Ho, Aymeric Fromherz, Guillaume Boisseau and many other collaborators. With this blog post, I’m hoping to showcase how proofs in Aeneas look like these days, and highlight recent…
Perhaps the greatest surprise of the last two years was, for me, the realization that people not only care about compiling C to Rust (for obvious reasons, such as, ahem, memory safety) – they also care about compiling Rust to C! Wait, what?
In November 2022, I opened issue 99108 on Python’s GitHub repository, arguing that after a recent CVE in its implementation of SHA3, Python should embrace verified code for all of its hash-related infrastructure.
I recently wrote about ongoing efforts to retarget the compilation of HACL* from C to Rust. Today, Aymeric, myself and the entire HACL* team are happy to announce that we have a first alpha release of HACL-rs! (Right on time for the HACS workshop).
Over the past few years, a lot of eyes in the software verification community have turned towards Rust. That’s hardly a surprise: programs written in Rust are easier to verify, owing to the language’s strong ownership discipline; the absence of undefined behaviors; and its strong notion of value. As a result, we now have a plethora of tools for Rust verification: Creusot, Prusti, Verus, and of…
Long gone are the days of my youth where AOL Messenger and IRC ruled online communication spaces… in this day and age, people use WhatsApp, Signal, Facebook Messenger, or even Instagram Messages (or so I am told). This new generation of messenger apps provides some fundamental technological improvements, such as Unicode Emoji instead of ASCII smileys, or perhaps more interestingly to readers of…
For the past five years or so, I have been exploring, along with many other collaborators, the space of verified cryptography and protocols. The premise is simple: to deliver critical code that comes with strong properties of correctness, safety and security. Some readers may be familiar with Project Everest: this is the umbrella under which a large chunk of this work happened.
In a valiant attempt to wean myself off of doomscrolling, I thought I’d try to write a few blog posts this summer. This one highlights some of the exciting things that happened over the past few months in Everest, and specifically around the HACL and EverCrypt projects.
Earlier this year, I was paired up with my colleagues Chris, Tom, Madan and intern Danielle Gonzalez (from Rochester) for the annual Microsoft Hackathon. The goal was to examine and extract meaningful data from GHTorrent, a colossal data set that contains an exhaustive log of all GitHub events, for all repositories.
Today, we’re announcing a preview release of EverCrypt, a verified cryptographic provider that offers a comprehensive collection of cryptographic algorithms. EverCrypt automatically selects the best available implementation for your platform (C or assembly); offers unified APIs for families of algorithms (e.g. hashes); and its performance is on-par with what you’d find in, say, OpenSSL. In short,…