Add support for the *ring* Rust crypto library

[briansmith]

https://github.com/briansmith/ring is a crypto library I am working on that is based (currently) on BoringSSL, but which aspires to become mostly Rust and assembly language (and less C). The whole point of that library is to provide a high level of assurance of correctness while being very fast and efficient.

I am very interested in using hacrypto to verify the correctness of the library, and I'm happy to contribute patches to do this. However, the learning curve for somebody completely new to all the tools is pretty daunting.

Let's say I wanted to start by verifying the SHA-2 implementations as thoroughly as possible. What's the first step? It seems like I need some way of adapting the Rust API/ABI to what these tools expect.

Note that while currently the hashing functions are wrappers around the OpenSSL/BoringSSL code you already verify, I am planning to replace a lot of the code, basically everything that gets generated due to md_common.h with Rust, and I'd love to be able to use this tool to verify that that refactoring is correct.

I'm also very interested in using this to verify the correctness of the AEAD, RSA, and ECC code, especially since I'll be replacing large parts of that code soon.

[kiniry]

Brian, I'll let the SAW key performers chime in, but in principle this is a fairly straightforward affair to get the infrastructure setup so you can begin to understand and perform formal verification. ( @atomb ? )

We even have some internal experience playing around with verifying Rust. ( @aisamanra )

[atomb]

Yes, it shouldn't be too hard to get the tools built, at least, and I'm happy to help in any way I can to get you going. You'll want to start with the saw-script repository. We've done some very basic things with Rust, and C-like Rust code should work ok, though more complex code might be tricky (and you'll have to describe everything in terms of LLVM-level concepts). I'd love to get the tools working better with Rust, though!

[atomb]

Also, since you mentioned API/ABI constraints: if you're structuring the code to be callable from C programs (i.e., making functions "extern"), they should be tractable to analyze with SAW. Code that uses Rust-specific types in the exported API will be more awkward, but perhaps still tractable. The main issue is that you'll need to describe those APIs in LLVM-oriented terms, rather than Rust-oriented terms, which could be tedious or brittle. For C-like APIs it should be fine, though.

[briansmith]

OK, sorry it has taken me a long time. I got scared by the license text I read regarding SAW and the need to have some agreement if there's any possibility that I might gain financially from ring if I use SAW on it. I am actually still confused about what's changed--what's open-source and what's not.

I actually start some infrastructure that would help with doing what you suggested above. In particular, I started https://github.com/briansmith/ring-ffi to make a C-like API. I believe I can crank out the FFI declarations as needed to help things.

I'm working on some new ECDH and ECDSA code (P-256 and P-384) that's almost ready. I know that Galois did some really interesting work on verification of ECC code before and I'm particularly interested in seeing how this would work for my Rust (ECDSA, ECDH, and ECC point multiplication) + C (Fermat's Last Theorem modular inversion, P-384 point addition + point doubling) + ASM (OpenSSL's nistz256 field operations + point addition + point doubling). Would this be jumping too far into the deep end to start with?

[atomb]

With the latest license changes, all of SAW (at least anything you can find on GitHub) is open source, and usable for anything by anyone.

If you want to take a look at our ECC Java code and the verification scripts, they're in the saw-script repository here:

https://github.com/GaloisInc/saw-script/tree/master/examples/ecdsa

The code is very C-like (or Rust-like, really). It doesn't make any particular use of Java-specific features. If written in either of those language, one major change would probably be simpler code, since the Java code has to do all sorts of contortions to get around the fact that Java doesn't have unsigned integers.

Since the code is fairly C-like, and since SAW works on LLVM, you may be able to use variants on those proof scripts to verify your Rust and C code (but not the ASM portions, for now). It would be a big job, but one with a large number of fairly similar components, so I definitely think it's worth trying.

We'll be updating the LLVM parser in SAW very soon to support the bitcode format used by the version of LLVM that comes with stable Rust. At the moment, you'll probably have a hard time loading Rust-generated LLVM, but that's a temporary issue.

[briansmith]

Thanks. Originally I filed this issue here because I thought putting the ring verification into this hacrypto repo might help with licensing stuff. But, it seems like that is no longer a concern. This is probably just making noise in the hacrypto issue tracker. So, instead I'll track this in the ring issue tracker at https://github.com/briansmith/ring/issues/214. In particular, the SAW ECDSA verification example linked to above looks awesome, but it looks like adapting it to work for ring is going to be something that is going to take more time than I have immediately available. Thanks!