Verus: Verified Rust for low-level systems code(github.com)
github.com
Verus: Verified Rust for low-level systems code
https://github.com/secure-foundations/verus
52 comments
I think that for a guarantee as central as non-panicking, there ought to be eventually some kind of support in the core language.
(Just throwing ideas here, but there could be `#[never_panic]` for simple cases where the compiler can clearly see that panic is not possible, or error otherwise, and `#[unsafe(never_panic)]` for more involved cases, that could be proven with 3rd party tools or by reasoning by the developer like normal unsafe blocks.)
For more complicated guarantees, it's harder to see if there's enough common ground for these tools to have some kind of common ground.
(Just throwing ideas here, but there could be `#[never_panic]` for simple cases where the compiler can clearly see that panic is not possible, or error otherwise, and `#[unsafe(never_panic)]` for more involved cases, that could be proven with 3rd party tools or by reasoning by the developer like normal unsafe blocks.)
For more complicated guarantees, it's harder to see if there's enough common ground for these tools to have some kind of common ground.
I think the current plan is to integrate never-panic into the upcoming effect system (formerly keyword generics), along with const and async. So all these function annotations can share the same behavior and syntax, and higher order functions can be generic over them (e.g. "iterator.map(f) is never-panic if f is never-panic" etc)
> effect system (formerly keyword generics)
Any recent link about that? Specially one that calls it effect system rather than the old name keyword generics
Any recent link about that? Specially one that calls it effect system rather than the old name keyword generics
Here's a semi-recent link (~a year ago) by one of the leaders of this initiative: https://blog.yoshuawuyts.com/extending-rusts-effect-system/
Normal rust can already do this. For example #[no_panic] attribute is implemented in https://github.com/dtolnay/no-panic crate.
Via an unreliable, linker-based hack.
On one hand you are right. On the other hand knowing it can't panic because the code is literally not there is a very strong guarantee.
[deleted]
A common specification language is a very ongoing discussion, we just haven't managed to find an agreement yet.
Things like `#[no_panic]` make sense, but it also doesn't require a spec language at all, the compiler already has support for these kinds of annotation and anyone could catch it. Though I cannot think of a single verification use case where all I want to check is the absence of panic.
Things like `#[no_panic]` make sense, but it also doesn't require a spec language at all, the compiler already has support for these kinds of annotation and anyone could catch it. Though I cannot think of a single verification use case where all I want to check is the absence of panic.
> single verification use case where all I want to check is the absence of panic.
Basically any decoder/deserializer. It might be sufficient to handle the correctness in tests but panics are the most severe thing you want to avoid.
How well `#[no_panic]` actually works in practice?
There might be cases where e.g. index access violation never happen but compiler might still think that it happes. I could be impossible to restructure code without adding some performance overhead.
Basically any decoder/deserializer. It might be sufficient to handle the correctness in tests but panics are the most severe thing you want to avoid.
How well `#[no_panic]` actually works in practice?
There might be cases where e.g. index access violation never happen but compiler might still think that it happes. I could be impossible to restructure code without adding some performance overhead.
#[no_panic] has false-positives, but no false-negatives. If it’s present, the code won’t panic and can’t panic.
Index access violation that “never happens” is the root of every buffer overflow, so I’m absolutely OK with the minimal overhead behind the bounds check for actual safety
Index access violation that “never happens” is the root of every buffer overflow, so I’m absolutely OK with the minimal overhead behind the bounds check for actual safety
> Though I cannot think of a single verification use case where all I want to check is the absence of panic.
Not for verification but in terms of ease of use, having no panic in a program means it would be fine and safe to have pointers to uninitialized memory (it's currently not because panics means your destructors can be run anywhere in the code, so everything must be initialized at all time in safe rust).
Not for verification but in terms of ease of use, having no panic in a program means it would be fine and safe to have pointers to uninitialized memory (it's currently not because panics means your destructors can be run anywhere in the code, so everything must be initialized at all time in safe rust).
One more case where the halting problem adds more confusion than it helps. The halting problem is equivalent to the acceptance problem, which is equivalent to the reachability problem.
>Though I cannot think of a single verification use case where all I want to check is the absence of panic.
You can reduce any static verification task to a check for a condition that produces a panic. In short, sprinkle your pre, post and intermediate conditions all over your code in a way that produces a panic (known as asserts) and the tool will do the heavy lifting.
>Though I cannot think of a single verification use case where all I want to check is the absence of panic.
You can reduce any static verification task to a check for a condition that produces a panic. In short, sprinkle your pre, post and intermediate conditions all over your code in a way that produces a panic (known as asserts) and the tool will do the heavy lifting.
See the related work section in the SOSP 2024 paper. I think verification speed is one of the main benefits of verus.
https://www.andrew.cmu.edu/user/bparno/papers/verus-sys.pdf
https://www.andrew.cmu.edu/user/bparno/papers/verus-sys.pdf
[deleted]
Would it be better to build dependent types into the language itself so that we can guarantee any spec we want? Or do these tools have some advantage over dependent typing?
From glancing at https://www.andrew.cmu.edu/user/bparno/papers/verus-ghost.pd... it is more related than you think.
- The various "modes" are going to be needed either way, because side-effectful functions at the type level are a research problem that probably isn't worth the effort.
- The in the pure functional "promotable" fragment, it probably also makes sense to relax aliasing rules / have infinite number types / etc. because all the stuff is going to compile away anyways.
I hope projects like this catch on, and incentivize Rust getting a stronger type system, because the benefits will flow in both directions.
- The various "modes" are going to be needed either way, because side-effectful functions at the type level are a research problem that probably isn't worth the effort.
- The in the pure functional "promotable" fragment, it probably also makes sense to relax aliasing rules / have infinite number types / etc. because all the stuff is going to compile away anyways.
I hope projects like this catch on, and incentivize Rust getting a stronger type system, because the benefits will flow in both directions.
Oh wow, that's incredibly cool. (tldr: the authors of Verus, mostly university researchers, are already thinking in this direction).
I think having guardrails like this is going to incredibly important as AI code gen starts taking a bigger role. Hopefully, as a separate comment mentioned, there can be a standard created so that AI tools can learn it more easily.
I think having guardrails like this is going to incredibly important as AI code gen starts taking a bigger role. Hopefully, as a separate comment mentioned, there can be a standard created so that AI tools can learn it more easily.
My feeling is that dependent types add complexity to a language that's already well-known for having a complex type system, so I'm nervous about blowing the complexity budget. But I'm bullish on tools like Verus, Prusti, and Creusot because they allow people who need to write low-level unsafe code to prove their code safe, while keeping the complexity of the safety proofs localized to that code, so most Rust programmers don't need to worry about it. This allows verification of Rust code without surfacing complexity to most developers. We can have our cake and eat it too.
Agreed. Rust is on track to becoming a practical language for many verification projects. If necessary, perhaps a dialect that focuses on verification could be made and separately maintained (it would probably cut out a lot of normal Rust), or one would just switch to a different technology.
I am not aware of a viable "dependent type system". Such ones as we have are very complicated and not generally a good engineering trade off.
It is The Dream in some ways, but it is much, much easier said than done.
It is The Dream in some ways, but it is much, much easier said than done.
We've head them for 20 years. Lean is getting a lot of attention. Dependent types are not very complicate --- proofs are very complicated, but that is inherent. Dependent types are "only pay for what you prove" --- if you don't try to prove anything there is no problem.
I'll cop to the word "viable" doing a lot of heavy lifting there, but I have not yet seen a dependent typing system that is adequate for engineering work. There are research systems, yes, and there are many people doing laudable work on it, but when people on HN pine for "dependent type systems", I think they're talking about wanting to live in a world where most people who are programming today are instead programming in dependently-typed systems happily and productively, not a world where all programmers not functioning at a PhD-candidate level are evicted from the profession because they can't handle proof languages.
Or, to put it another way, there is no dependently-typed language I can even consider saying to my manager "Hey, you asked me to do X and I think I'll use language Y which is dependently typed", and as far as I can see, the problem isn't just that "nobody has built the standard library for it yet" or any thing else, the problem boils down to, they just aren't easy enough to use to call them practical.
I'd also say that "hey, you can use this dependently-typed language, just don't try to actually use the dependently-typed features" is also not what people are pining for.
Or, to put it another way, there is no dependently-typed language I can even consider saying to my manager "Hey, you asked me to do X and I think I'll use language Y which is dependently typed", and as far as I can see, the problem isn't just that "nobody has built the standard library for it yet" or any thing else, the problem boils down to, they just aren't easy enough to use to call them practical.
I'd also say that "hey, you can use this dependently-typed language, just don't try to actually use the dependently-typed features" is also not what people are pining for.
> not a world where all programmers not functioning at a PhD-candidate level are evicted from the profession because they can't handle proof languages.
Well, to be fair, I would not cry if this happened.
> Or, to put it another way, there is no dependently-typed language I can even consider saying to my manager "Hey, you asked me to do X and I think I'll use language Y which is dependently typed", and as far as I can see, the problem isn't just that "nobody has built the standard library for it yet" or any thing else, the problem boils down to, they just aren't easy enough to use to call them practical.
I wrote a tic-tac-toe in Lean. https://github.com/Ericson2314/lean-tic-tac-toe/. Yes, it took me far longer than I would have in Haskell, but that is just because:
1. Unfamiliarity with the standard library, tooling etc. I didn't expect Applicative to be in mathlib not batteries, for example.
2. I tried to prove things I wouldn't have in the Haskell version
If I knew the standard library, and did plane old arbitrary-length lists and partial (bounds-checked) indexing with arbitrary nats, I would have had less fun, but also done things way faster.
I am excited for the latest Machine-Learning tactics or whatever too, but the idea that "everything is going to do something they didn't before (proofs) and it will be no harder" is not a goal I am aiming for. Proofs will always be a trade-off between up-front costs and fearless refactoring on an ongoing basis. That's OK! I don't expect magic, I just want my programming language to give me the full spectrum of options, and then I can make my own economic decisions.
Well, to be fair, I would not cry if this happened.
> Or, to put it another way, there is no dependently-typed language I can even consider saying to my manager "Hey, you asked me to do X and I think I'll use language Y which is dependently typed", and as far as I can see, the problem isn't just that "nobody has built the standard library for it yet" or any thing else, the problem boils down to, they just aren't easy enough to use to call them practical.
I wrote a tic-tac-toe in Lean. https://github.com/Ericson2314/lean-tic-tac-toe/. Yes, it took me far longer than I would have in Haskell, but that is just because:
1. Unfamiliarity with the standard library, tooling etc. I didn't expect Applicative to be in mathlib not batteries, for example.
2. I tried to prove things I wouldn't have in the Haskell version
If I knew the standard library, and did plane old arbitrary-length lists and partial (bounds-checked) indexing with arbitrary nats, I would have had less fun, but also done things way faster.
I am excited for the latest Machine-Learning tactics or whatever too, but the idea that "everything is going to do something they didn't before (proofs) and it will be no harder" is not a goal I am aiming for. Proofs will always be a trade-off between up-front costs and fearless refactoring on an ongoing basis. That's OK! I don't expect magic, I just want my programming language to give me the full spectrum of options, and then I can make my own economic decisions.
> Dependent types are "only pay for what you prove" --- if you don't try to prove anything there is no problem.
I have to disagree with this, since fully general dependent types seem to inherently involve a kind of compile-time evaluation. You can recover a sort of phase distinction (i.e. a post-compile "run time" phase) but only AIUI through an "extraction" step that dispenses with the actual dependently typed parts of the program.
I have to disagree with this, since fully general dependent types seem to inherently involve a kind of compile-time evaluation. You can recover a sort of phase distinction (i.e. a post-compile "run time" phase) but only AIUI through an "extraction" step that dispenses with the actual dependently typed parts of the program.
> You can recover a sort of phase distinction
Yes the literature says how to do this. It's not hard. Any program that could be written in something weaker like System F will have the same erasure.
> inherently involve a kind of compile-time evaluation.
compile-time evaluation doesn't pose a phase-separation problem. Indeed, nothing to the right of a `:` will ever need to be evaluated on runtime.
Yes the literature says how to do this. It's not hard. Any program that could be written in something weaker like System F will have the same erasure.
> inherently involve a kind of compile-time evaluation.
compile-time evaluation doesn't pose a phase-separation problem. Indeed, nothing to the right of a `:` will ever need to be evaluated on runtime.
Personally, I think the verus! macro is too much in the way for this approach to be feasible. Kani or Prusti syntax is much more usable for real projects.
love another rust project! are there plans to expand support for concurrency primitives or async constructs in future releases?
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.
> 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.
Tests 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.
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]
Tests 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.
both have their place.
Yes, 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.
Buffer overflows etc. are absurd things that should not be possible, but preventing them is the first step towards security.
This is something that Rust should prevent, not another layer on top of Rust.
Buffer 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.
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.
Yes, it should make sure that there are not buffer overflows, but this is the next step.
[deleted]
Why is verification excessive but not tests?
A verification of a property is stronger than a mere test of a property.
A verification of a property is stronger than a mere test of a property.
The test is supposed to be the verification.
Test verify that the code works on specific inputs. Formal verification checks that it works on every input.
Can't you make the tests check every input? (This is also what they're supposed to do.)
I don't know why you are trolling us. Tests aren't supposed to check every input. The entire point of classic testing is to define static execution traces by hand. That is obviously meant to only cover a finite number of execution traces. Even 100% test coverage doesn't give you proof over all possible execution traces. Tests prove that the software "works", but they do not prove the absence of bugs (which inherently requires you to specify what a "bug" is, hence the need for a specification).
Not only is static verification more powerful, there is also a massive usability difference. You define your pre and post conditions in each function (also known as specification or design contract) and the tool will automatically check that you do not violate these conditions. It solves a very different problem from classic unit or integration tests.
Not only is static verification more powerful, there is also a massive usability difference. You define your pre and post conditions in each function (also known as specification or design contract) and the tool will automatically check that you do not violate these conditions. It solves a very different problem from classic unit or integration tests.
Obviously 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.
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.
Indeed. 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.
But why? Tests can't catch everything. A single verified predicate is equivalent to a very large, potentially infinite number of tests.
Right now the Rust stdlib is being verified using Kani, a model checker, https://model-checking.github.io/verify-rust-std/
In Kani, a proof looks like this
https://github.com/model-checking/verify-rust-std/blob/00169...
https://github.com/model-checking/verify-rust-std/blob/00169...
That's a kind of trivial contract but Kani tests for all possible pointers (rather than some cherry picked pointers like the null pointer and something else), without actually brute-forcing them but instead recognizing when many inputs test the same thing (while still catching a bug if the code changes to handle some input differently). And this approach scales for non-trivial properties too, a lot of things in the stdlib have non-trivial invariants.
You can check out other proofs here https://github.com/search?q=repo%3Amodel-checking%2Fverify-r...
It's not that different from writing a regular test, it's just more powerful. And you can even use this #[requires] and #[ensures] syntax to test properties in regular tests if you use the https://crates.io/crates/contracts crate.
Really if you have ever used the https://proptest-rs.github.io/proptest/intro.html or the https://crates.io/crates/quickcheck crate, software verification is like writing a property test, but rather than testing N examples generated at random, it tests all possible examples at once. And it works when the space of possible examples is infinite or prohibitively large, too.
Right now the Rust stdlib is being verified using Kani, a model checker, https://model-checking.github.io/verify-rust-std/
In Kani, a proof looks like this
https://github.com/model-checking/verify-rust-std/blob/00169...
#[kani::proof_for_contract(NonNull::new_unchecked)]
pub fn non_null_check_new_unchecked() {
let raw_ptr = kani::any::<usize>() as *mut i32;
unsafe {
let _ = NonNull::new_unchecked(raw_ptr);
}
}
https://github.com/model-checking/verify-rust-std/blob/00169...
#[requires(!ptr.is_null())]
#[ensures(|result| result.as_ptr() == ptr)]
That's a kind of trivial contract but Kani tests for all possible pointers (rather than some cherry picked pointers like the null pointer and something else), without actually brute-forcing them but instead recognizing when many inputs test the same thing (while still catching a bug if the code changes to handle some input differently). And this approach scales for non-trivial properties too, a lot of things in the stdlib have non-trivial invariants.
You can check out other proofs here https://github.com/search?q=repo%3Amodel-checking%2Fverify-r...
It's not that different from writing a regular test, it's just more powerful. And you can even use this #[requires] and #[ensures] syntax to test properties in regular tests if you use the https://crates.io/crates/contracts crate.
Really if you have ever used the https://proptest-rs.github.io/proptest/intro.html or the https://crates.io/crates/quickcheck crate, software verification is like writing a property test, but rather than testing N examples generated at random, it tests all possible examples at once. And it works when the space of possible examples is infinite or prohibitively large, too.
Say I have as input a byte. I create a test that exercises every possible byte value.
A verification would be the equivalent of that. In practice that matters since the input space is often much larger than just one byte.
A verification would be the equivalent of that. In practice that matters since the input space is often much larger than just one byte.
> 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.
Well, Rust doesn't yet have taint checking or effects, so there's two things lacking.
if 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
I feel, with more and more tools crowding that space, a common specification language would make sense. Sure, every tool has its own unique selling points but there is considerable overlap. For example, if all I want is to express that I expect a function not to panic, there should be one syntax that works with all tools.