Hi all,
We are a company based in Tel Aviv (KZen Networks) working on multi-party digital signatures for blockchains and our cryptography layer is exclusively in Rust. We are dealing with several types of elliptic curves, implementing zero-knowledge proofs, bullet-proofs etc...
We are talking with the French INRIA Prosecco team led by Karthik Bhargavan (http://prosecco.gforge.inria.fr/personal/karthik/) and we are investigating in Rust code generation with HACL / F. Our goal is to formally verify our cryptographic protocols.
We were wondering how mature is formal verification in Rust and what could be a good starting point.
We are a company based in Tel Aviv (KZen Networks) working on multi-party digital signatures for blockchains and our cryptography layer is exclusively in Rust. We are dealing with several types of elliptic curves, implementing zero-knowledge proofs, bullet-proofs etc...
We are talking with the French INRIA Prosecco team led by Karthik Bhargavan (http://prosecco.gforge.inria.fr/personal/karthik/) and we are investigating in Rust code generation with HACL / F. Our goal is to formally verify our cryptographic protocols.
We were wondering how mature is formal verification in Rust and what could be a good starting point.
@/all i'm planning on doing a "reboot" soon, similar to what the unsafe code guidelines wg recently did--if anyone has comments/ideas about that, let me know
Hi! I'm trying to write a formalization of parsing expression grammars and I'm not quite sure what tool to use. What I think I need is something that can use a partial definition: in order not to complicate things with a full formalization, I'm thinking about just writing the properties of the base combinatord then have more complicated ones defined on top. I need this to be able to tell me whether two expressions invalida
... whether two expression's purported equivalence invalidates any of the properties/definition.
Did a quick search, and it seems somebody has verified PEGs in Coq, but sadly the artifacts were never made public :( https://arxiv.org/pdf/1105.2576.pdf
looking at the inductive types that they use and the proof outlines could be helpful though
Z3 doesn't do any termination checking, afaik, so understandable that you might start running into timeouts
Another interesting one, for parser combinators (not PEGs) in Agda is: http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.pdf
Somehow I missed your comments a while back, @gbenattar . If you'd like to try SAW, it currently supports LLVM and has some MIR support in progress. Trying the existing LLVM verification capabilities on some of your primitives could give you some sense for how applicable it might be. This example might be helpful to look over: https://github.com/GaloisInc/saw-script/tree/master/examples/salsa20
I wouldn't be surprised if you encounter problems with unimplemented LLVM intrinsics that are used by rustc but not by clang. If you come across anything like that, we'd love a GitHub issue describing it.
And once the MIR support is done, that'll likely be an even better path to take. I suspect it'll be able to handle typical crypto code by the end of the year.
Oh, and use nightly binaries, rather than the somewhat old GitHub releases. See here: https://saw.galois.com/builds/nightly/
I'd like to gather as much information on the tools that are interested in working on rust codebases as possible, so if that describes you, either message me or open up an issue/pr on the github :)
if anyone has opinions on chat medium, pop them in there
@avadacatavra I have created a github repository https://github.com/vakaras/mir-dump/ that illustrates how we extract information from the compiler.
Is there some "pure" subset of Rust in which you can write specs and that can be embedded into an attribute ?
Hello @denismerigoux .The functional specifications were discussed in this issue: rust-lang-nursery/wg-verification#14. As far as I know, we currently do not even have a consensus how specifications should be written.
What I am currently working on, is a way to get typed ASTs of something like this: https://github.com/nrc/libhoare
Wouahou this is very nice ! I'm currently wortking on code examples from Servo that would benefit some verification, to see exactly what kind of invariants and pre/post-conditions we're looking at. I'm manually translating the Rust code into pure functional Fstar (think of it as a full-spectrum dependently typed OCaml/F#), and using Fstar to verify some properties
If you want I can show you what annotations I would need on the Rust code and that would be expressed using libhoare
I've created a zulip for the wg--https://rust-lang.zulipchat.com/#narrow/stream/183875-wg-formal-methods
The reason I've chosen zulip is that the way it groups topics is much easier to process asynchronously
And it will organize the discussions more I hope :)
There's also a number of other working groups on zulip--let me know if anyone as questions/needs help getting onto zulip!
@dragostis it's not about the function being small, it's about the bug only triggering on a tiny part of the input space. typically, fuzzers basically send random data into your program, so you cannot expect them to find such panics. for this you'd need some kind of instrumented fuzzer that determines how it can get a good branch coverage. such fuzzers exist as research prototypes but I don't know how far into the practically appliable tools this technology has made it.