Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Verus: Verified Rust for low-level systems code

github.com

Post reply on HN
Print view View original

11–20 of 53 posts

Re: Verus: Verified Rust for low-level systems code

#11

Post by giltho »

weinzierl wrote: post #3

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.

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.

Re: Verus: Verified Rust for low-level systems code

#12

Post by rice7th »

worldsavior wrote: post #9

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.

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.

Re: Verus: Verified Rust for low-level systems code

#13

Post by GolDDranks »

noxer wrote: post #8
GolDDranks wrote: post #6

Earlier quoted context omitted.

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 develope…

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.

Re: Verus: Verified Rust for low-level systems code

#14

Post by bluGill »

worldsavior wrote: post #9

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.

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.

Re: Verus: Verified Rust for low-level systems code

#15

Post by nicce »

giltho wrote: post #11
weinzierl wrote: post #3

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.

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.

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

Re: Verus: Verified Rust for low-level systems code

#16

Post by littlestymaar »

giltho wrote: post #11
weinzierl wrote: post #3

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.

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.

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

Re: Verus: Verified Rust for low-level systems code

#17

Post by keybored »

worldsavior wrote: post #9

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.

Why is verification excessive but not tests?

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

Re: Verus: Verified Rust for low-level systems code

#19

Post by rowanG077 »

GolDDranks wrote: post #13
noxer wrote: post #8

Earlier quoted context omitted.

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.

Re: Verus: Verified Rust for low-level systems code

#20

Post by Conscat »

worldsavior wrote: post #9

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.

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

Post reply on HN