Coq-of-rust: Formal verification tool for Rust

https://github.com/formal-land/coq-of-rust

by todsacerdoti • 1 year ago

159 42 1 year ago

jedisct1• 1 year ago

Do that for Zig.

arn3n• 1 year ago

Rust’s “mutable-xor-aliased” model makes it particularly amenable to developing verification tools on top of it [1]. Without this model, verification becomes just as hard — and just as practically intractable — as all the verifiers for existing languages.

1: https://graydon2.dreamwidth.org/312681.html

johnisgood2• 1 year ago

Rust supports it better than many other imperative systems languages -- even some impure functional ones!

I am surprised that this blog post does not mention Ada / SPARK at all though.

porridgeraisin• 1 year ago

The link returns 403.

throwawaymaths2• 1 year ago

Without [mutable-xor-aliased], verification becomes just as hard

i get graydons point but as a counterpoint: at the point where you're adding a verifier to X-lang, you might as well put mutable xor aliased in the verifier instead of in the compiler.

throwawaymaths2• 1 year ago

probably zig air is a better target:

https://github.com/ityonemo/clr

https://m.youtube.com/watch?v=ZY_Z-aGbYm8

SAI_Peregrinus• 1 year ago

Even if Rust's type system prevents many mistakes, including memory errors, the code is still not immune to vulnerabilities, such as unexpected panics or wrongly implemented business rules.
The way to go further is to mathematically prove that it is bug-free: this is named "formal verification" and what coq-of-rust proposes! This is the only way to ensure your code contains no bugs or vulnerabilities, even against state-level actors .

I like formal verification. But I consider this a misrepresentation of what it offers. It lets you mathematically prove that your code implements a specification correctly. It doesn't prove that your specification is bug-free & vulnerability-free. It doesn't prove that your specification correctly implements your business rules.

Formal verification is still extremely useful. It's often much easier to use a specification language to define invariants your programming language code needs to obey than to only implement things in a programming language. To me that's a much better, more honest selling point for formal methods. You have to write more code, and in a different language, but unlike just testing you can actually prove that invariants hold for all possible inputs.

amw-zero2• 1 year ago

You are describing "validation": the process of verifying that your spec really says what you mean.

nicce2• 1 year ago

He is saying that original spec can be incorrect.

Animats• 1 year ago

It's very useful for things where the specification is much simpler than the implementation. Databases and file systems are good examples. A database can be specified as giant arrays with linear search. Now prove that the database with all its optimizations and concurrency behaves the same as the simple spec.

SubjectToChange3• 1 year ago

Using (formal) specification languages doesn't guarantee a specification is "correct" either.

You have to write more code, and in a different language, but unlike just testing you can actually prove that invariants hold for all possible inputs.

Formal verification is needed to show that the code actually implements a specification. If anything, a formal specification is really good for generating test suites for the implementation code.

9rx• 1 year ago

It doesn't prove that your specification is bug-free & vulnerability-free.

Mathematically prove might be a little strong, but if the implementation agrees then it is proven in the more general sense of the word. Similar to double entry accounting, there are two sides to the coin and both sides have to agree else you know there is a problem somewhere. To make the very same mistake twice here is statistically unlikely, so when they do agree there is sufficient evidence to believe that it is proven.

What is more likely is that one does not take the time to truly understand what they need from software and introduce features that, in hindsight, they wish they hadn't, but that is done with more intentionality and isn't really the same thing as a bug or vulnerability traditionally.

nextos• 1 year ago

It doesn't prove that your specification is bug-free & vulnerability-free.

There are formal development methodologies where you start with a small set of very simple axioms and you iteratively refine them. Eventually, you end up with code. All steps are formally verified along the way. This addresses your (valid) concerns. For example, many railway software control systems have been developed this way. See e.g. references [1,2] for some more in-depth discussion. Some of these ideas might make a comeback given that code generation is cheap now, but it's quite unreliable.

[1] https://raisetools.github.io

[2] https://raisetools.github.io/material/documentation/raise-me...

IshKebab• 1 year ago

Yeah that's fine if you can do it. His point is that most software is not that simple. I work in RISC-V verification and the spec is full of ambiguously worded or easy to misinterpret or just plain unspecified requirements. Even if you formally verify your chip against a formal specification there's a huge gap between the asciidoc ISA manual and that formal specification where bugs can exist.

Something like compression is the absolute best case - you have a trivial property that covers everything. Mostly it isn't like that though.

im3w1l• 1 year ago

I sort of imagine (but I'm not experienced enough to actually state) that you could create a negative specification. Something like: this program will certainly not open the file flag.txt

This doesn't guarantee the program is correct. But it's not nothing.

ynik• 1 year ago

Even the trivial specification "given a valid input, the program exits successfully with some arbitrary output" will already get you very far: to prove this trivial specification as correct, you need to prove the absence of panics, undefined behavior or infinite loops. Doing that for a complex program will require formulating useful invariants and proving those. So even if using the trivial specification for the overall program, you'll likely find that the proof will require you to write actually useful specifications for several components of your program (because the program likely contains code that relies on the correctness of the component, in order to prove absence of crashes in the code using the component).

zozbot234• 1 year ago

to prove this trivial specification as correct, you need to prove the absence of panics, undefined behavior or infinite loops.

Note that Rust supports this already for a significant subset of code, namely 'const fn' code. This is also the subset of Rust that could most feasibly be extended to support something akin to theorem proving since it's supposed to be safely evaluated "at compile time", just like a Coq proof term or script. If Rust had some simple but comprehensive support for raw "proof terms" - namely, expressions evaluated at compile time which could either result in () or abort the build, I assume that much of the "convenience" features involved in an actual theorem prover could be implemented as macros and live in custom crates. But we don't know what a raw "proof term" could look like in Rust for useful program properties.

UltraSane• 1 year ago

AWS says that when code has a good set of formal verification they can be as aggressive as possible in performance optimization without having to worry they are breaking the logic of the code. This helped them double the performance of the IAM ACL evaluation code.

yodsanklai• 1 year ago

I learned recently that the Coq project was renamed Rocq https://rocq-prover.org.

rafram2• 1 year ago

Probably the right move.

bigstrat2003• 1 year ago

Definitely not the right move. The old name was perfectly fine and allowed for harmless fun. They can obviously do what they wish, but IMO there's no good reason to destroy good clean fun just because it might upset the occasional person.

lelandfe2• 1 year ago

Not even a wink or a nudge about why they renamed: https://rocq-prover.org/about#Name

SubjectToChange3• 1 year ago

The linked discussion is upfront about the name change, if it wasn't already obvious.

https://coq.discourse.group/t/coq-community-survey-2022-resu...

sitkack• 1 year ago

Speaking of https://www.why3.org/

For completeness https://github.com/creusot-rs/creusot

The French were right about so many things.

lsuresh• 1 year ago

Related: Verus (verified Rust): https://github.com/verus-lang/verus

It's aimed more at full systems verification (been used to build verified filesystems, kubernetes controllers etc...).

eggy• 1 year ago

I am just starting out with the ironclad kernel and the gloire OS built on top of it [1,2]. From the web page:

  "Ironclad is a formally verified, real-time capable, UNIX-like operating system kernel for general-purpose and embedded uses. It is written in SPARK and Ada, and is comprised of 100% free software."

I recall AdaCore working with Ferrous Systems a while back. Did anything come of it for rust? I believe one of the non-starters is rust does not have a formal standards specification like C, Common Lisp, or other PLs. It's hard to develop formal verification systems for a moving target.

SPARK has formal verification tools and a legacy of high-integrity applications. The Ironclad kernel is progressing towards a substantially, formally verified kernel written in SPARK. Gloire is an OS implemented on top of Ironclad for PoC.

I have sort of given up on rust, because I just don't find it enjoyable. I am working with Zig. This would be a good direction for Zig to take. Glad to see the effort here. I'll have to check it out a bit more.

[1] https://ironclad.nongnu.org/

[2] https://github.com/Ironclad-Project/Gloire?tab=readme-ov-fil...

steveklabnik• 1 year ago

Did anything come of it for rust?

They parted ways, and both are selling Rust compilers.

I believe one of the non-starters is rust does not have a formal standards specification like C

It's not an issue in practice.

Pelayu• 1 year ago

Does anyone know of any good resources explaining how a theorem prover like Coq is actually used to prove safety properties of software? All the resources I’ve found thus far have been more in the pure mathematics domain, and not so much about applying it to software.

lheck• 1 year ago

Colleagues of mine are using it to verify concurrent programs: https://iris-project.org/tutorial-material.html

SubjectToChange3• 1 year ago

Software Foundations is quite a comprehensive series on program verification.

diegolas• 1 year ago

should've been called roost

Coq-of-rust: Formal verification tool for Rust

Related Stories