8 ms·
Translation of Rust's core and alloc crates to Coq for formal verification
- Havoc 2y agoDidn’t know that is even feasible. I wonder if efforts like this could speed up rust in key parts of kernel adoption
- deleted 2y ago[deleted]
- hgyjdetjj 2y ago[flagged]
- gwervc 2y agoA new name always take time to disseminate after a rebranding, especially when the change is controversial. The most glaring example being X.
- deredede 2y agoThe decision to change the name has been taken by the Coq team, but I believe they do not want the new name to be used until it has been acted administratively, legally and technically (e.g. the documentation should mention the new name and be hosted on rocq.inria.fr).
- speedbird 2y ago[flagged]
- psychoslave 2y agoTrue, W(indow), X, Xfre86, X.org. And you might thought that they would have come with Y and Z next, but no they throw Wayland (name after some locality) instead in your face. How do you want to follow this stuffs? :D
- Narishma 2y agoThere was a Y windowing system. http://www.y-windows.org/ http://www.y-windows.org/
- humzashahid98 2y agoI thought to myself a rename to FACT Prover (Formerly known As Coq Theorem Prover) would be nice when seeing they wanted to rename the project and it's a bit of a disappointment that didn't quite pan out. Rocq is similar to the Roc programming language which is confusing naming (and they sound identical as far as I know).
- rob74 2y agoQuite fittingly, there is a South American bird called Coq of the Rocq... errr, Cock of the Rock: https://en.wikipedia.org/wiki/Cock-of-the-rock https://en.wikipedia.org/wiki/Cock-of-the-rock
- baq 2y agoThe 'problem' was very obviously directed at politically correct English people who have no idea what the word means in other languages. Also, people don't have a problem with the 'git' brand, somehow?
- deredede 2y agoIt is also very likely (if not definitely known) that the name was chosen at least in part because of the English meaning of the word, making the "people have no idea what the word means" argument moot. Outside of France, most users of Coq are in the US where it is taught in many universities. I am sure there were no female professors or TA whose job was made harder purely due to being "the coq teacher" (this is sarcastic, multiple such professors and TAs have mentioned having this type of issues on the Coq mailing list).
- hurutparittya 2y agoOh no, giggling students! Someone do something, quick! I can only imagine the horror.
- cccbbbaaa 2y agoThis is what happens in french classrooms when you talk about bits :-)
- littlestymaar 2y agoDon't forget strings.
- hiddencost 2y agoReminds me of renaming NeurIPS. Another change we're better for.
- baq 2y agoSo teachers complain on the mailing list instead of telling the students to grow the f* up. I don't doubt this is true, but I question the worth of complaints.
- zorked 2y ago> niche theorem prover As opposed to popular theorem provers.
- cjfd 2y agoSince I am both gay and a user of coq, I have had the opportunity to jokingly say that I like coq in all of its spellings. It goes without saying that I am against the name change.
- boxed 2y agoPython has a pretty big naming problem too. Ophidiophobia is the number one phobia in the world, and even though "python" is from Monty Python and not the snake, people keep posting enormous pictures of snakes on book covers and blogs, making it basically impossible for ophidiophobia sufferers to go near python. There are estimates that this is 10% of the population. Now.. do I think Python should change its name? No.
- yau8edq12i 2y agoI am extremely skeptical about the idea that 10% of the population has a phobia of serpents severe enough to avoid learning a programming language named after a kind of snake.
- boxed 2y agoYou mean severe enough to want to avoid being exposed to pictures of snakes. You have to see it from the sufferers perspective.
- thaliaarchi 2y agoThat's really impressive. Automatic translation like this shifts the trust to the tool. coq-of-rust itself is written in Rust, not in Coq. The recursive nature is somewhat boggling, but I think a proof of its correctness is possible in a similar process to David A. Wheeler's “Countering Trusting Trust through Diverse Double-Compiling” (2009) [0] (which circumvents Ken Thompson's Trusting Trusting attack by using a second compiler), but with a mix of a CompCert approach. To verify it, you'd use coq-of-rust to convert the coq-of-rust translator from Rust to Coq. That translation is not trusted, because it was performed in Rust, but it doesn't matter. Once in Coq, you prove the desired correctness properties—crucially, that it preserves the semantics of the Rust program when it translates a program to Coq. As in the article, it is likely easier to work with more functional definitions in proofs instead of generated ones, so you'd undertake the same process as they do with the stdlib of proving equivalence between definitions. Since the current line count for the coq-of-rust translator (specifically, lib/ [1]) is 6350 lines of Rust, it even seems feasible to write a full translator in Coq and prove its equivalence to the generated one. Then, you execute the proven-correct Coq coq-of-rust translator on the Rust source of the coq-of-rust translator. The Coq definitions it outputs should match the output of the Rust coq-of-rust translator that you started with. As an aside, it's nice to see industry funding for work like this. I'm often cynical of cryptocurrency, but its correctness constraints really push for improvements in areas I like (Rust, Coq, funding for masters students I know, etc.). [0]: https://dwheeler.com/trusting-trust/wheelerd-trust.pdf https://dwheeler.com/trusting-trust/wheelerd-trust.pdf [1]: https://github.com/formal-land/coq-of-rust/tree/main/lib https://github.com/formal-land/coq-of-rust/tree/main/lib
- clarus 2y agoThanks for the comment! One of the authors here. Indeed this would be a nice process to verify coq-of-rust. Also, although the code is rather short, we depend on the Rust compiler to parse and type-check the input Rust code. So that would need to be also verified, or at least formally specified without doing the proofs, and the API of rustc is rather large and unstable. It could still be a way to get more insurance.
- deredede 2y ago
- weinzierl 2y agoWhat I don't quite understand with these efforts is this: If we have to translate the code to Coq manually or semi-manually, isn't the likelihood that we make mistakes there much higher than what we ultimately gain with the formal verification. In other words, how do we know that what we proof is still valid for the original code?
- clarus 2y agoThe code is translated automatically with coq-of-rust! When issues are found in the translation they can be fixed once in the coq-of-rust tool, and all the translations are updated.
- weinzierl 2y agoOk, what I think I do not understand is what they mean by "tedious and error prone"? Is it tedious to write the automated translation (aka the coq-of-rust tool in this case) or does the translation of a concrete piece of code (e.g. the core crate) still involve manual work?
- clarus 2y agoThe "tedious and error prone" code was what we were doing before, when the translation of the standard library was not yet working automatically with coq-of-rust. Now, this is automatic. Maybe the explanations on the blog post were not clear.
- bennofs 2y agoYes, that is a limitation. But this limitation is not too bad. In many cases, a bug in the translation simply makes the proof impossible. Somebody then investigates why the proof does not go through and finds the bug in the translation. We only have a problem if the bug in the translation specificially cancels a bug in the original code. If there is no systematic risk, it is quite unlikely that two bugs cancel each other in this way.
- 2y ago
- p4bl0 2y agoNote to interested readers: I submitted this blog post because it is less directly versed in cryptocurrency-related stuff than other posts from the same blog, but there are many more technically interesting posts there, especially the last two discussing the same approach but for Python instead of Rust.
- zem 2y agowonder how much work it would be to add a rust backend to F* [https://github.com/FStarLang/FStar https://github.com/FStarLang/FStar]
- clarus 2y agoIt shoud be possible. A specific feature of Coq that we use is impredicative Set. I do not know if this is the case in F*.
- xavxav 2y agoCan you compare how your approach contrasts to Aeneas or RustHornBelt? How do you handle pointers and mutable borrows?
- clarus 2y agoI do not know how RustHornBelt works. We are focusing on safe code, although we still generate a translation for unsafe blocks as a "best effort". Compared to Aeneas the goal is very similar as we want to verify Rust programs using interactive theorem provers. However, with coq-of-rust we write the purely functional version of the code (the one on which we make proofs) by hand, or with the help of some GitHub Copilot as this is rather repetitive, and prove it equivalent with the automatic translation. In Aeneas the aim is to directly generate a functional version. We handle all the pointers as if they were mutable pointers (the `*` type). We do not use any information from Rust's borrow checker, which simplifies the translation, but we pay that at proof time. To reason about pointers in the proofs, we let the user provide a custom allocator that can be designed depending on how the memory will be used. For example, if the program uses three global mutable variables, the memory can be a record with three entries. These entries are initially `None` to represent when they are not yet allocated. We do not yet know how this technique can scale, but at least we can avoid separation logic reasoning for now. We hope that most of the programs we will verify have a rather "simple" memory discipline, especially on the application side.
- clarus 2y agoI should add that for pointers to immutable data, we can translate them to immutable values on the Coq side. Thus for Rust code written in a purely functional way (using only immutable data structures) the translation is almost one-to-one with Coq, that is to say the same code up to syntactical differences and the verbosity of our monad that behaves like the identity monad in that case. Thus we can provide a path for people who are ready to sacrifice performance for proofs. I guess that immutable Rust is simpler to verify with the other systems too.
- xavxav 2y ago
- fsloth 2y agoTotally not expert on formal verification. If Rust’s base libraries get formally verified, and one does not use unsafe code, does that means all Rust programs that use the formally verified libs get de-facto formally verified quality regarding their memoryhandling?
- hu3 2y agoI'm no Rust expert but it seems to have a lot of unsafe in core code. And understandably so: https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+language%3ARust&type=code&p=5&l=Rust https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+l... I don't think coq, as being presented here, can verify all unsafe calls.
- steveklabnik 2y agoMost of the interest in formalizing Rust is specifically about formalizing the model that unsafe code is supposed to uphold.
- Galanwe 2y agoRust safety has very little to do with bugs. Rust has its own definition of what "safe" means, which is arguably a subset of memory safety. You can have perfectly safe Rust code with data races, deadlocks, memory exhaustion, etc. Not even talking about logical errors.
- dist1ll 2y ago> You can have perfectly safe Rust code with data races No, you can't. Data races are explicitly one type of race condition that Rust protects you from. Anything else would indicate an unsound library or compiler bug. For reference, you can take a look at the non-exhaustive list of undefined behaviors[0]. None of those behaviours should be possible to trigger from safe Rust. [0] https://doc.rust-lang.org/reference/behavior-considered-undefined.html https://doc.rust-lang.org/reference/behavior-considered-unde...
- 2y ago
- pron 2y agoThe size of programs (as opposed to libraries, which could be easier because their code is not nearly as self-interacting) that has been end-to-end verified with semi-automated deductive proof systems like Coq is quite small. In fact, the size of programs that can be verified in this way has grown at a slower pace than the growth in the average size of programs overall. While sound software verification (i.e. a 100% conformance to a spec) certainly has its place (usually to prove the correctness of some core algorithms), it doesn't scale well, which is why there's been a shift in research into unsound methods because the cost of 100% assurance can be 10x that of 99.9999% assurance, and the difference in probability may fall below that of non-software failures (after all, a physical system cannot be proven to conform to a spec) or the probability of a spec that doesn't conform well enough to reality.
- pcwalton 2y agoThe point is that, by proving the unsafe parts of the standard library correct and Rust's safety guarantees correct, we transitively prove the memory safety (as well as data race freedom, etc.) of all safe Rust code (that uses only the standard library). Only proving the unsafe code correct is far less effort than proving all Rust code correct would be. This addresses the common criticism of "what about unsafe code?" when people talk about Rust's safety guarantees. We can use a more powerful system, like Coq, to fill in the gaps that the Rust type system itself isn't powerful enough to handle.
- pron 2y agoSure (assuming Rust's type system were sound, which, I believe, it isn't yet). But my general point -- which isn't at all specific to Rust -- is that with deductive methods, sometimes the effort required may not be worth the added assurance probability they give over unsound methods, while in other cases, deductive methods may be cost-effective. The question of cost-effectiveness is one that always needs to be asked in software assurance. The level of confidence that software requires (as opposed to an abstract algorithm) is not that much higher than one minus the probability of an "unaccounted" failure (such as a hardware failure). Sometimes the extra confidence beyond that point is free, and sometimes it can be very expensive.
- konstantinua00 2y agoI remember lecture [1] that mentioned fuzzer finding bugs in formally-verified C compiler - because formal verification didn't cover frontend and backend I know people raise questions about trust in Coq itself and in translation (and I question how it will synchronize with rust updates), but even perfect formal verification doesn't mean 100% correctness from start to finish [1] https://youtu.be/Ux0YnVEaI6A https://youtu.be/Ux0YnVEaI6A
- the8472 2y agoDid you find any bugs in the crates?
- clarus 2y agoNo, we have not found bugs! We have only scratched the surface and bugs are probably well hidden as the standard library is very well tested. We do not expect to find bugs there, especially as we also assume the unsafe code is safe. Our main hope with the translation to Coq of the standard library is to get a formalization of it, so that we can precisely verify Rust programs calling core and alloc.
- vlovich123 2y agoIs formal verification specification writing similar to writing a more complicated property test? I’ve found writing property tests to be kinda difficult and time consuming for non-trivial programs.
- Jtsummers 2y agoSimilar, not always the same. Property tests generally work at the interface of a system (either down to the function/procedure level or higher level) where you specify a description of the inputs and test the outputs satisfy some property or set of properties. This will look a lot like what you do with formal verification at the same level. Formal verification tools can go deeper, though, like answering questions about the state of the system internal to a computation. Like "I have this loop invariant, can I prove (or have a system prove) that it actually holds across all iterations?" or "Can I prove that while doing this computation there is never underflow/overflow in any intermediate computation?" The former could be done with property testing if you pull the loop kernel out into its own procedure and then test the invariant property by executing the kernel with a large number of intermediate states. The latter is harder to do without really, really tearing your program apart down to the level of making each line separately executable.
- vlovich123 2y agoI think my main point is that writing the specification is difficult enough with a non-trivial program with property tests, with many places tending to even avoid it if they can. If formal verification is even more difficult, it doesn't matter that it has more power and can make the code even more correct - the cost is a huge blocker.
- Jtsummers 2y agoIt depends on how you do the formal verification. There are systems like SPARK/Ada which brings the specification into the language you're developing in (supports only a subset of Ada, but every year they're expanding what it covers), JML which does something similar for Java but the specification language is expressed in its own notation in Java comments, and others. If you use these kinds of systems you can be more judicious in what you try to prove. Whole program proofs are infeasible (or at least impractical) generally, but you pick the subsets you care about most and you can add annotations and prove them (automatically ideally, but you can bring in an external proof assistant as well). You leave the rest of the system to testing which has proven remarkably effective over the decades (when taken seriously, at least). This isn't an all-or-nothing proposition, you choose how to spend your time and effort with formal verification just like you do with testing or other work.
- CrimsonCape 2y agoCould someone ELI5 the concept of "verification", why does an entire language (Coq) exist for this purpose, and what practical implications this has on wider society?