3 ms·
Rust is supposed to be a "safe" language for low level use, and thus has borrow checker, unsafe, etc. Building a "verifier" on top of Rust seems a bit excessive
by worldsavior 1y ago
Rust is supposed to be a "safe" language for low level use, and thus has borrow checker, unsafe, etc. Building a "verifier" on top of Rust seems a bit excessive and unneeded.
> Developers write specifications of what their code should do ... Verus statically checks ... the specifications for all possible executions of the code
This is what tests are for.
- ramon156 1y agoif i read it correctly, it also checks raw memory access during compilation. My assumption is that it also checks unsafe blocks, which is important when working with low level
- rice7th 1y agoTests do not account for all possible executions of the code, rather only a subset of it. Rust is indeed a safe language, in terms of memory safety. Vulnerabilities are still very possible within a rust program, they just need to not rely on memory exploits, and the borrow checker won't catch them. That is why formal verification exists. If you have a really critical, high security application then you should ensure the maximum amount of safety and reliability. Formal verification enables the developer to write a mathematical proof that the program behaves correctly in all situations, something that the borrow checker cannot do.
- deleted 1y ago[deleted]
- bluGill 1y agoTests and proofs cover very different things. For large code bases getting all the requirements rights is nearly impossible while tests tendto be obvious - even if we don't have the requirements right (or at all) this one fact is true in this one case. However the marjority of cases are not covered at all and so you only hope they work. both have their place.
- keybored 1y agoWhy is verification excessive but not tests? A verification of a property is stronger than a mere test of a property.
- worldsavior 1y agoThe test is supposed to be the verification.
- GolDDranks 1y agoTest verify that the code works on specific inputs. Formal verification checks that it works on every input.
- worldsavior 1y agoCan't you make the tests check every input? (This is also what they're supposed to do.)
- sangel 1y agoObviously not. Suppose the input to my function is a 64-bit integer. My test cannot possibly try every possible 64-bit integer. It would take years for such a test to finish. This is why tools like formal verification and symbolic analyses can help you establish that for all possible integers X, your function does the right thing (for some definition of “right”). You get this assurance without having to actually enumerate all X.
- stephencanon 1y agoIndeed. Exhaustively testing a 64b input space requires about 600 machine years for each nanosecond that the function under test takes to run. So, _very_ short-running critical functions are testable on a cluster, but not efficiently testable, and if a function is simple enough to be testable, then it's usually easier to prove that it's correct instead.
- 1y ago
- Conscat 1y ago> Building a "verifier" on top of Rust seems a bit excessive and unneeded. Well, Rust doesn't yet have taint checking or effects, so there's two things lacking.
- impossiblefork 1y agoYes, but remember that Erlang bug discussed here last week where somebody apparently messed up SSH state transitions in such a way that people could just log in without having the password or anything? Buffer overflows etc. are absurd things that should not be possible, but preventing them is the first step towards security.
- worldsavior 1y agoThis is something that Rust should prevent, not another layer on top of Rust.
- impossiblefork 1y agoYes, it should make sure that there are not buffer overflows, but this is the next step.
- deleted 1y ago[deleted]
- trealira 1y agoBuffer overflow vulnerabilities are prevented with bounds checking, but that just means you get a panic at runtime. With formal verification, you can prove that the program never accesses an array with an index that's out of bounds. I guess you're asking why that wasn't built into Rust from the start; after all, there are programming languages with the formal verification and theorem-proving built-in, e.g. for imperative languages, the SPARK extension to Ada, as well as ATS, or for a functional one, Idris. My guess is that Rust never would have become popular if you needed to write actual formal proofs to guarantee some degree of safety, since satisfying the borrow checker is easier in comparison, and it also probably would have been a lot harder to develop Rust after that. The borrow checker simply eliminating use-after-free errors and data races in safe code was good enough.