Prusti for verified Rust crypto about subtle HOT 2 CLOSED

Hi there, having better tooling for verified crypto would be great.

From my perspective, there's a spectrum of tooling choices that ranges from immediately pragmatic on one end to more theoretically complete on the other hand. This library is focused pretty squarely at one end, trying to provide tools that are practical today (a rust library that can be pretty easily integrated) but still eliminate a wide class of errors (it's not possible to accidentally apply variable-time operations to Choices). Getting guarantees all the way down to the assembly level would be nice, but I think that the current implementation gets 80-90% of the benefit without requiring significantly more complex tooling.

In contrast, projects like Vale or Evercrypt may be able to make better guarantees, but they are not really integrable into existing projects, and they take a pretty specialized all-or-nothing approach. So my expectation is that at least in the near-to-medium-term, these projects will have pretty different positions in the space of design tradeoffs.

from subtle.

I see a couple issues with the Prusti approach (although that looks like a really cool project!):

1. Any "pure" function (i.e. deterministic and side-effect free) can currently only return an integer or a bool, so we'd have to remove our Choice type, which is the whole point of this library, i.e. to prevent a compiler from optimising a u8 into a bool/i1.
2. The only constraints we really care about are "when called with any possible inputs, do these functions execute the same set of instructions" and "do those instructions branch on secret data", neither of which appear to be testable with Prusti.

That's not to say we don't wish to formally verify these constraints, just that the tooling for this isn't really applicable for integration into a production library which implements the kinds of safety checks we have in subtle.

Closing for now, since this isn't really an issue, but feel free to discuss further of course.

from subtle.