4 ms·

Coq-of-rust: Formal verification tool for Rust

159 points by todsacerdoti 2y ago

diegolas 2y ago
should've been called roost
jedisct1 2y ago
Do that for Zig.
- arn3n 2y 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 https://graydon2.dreamwidth.org/312681.html
  - porridgeraisin 2y ago
    The link returns 403.
    - johnisgood 2y ago
      It (still) works for me.
  - johnisgood 2y 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.
    - gaugefield 2y ago
      While this does not mention it, in many other discussions Rust vs Ada is mentioned. My (late) introduction to Ada via was finding out in one of the Rust forums.
  - throwawaymaths 2y 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.
- throwawaymaths 2y ago
  probably zig air is a better target: https://github.com/ityonemo/clr https://github.com/ityonemo/clr https://m.youtube.com/watch?v=ZY_Z-aGbYm8 https://m.youtube.com/watch?v=ZY_Z-aGbYm8
SAI_Peregrinus 2y 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-zero 2y ago
  You are describing "validation": the process of verifying that your spec really says what you mean.
  - nicce 2y ago
    He is saying that original spec can be incorrect.
    - jghn 2y ago
      Yes. And the post you're replying to is pointing out that that would be part of `Validation` to decide. Verification is confirming the software meets the spec. Validation is confirming that the software meets the actual desired behavior.
      - nicce 2y ago
        I think the comment was way shorter than it currently is when I replied. It is sometimes difficult to say what is meant with "validation". Many also use it to mean "functional testing", for example, which is incorrect.
yodsanklai 2y ago
I learned recently that the Coq project was renamed Rocq https://rocq-prover.org https://rocq-prover.org.
- rafram 2y ago
  Probably the right move.
  - bigstrat2003 2y 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.
    - rafram 2y ago
      The developers of a serious academic tool may not have wanted their image to be "harmless fun," especially of a sort that can reasonably offend people and make it hard to talk about in formal settings. "Let's try [something that sounds like rock]" is going to be an easier sell to your boss than "Let's try [something that sounds like cock]."
- lelandfe 2y ago
  Not even a wink or a nudge about why they renamed: https://rocq-prover.org/about#Name https://rocq-prover.org/about#Name
  - SubjectToChange 2y 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-results-part-iv-and-itp-paper-announcement/2001 https://coq.discourse.group/t/coq-community-survey-2022-resu...
    - lelandfe 2y ago
lsuresh 2y ago
Related: Verus (verified Rust): https://github.com/verus-lang/verus https://github.com/verus-lang/verus It's aimed more at full systems verification (been used to build verified filesystems, kubernetes controllers etc...).
eggy 2y 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/ https://ironclad.nongnu.org/ [2] https://github.com/Ironclad-Project/Gloire?tab=readme-ov-file https://github.com/Ironclad-Project/Gloire?tab=readme-ov-fil...
- steveklabnik 2y 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 2y 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 2y ago
  Colleagues of mine are using it to verify concurrent programs: https://iris-project.org/tutorial-material.html https://iris-project.org/tutorial-material.html
- SubjectToChange 2y ago
  Software Foundations is quite a comprehensive series on program verification.

159 points by todsacerdoti 2y ago

diegolas 2y ago

should've been called roost

jedisct1 2y ago

Do that for Zig.

arn3n 2y 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 https://graydon2.dreamwidth.org/312681.html
- porridgeraisin 2y ago
  The link returns 403.
  - johnisgood 2y ago
    It (still) works for me.
- johnisgood 2y 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.
  - gaugefield 2y ago
    While this does not mention it, in many other discussions Rust vs Ada is mentioned. My (late) introduction to Ada via was finding out in one of the Rust forums.
- throwawaymaths 2y 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.
throwawaymaths 2y ago
probably zig air is a better target: https://github.com/ityonemo/clr https://github.com/ityonemo/clr https://m.youtube.com/watch?v=ZY_Z-aGbYm8 https://m.youtube.com/watch?v=ZY_Z-aGbYm8

SAI_Peregrinus 2y 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-zero 2y ago
You are describing "validation": the process of verifying that your spec really says what you mean.
- nicce 2y ago
  He is saying that original spec can be incorrect.
  - jghn 2y ago
    Yes. And the post you're replying to is pointing out that that would be part of `Validation` to decide. Verification is confirming the software meets the spec. Validation is confirming that the software meets the actual desired behavior.
    - nicce 2y ago
      I think the comment was way shorter than it currently is when I replied. It is sometimes difficult to say what is meant with "validation". Many also use it to mean "functional testing", for example, which is incorrect.

yodsanklai 2y ago

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

rafram 2y ago
Probably the right move.
- bigstrat2003 2y 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.
  - rafram 2y ago
    The developers of a serious academic tool may not have wanted their image to be "harmless fun," especially of a sort that can reasonably offend people and make it hard to talk about in formal settings. "Let's try [something that sounds like rock]" is going to be an easier sell to your boss than "Let's try [something that sounds like cock]."
lelandfe 2y ago
Not even a wink or a nudge about why they renamed: https://rocq-prover.org/about#Name https://rocq-prover.org/about#Name
- SubjectToChange 2y 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-results-part-iv-and-itp-paper-announcement/2001 https://coq.discourse.group/t/coq-community-survey-2022-resu...
  - lelandfe 2y ago

lsuresh 2y ago

Related: Verus (verified Rust): https://github.com/verus-lang/verus https://github.com/verus-lang/verus It's aimed more at full systems verification (been used to build verified filesystems, kubernetes controllers etc...).

eggy 2y 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/ https://ironclad.nongnu.org/ [2] https://github.com/Ironclad-Project/Gloire?tab=readme-ov-file https://github.com/Ironclad-Project/Gloire?tab=readme-ov-fil...

steveklabnik 2y 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 2y 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 2y ago
Colleagues of mine are using it to verify concurrent programs: https://iris-project.org/tutorial-material.html https://iris-project.org/tutorial-material.html
SubjectToChange 2y ago
Software Foundations is quite a comprehensive series on program verification.