Maxime Dénès (Oct 18 2021 at 15:01): Maxime Dénès (Oct 18 2021 at 15:01):What tools are available today to verify Rust programs in Coq? I mean verification using Coq of existing Rust code (as opposed to extraction). Something around Iris & RustBelt, I guess?
Karl Palmskog (Oct 18 2021 at 15:09):I thought this was the state of the art: https://gitlab.mpi-sws.org/iris/lambda-rust/-/tree/master/theories/typing/lib
Andrés Goens (Oct 18 2021 at 16:11):There's also this, which is at a higher level of abstraction (closer to the language's syntax), but seems to be less mature https://github.com/aatxe/oxide
Andrés Goens (Oct 18 2021 at 16:13):Although I just realized that they don't have much Coq code in the repo after browsing it a bit (I had only looked at the paper, where they claim to be working on formalizing everything in Coq)
Paolo Giarrusso (Oct 18 2021 at 18:42):Formalizing != releasing I guess, but yes Oxide seems less mature... the two projects also have different focuses
Paolo Giarrusso (Oct 18 2021 at 18:45):RustBelt focuses on unsafe code (tho it also gives semantics to safe code), while IIUC Oxide focuses on safe code? But I'd rather ask @Ralf Jung.
Paolo Giarrusso (Oct 18 2021 at 18:47):and as a follow-up (loaded) question, is there any public tooling geared to "verifying Rust programs" more in general, building on RustBelt?
Paolo Giarrusso (Oct 18 2021 at 18:50):IIRC, RustBelt focuses on safety and functional correctness of key pieces of unsafe code, but you translate the code into Coq ASTs in CPS by hand (eg https://gitlab.mpi-sws.org/iris/lambda-rust/-/blob/master/theories/typing/lib/rwlock/rwlock_code.v) — no AST generation, right?
Paolo Giarrusso (Oct 18 2021 at 18:51):@Ralf Jung Would POPL people call the missing tooling 'just engineering' (even if huge amounts of) or would there be research challenges as well?
Maxime Dénès (Oct 18 2021 at 22:02):@Paolo Giarrusso Yes, these questions are exactly what I was wondering :) Hope Ralf can say more.
Ralf Jung (Oct 19 2021 at 02:39):yeah what we published with RustBelt so far relies on manual translation and is geared towards verifying safe encapsulation of unsafe code behind a typed API surface
Ralf Jung (Oct 19 2021 at 02:39):but verifying functional properties of Rust code and having more automated translation is certainly on the agenda for us :)
Ralf Jung (Oct 19 2021 at 02:41):Paolo Giarrusso said:
Ralf Jung Would POPL people call the missing tooling 'just engineering' (even if huge amounts of) or would there be research challenges as well?
I would say there are some research challenges left in developing systems for verifying functional correctness of Rust programs
Bas Spitters (Oct 19 2021 at 11:03):We've collected a number of formal method tools for rust here: https://rust-formal-methods.github.io/tools.html
The three methods that work for surface rust, as far is I know are:
Paolo Giarrusso (Oct 19 2021 at 21:23):oh right, a full Rust spec needs to deal with the semantics of unsafe code, sometimes with similar questions to those for C/C++ — from pointer provenance to atomics to ...
Ralf Jung (Oct 27 2021 at 18:21):Paolo Giarrusso said:
oh right, a full Rust spec needs to deal with the semantics of unsafe code, sometimes with similar questions to those for C/C++ — from pointer provenance to atomics to ...
indeed. there's a reason I am talking so much about pointer provenance the last year(s). ;)
Bas Spitters (Oct 27 2021 at 18:33):I should add that oxide also treats surface rust. So, do some of the other none Coq tools in the link above.
@Maxime Dénès what are you looking for?
Maxime Dénès (Oct 27 2021 at 20:09):I haven't looked at all of them yet, but I'm still wondering what would be the way to go if one wanted to reason on an existing Rust codebase. I guess, as you wrote, some work first has to be done to mechanically specify the Rust language itself.
Ralf Jung (Oct 27 2021 at 20:42):depends on the codebase -- if its safe Rust, most of the tricky questions of the Rust spec are not relevant
Bas Spitters (Oct 28 2021 at 11:14):In the last RFMIG we had a specification challenge. Creusot/rustHorn and prusti were presented.
The first group seems to be most concise.
The tools I mentioned above would probably be less suitable for an existing tool base, but could work well if you can start with a clean slate and are in a specific domain.
Last updated: Oct 08 2024 at 16:02 UTC