Verus: Verified Rust for low-level systems code

https://github.com/secure-foundations/verus

by mmcloughlin • 1 year ago

158 48 1 year ago

github.com

bk496• 1 year ago

How many of these are there?

IshKebab• 1 year ago

The main ones are Verus, Prusti and Creusot, but they take quite different approaches. This isn't redundant.

weinzierl• 1 year ago

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.

GolDDranks3• 1 year ago

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• 1 year ago

Normal rust can already do this. For example #[no_panic] attribute is implemented in https://github.com/dtolnay/no-panic crate.

hmry• 1 year ago

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)

giltho• 1 year ago

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• 1 year ago

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.

littlestymaar• 1 year ago

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).

imtringued2• 1 year ago

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.

meling• 1 year ago

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

badmonster• 1 year ago

love another rust project! are there plans to expand support for concurrency primitives or async constructs in future releases?

worldsavior4• 1 year 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• 1 year ago

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• 1 year ago

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• 1 year ago

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.

keybored2• 1 year ago

Why is verification excessive but not tests?

A verification of a property is stronger than a mere test of a property.

worldsavior4• 1 year ago

The test is supposed to be the verification.

Conscat• 1 year 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.

impossiblefork2• 1 year ago

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.

worldsavior4• 1 year ago

This is something that Rust should prevent, not another layer on top of Rust.

daxfohl2• 1 year ago

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?

Ericson23144• 1 year ago

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.

daxfohl2• 1 year ago

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.

jerf2• 1 year ago

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.

Ericson23144• 1 year ago

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.

pcwalton• 1 year ago

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.

vacuity• 1 year ago

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.

yencabulator2• 1 year ago

Previously:

https://news.ycombinator.com/item?id=32105781

https://news.ycombinator.com/item?id=36530561

https://news.ycombinator.com/item?id=35129690

https://news.ycombinator.com/item?id=40259185 (has actual discussion)

yencabulator2• 1 year ago

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.

Verus: Verified Rust for low-level systems code

Related Stories