the performance was pretty much identical, however, as an added benefit, Blake2 got quite a bit faster due a combination of
1) our code being slightly more optimized, and
2) python's blake2 integration not actually doing runtime cpu detection, meaning that unless you compiled with -march=native (like, Gentoo), at the time, you were not getting the AVX2 version of Blake2 within Python -- my PR fixed that and added code for CPU autodetection
Author here, I thought it'd be helpful to address a few of the points brought up in the various comment threads.
1. This is an academic paper that we posted on arxiv, not a release announcement for a new product where we claim we have solved C to Rust. We submitted to a PL conference, not an open-source meeting like e.g. FOSDEM -- this is not the same audience at all, and the expectations are very different.
2. Our story is simple. We start from the constraint of translating C to /safe/ Rust, and see what this entails: a small well-behaved subset of C, inference of slice splitting, a translation that may error out, and a program that may abort (plus a few other things described in the paper). We evaluate our ideas on what we have (C embedded in F*), and show that it scales decently with those constraints in mind, on a large-scale C library that is used in Firefox, Python, and many other pieces of mainstream software. We don't claim we can rewrite e.g. Firefox in Rust automatically.
3. This is how research works. We think we have an interesting point in the design space; we don't claim we solve every issue, but think this is an interesting idea that may unlock further progress in the space of C to Rust translation, and we think it's worth putting out there for others to take inspiration from. Who knows, maybe some existing tool will use this approach for parts the fit in the subset, and fall back to unsafe Rust for other parts that don't fit! This is a very active area: if we can contribute something that other tools / researchers can use, great.
4. This is not the final story, and again this is how research works. We are working on an actual C frontend via libclang, and are exploring how e.g. guarantee that the generated Rust does not generate out of bounds accesses, perhaps by emitting verification conditions to Z3 (speculating on future work here). If the reviewers think more work is needed, that's fine, and we'll resubmit with enhancements. If the reviewers think this is an active area and others could benefit from our ideas, and take the paper, even better.
Hi, one of the paper authors here. This is unfortunately only part of the story. This "calculette" covers only a fraction of the tax computation; furthermore, without knowing the crazy semantics and computational rules of the M language, it's very hard to reproduce the tax computation.
Just to build on Catalin's answer. We are actively working on an implementation of QUIC's transport layer (i.e. packet encryption and decryption), along with a proof of cryptographic security. This is what Catalin linked to (https://github.com/project-everest/everquic-crypto). EverQuic-Crypto builds upon two previous projects: EverParse, a library of verified low-level parsers and serializers which we apply to the QUIC network formats, and EverCrypt, a cryptographic provider with agility and multiplexing, which we use for all the cryptography, e.g. packet number encryption, AEAD, etc.
This is not yet a full QUIC implementation, but we have plans for extending this codebase to cover more of the QUIC protocol.
Several comments note that the headline is perhaps a little misleading; I agree, and I don't think any of us (I'm one of the cited people in the article) would've made such a strong claim.
Ignoring for a moment the fact that this is an alpha release (and that as such, a handful of minor proofs, e.g. mundane facts related to endianness conversions, have yet to be completed), there are several limitations of our work.
- Our tools themselves are not verified, so there could be a bug in F, z3, the kremlin F-to-C compiler; or a bug about the C compiler itself (unless one uses a constant-time fork of CompCert). We consider most of these to be theoretically unpleasant, but still an acceptable tradeoff.
- Specifications are extremely hard to get right: one might introduce a typo when reading an RFC, or, say, state an endianness conversion wrong. So, even before implementing an optimized version of anything, we audit and test the spec first. This is usually a good sanity check, but certainly not bulletproof (note that this is a general problem of software verification, not specific to us).
- As noted near the end of the article, our models do not account for Spectre and Meltdown; and there might be new classes of attacks that we can't guard against, for the simple reason that they haven't been found yet.
As to whether this is an attempt to get free security audits, I guess we weren't intentionally thinking of it! But we certainly would love it if people could test the code and give us feedback on what to improve to make this an even more compelling choice for whoever needs a good cryptographic library. I've written a bit about this here: https://jonathan.protzenko.fr/2019/04/02/evercrypt-alpha1.ht...
> I don’t expect Mezzo to be the next big thing, but ideas from it will most probably make their way into upcoming type-safe systems languages.
I guess that's also one difference between Rust and us. Being researchers, we don't have the manpower to turn this into a working, industrial project, so we're hoping that the ideas percolate. Rust, in contrast, it trying to become the next big thing, maybe at the expense of having theoretical soundness results and papers in 10pt LaTeX :).
(Disclaimer: I'm the co-author of Mezzo, and I also happen to be a long-time Mozilla contributor).
While we indeed do not mention Rust in the bibliography, the question does pretty much come up all the time (rightly so). The answer I usually give is that Rust and Mezzo are in essence trying to achieve the same thing, except that Mezzo is in the context of ML.
Being a high-level language gives us more flexibility:
- we can afford _not_ to think about what's stack-allocated or heap-allocated;
- our adoption/abandon mechanism, which somehow keeps the complexity of the system within reasonable bounds, is implemented using run-time tests;
- de-allocation is not predictable because we use a GC (so no destructors).
So I would say that we don't have to deal with all the high-performance constraints that Rust is tackling, which makes our life easier :-).
Also, the implementation and the design is a two-man project. I think the Rust team is a tiny bit bigger now!