Live data from Hacker News

Prusti: Static Analyzer for Rust

github.com

21–30 of 93 posts

Re: Prusti: Static Analyzer for Rust

#21

Why would you need a static analyzer for a language that promotes itself as safe out of the box.

Rust promises that safe rust is memory/type safe. You can still get interger over/under-flows, indexing out of bounds, and allocation failures (oom), etc... all of which "panic" - which means that rust will safely unwind the stack and exit in a way that remains memory safe.

Re: Prusti: Static Analyzer for Rust

#22
post #16
post #15

Earlier quoted context omitted.

It is safe for the 70% of security flaws found out in languages like C and C++. The remaining 30% still need to be tracked down.

I wonder where you got those numbers from.

https://alexgaynor.net/2019/aug/12/introduction-to-memory-un...

Re: Prusti: Static Analyzer for Rust

#23
I don't understand how this could work from looking at the readme. It says:

> verifies absence of integer overflows and panics by proving that statements such as unreachable!() and panic!() are unreachable

But integer overflows in release builds don't panic! and aren't unreachable!. Additionally, clippy already checks this for you if you enable an optional lint.

So if it detects any panic! Then that's amazing. But if it only detects panic for integer operations, we already have that feature. Either way, the overflow/panic! wording is confusing because it either only applies to debug builds or applies to more than integer operations

Re: Prusti: Static Analyzer for Rust

#24
post #2

What are people's experiences with static analyzers at companies? Many people I have spoken with have either never heard of them, or expressed no interest. Usually those same people use dynamic languages like Ruby or Python.

They work really well, and people, while initially skeptical, eventually get the idea. The key is to run a first pass on your codebase, find and fix real bugs, and share your findings. This turns a very theoretical tool into 'see, it works, and that's one nasty bug we won't have in production'.

Re: Prusti: Static Analyzer for Rust

#25
post #2

What are people's experiences with static analyzers at companies? Many people I have spoken with have either never heard of them, or expressed no interest. Usually those same people use dynamic languages like Ruby or Python.

I lead a Go team, and we pretty much never go (heh) anywhere without a suite of static analysers. go vet, govulncheck, errcheck, and staticcheck are the required minimum, but we do use some others.

Back when I used to write Ruby, lack of static analysis was a serious problem. I've been able to add Rubocop later, but it's not exactly on the same level as staticcheck, to say nothing about Prusti from the OP.

Re: Prusti: Static Analyzer for Rust

#26

I don't understand how this could work from looking at the readme. It says: > verifies absence of integer overflows and panics by proving that statements such as unreachable!() and panic!() are unreachable But integer overflows in release builds don't panic! and aren't unreachable!. Additionally, clippy already checks this for you if you enable an optional lint. So if it detects any panic! Then that's amazing. But if…

You can enable (or disable) panic-on-overflow in Rust via a compiler flag or the corresponding value in Cargo.toml: https://doc.rust-lang.org/cargo/reference/profiles.html#over...

Re: Prusti: Static Analyzer for Rust

#27

I don't understand how this could work from looking at the readme. It says: > verifies absence of integer overflows and panics by proving that statements such as unreachable!() and panic!() are unreachable But integer overflows in release builds don't panic! and aren't unreachable!. Additionally, clippy already checks this for you if you enable an optional lint. So if it detects any panic! Then that's amazing. But if…

You are overthinking things. Those are just usee to mark places in the control flow it tries to proove are unreachable. The meaning of those constructs is irrelevant.

Re: Prusti: Static Analyzer for Rust

#28
post #26

I don't understand how this could work from looking at the readme. It says: > verifies absence of integer overflows and panics by proving that statements such as unreachable!() and panic!() are unreachable But integer overflows in release builds don't panic! and aren't unreachable!. Additionally, clippy already checks this for you if you enable an optional lint. So if it detects any panic! Then that's amazing. But if…

You can enable (or disable) panic-on-overflow in Rust via a compiler flag or the corresponding value in Cargo.toml: https://doc.rust-lang.org/cargo/reference/profiles.html#over...

> If not specified, overflow checks are enabled if debug-assertions are enabled, disabled otherwise

Both of the values you can set don't give you a warning though. The linked article is about producing a warning or error when there can possibly be an overflow/panic, which clippy already does.

Edit: here's the lint that warns you that a panic or overflow can be caused: https://rust-lang.github.io/rust-clippy/master/#integer_arit...

Re: Prusti: Static Analyzer for Rust

#29
post #2

What are people's experiences with static analyzers at companies? Many people I have spoken with have either never heard of them, or expressed no interest. Usually those same people use dynamic languages like Ruby or Python.

I'm a "hard core PLer" and I am skeptical. I don't like automated solvers where there is no way to manually include a proof (to be checked).

Re: Prusti: Static Analyzer for Rust

#30

Why would you need a static analyzer for a language that promotes itself as safe out of the box.

It is written in the linked README, but I will state it here. Rust checks integer overflows at runtime (or not at all, if building for maximum speed). It is safer than not checking at all. But costs performance and can lead to (predictable) crashes. This tool is a way to prove that overflows can not happen at compile time. Which is extremely hard in the general case.

Also note that the reason that Rust can get away with not checking for integer overflow while still being memory-safe is because indexing operations are bounds-checked, so an overflowing index variable panics anyway.
Post reply on HN