Stream: Coq users

Topic: Verifying Rust programs


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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 ...

view this post on Zulip 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). ;)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: Feb 01 2023 at 13:03 UTC