Planet Firefox

Previously I introduced some very basic Cryptol and SAWScript, and explained how to reason about the correctness of constant-time integer multiplication written in C/C++.
In this post I will touch on using formal verification as part of the code review process, in particular show how, by using the Software Analysis Workbench, we saved ourselves hours of debugging when rewriting the GHASH implementation for NSS....

An early version of the new Form Autofill feature is ready for testing by early adopters with U.S. addresses and websites using Firefox Nightly on desktop. Form Autofill helps you fill out addresses in online forms. You can give the work-in-progress...

A while ago I wrote about the state of server-side session resumption implementations in popular web servers using OpenSSL. Neither Apache, nor Nginx or HAproxy purged stale entries from the session cache or rotated session tickets automatically, potentially...

In the previous post I showed how to prove equivalence of two different implementations of the same algorithm. This post will cover writing an algorithm specification in Cryptol to prove the correctness of a constant-time C/C++ implementation.
Apart from rather simple Cryptol I’m also going to introduce SAW’s llvm_verify function that allows much more complex verification. We need this as our function will not only take scalar inputs but also store the result of the computation using pointer...