Doing What It Says on The Crypto Tin: Verified Cryptography Code For Everyone

Doing What It Says on The Crypto Tin: Verified Cryptography Code For Everyone

When do developers ever create proof that their code actually does what it says it does? Well, it’s not an easy task, especially to prove against a mathematical implementation. So what we normally do is to test against a specification that matches the requirements, but this is no proof we have forgotten to test for every scenario. But a great new paper by Brett Boston, et al defines machine-assisted proofs for 256-bit AES (GCM) and SHA-384 [here]:

Within the paper, the authors focus on the LibCrypto, and which contains a range of cryptographic primitives that normally have tightly focused code and which does not have many external dependencies. One of the major challenges is that the code tends to be highly optimized (and typically written as a mixture of assembly language code and C), and where it is not easy to match these to formal proofs of operation. On the other hand, we see the “secure-by-design” software libraries, such as with EverCrypt. While these provide a good way forward in terms of security, these are not as widely adopted as the popular libraries of OpenSSL and BoringSSL. The paper provides a formal proof of implementation using legacy libraries.

The work focuses on two cryptographic primitives on a symmetric key method (AES-256-GCM) and a hashing method (SHA-384), and which are new implementations with the AWS-LC (AWS LibCrypto) library. Overall, the cryptography specification is written in Cryptol. It is thought that these formal proofs can be easily extended to other cryptographic libraries, as they tend to use similar implementation methods.

An example of implementing SHA-256 in Cryptol is:

f : ([8], [32], [32], [32]) -> [32]
f (t, x, y, z) =
  if (0 <= t)  && (t <= 19) then (x && y) ^ (~x && z)
   | (20 <= t) && (t <= 39) then x ^ y ^ z
   | (40 <= t) && (t <= 59) then (x && y) ^ (x && z) ^ (y && z)
   | (60 <= t) && (t <= 79) then x ^ y ^ z
   else error "f: t out of range"

In the following we create a Crytol file that implements the Atbash cipher:

% cat atbash.cry   
atbash : {n} String n -> String n
atbash pt = [ alph ! (c - 'A') | c <- pt ]
    where alph = ['A' .. 'Z']

 % cryptol
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.12.0
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol> :l atbash.cry
Loading module Cryptol
Loading module Main
Main> :set ascii=on
Main> atbash "ATTACKATDAWN" 
"ZGGZXPZGWZDM"

One of the advantages of using Crytol is that the specification can then be built as an executable, and then checked against the formal proof. These proofs use the Software Analysis Workbench (SAW) and which include abstract specifications. An example of the scripted used for AES verification is:

If you are interested in reading more, the paper is here:

References

[1] Boston, B., Breese, S., Dodds, J., Dodds, M., Huffman, B., Petcher, A., & Stefanescu, A. (2021, July). Verified Cryptographic Code for Everybody. In International Conference on Computer Aided Verification (pp. 645–668). Springer, Cham.