Verified Cryptographic Code for Everybody

Along with Amazon Web Services, Galois is publishing a new paper titled “Verified Cryptographic Code for Everybody,” and we really do mean everybody. One benefit of the way we’ve done this work is that everyone who was using the code already is now using verified code. The library we’ve verified parts of is called AWS-LibCrypto. Much of that library is code that originated from BoringSSL, and BoringSSL is composed of code originating from OpenSSL. By almost any metric, these are the most-used cryptography libraries in the world, and we have verified some of the most critical code that they contain!

In the proof, we used SAW to verify hand-written cryptography safe and correct with regards to Cryptol specifications. The optimizations and details of the code we were verifying made the work very challenging but equally rewarding and important. We’re happy that our proofs have helped provide assurance for commonly used cryptography. The paper describes how our proofs work, and it also covers some of the challenges and engineering we did to accomplish such a challenging task. I hope you give it a read, and please reach out with your questions.

Read More

The Cost of IEEE Arithmetic in Secure Computation

As secure multi-party computation (MPC) moves into the mainstream, users will expect it to support familiar data types such as IEEE-754 standard floating-point representations. Today, however, MPC typically does not support that standard. Instead, MPC implementations generally support alternative real number representations that are more amenable to MPC computation. In this paper, we compare performance of IEEE-754 floating point in MPC with those alternative representations, and we show that IEEE-754 may not perform well enough in MPC to be a wise choice.

Read More