[HN Gopher] Verus: Verified Rust for low-level systems code
___________________________________________________________________
Verus: Verified Rust for low-level systems code
Author : mmcloughlin
Score : 144 points
Date : 2025-04-20 19:38 UTC (2 days ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| bk496 wrote:
| How many of these are there?
| IshKebab wrote:
| The main ones are Verus, Prusti and Creusot, but they take
| quite different approaches. This isn't redundant.
| weinzierl wrote:
| How does it differ from Prusti and Creusot?
|
| 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.
| GolDDranks wrote:
| 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.
| noxer wrote:
| Normal rust can already do this. For example #[no_panic]
| attribute is implemented in https://github.com/dtolnay/no-
| panic crate.
| GolDDranks wrote:
| Via an unreliable, linker-based hack.
| rowanG077 wrote:
| 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.
| hmry wrote:
| 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)
| nextaccountic wrote:
| > effect system (formerly keyword generics)
|
| Any recent link about that? Specially one that calls it
| effect system rather than the old name keyword generics
| NobodyNada wrote:
| 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/
| giltho wrote:
| 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.
| nicce wrote:
| > 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.
| freeone3000 wrote:
| #[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
| littlestymaar wrote:
| > 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).
| badmonster wrote:
| love another rust project! are there plans to expand support for
| concurrency primitives or async constructs in future releases?
| worldsavior wrote:
| 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 wrote:
| 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
| rice7th wrote:
| 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.
| bluGill wrote:
| 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.
| keybored wrote:
| Why is verification excessive but not tests?
|
| A verification of a property is stronger than a mere test of a
| property.
| worldsavior wrote:
| The test is supposed to be the verification.
| GolDDranks wrote:
| Test verify that the code works on specific inputs. Formal
| verification checks that it works on every input.
| nextaccountic wrote:
| 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...
| #[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); } }
|
| It looks like a test, but actually it is testing that
| _every possible usize_ , when converted to a pointer to i32
| and built with NonNull::new_unchecked, will follow the
| contract of NonNull::new_unchecked, which is defined here
|
| https://github.com/model-checking/verify-rust-
| std/blob/00169...
| #[requires(!ptr.is_null())] #[ensures(|result|
| result.as_ptr() == ptr)]
|
| Which means: if the caller guarantees that the parameter
| ptr is not null, then result.as_ptr() is the same as the
| passed 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.
| keybored wrote:
| 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.
| Conscat wrote:
| > 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 wrote:
| 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.
| worldsavior wrote:
| This is something that Rust should prevent, not another layer
| on top of Rust.
| impossiblefork wrote:
| Yes, it should make sure that there are not buffer
| overflows, but this is the next step.
| trealira wrote:
| 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.
| daxfohl wrote:
| 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?
| Ericson2314 wrote:
| 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.
| daxfohl wrote:
| 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.
| jerf wrote:
| 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.
| Ericson2314 wrote:
| 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.
| jerf wrote:
| 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.
| pcwalton wrote:
| 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.
___________________________________________________________________
(page generated 2025-04-22 23:01 UTC)