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

Prusti: Static Analyzer for Rust

github.com

Post reply on HN
Print view View original

31–40 of 93 posts

Re: Prusti: Static Analyzer for Rust

#31

Post by jerf »

piterdevries wrote: post #8

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

In addition to the many other fine points about how Rust doesn't perfectly secure against everything, having a static analyzer out of the compiler means that the static analyzer can continue to develop on its own time frame without being tied to the compiler releases. The importance of this is easy to underestimate. It is really helpful to have external projects able to iterate independently for this sort of thing.

Re: Prusti: Static Analyzer for Rust

#32

Post by hn92726819 »

Ericson2314 wrote: post #27
hn92726819 wrote: post #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…

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.

I think they're talking about literal panic!() calls though. They used parenthesis in their examples too, which indicates they're probably talking about the macro calls.

This is a static analyzer so I would expect it can trace calls to a panic handler (which both panic! and unreachable! use). I might be overthinking things, but it looks to me like this may be able to detect panic! calls even in, say, stdlib

Re: Prusti: Static Analyzer for Rust

#33

Post by nerdponx »

According to the Readme, this is based on a more-general verification framework called Viper, which apparently works for several languages (including Rust): https://www.pm.inf.ethz.ch/research/viper.html

There also appear to be equivalents of this tool in Python ("Nagini" https://www.pm.inf.ethz.ch/research/nagini.html) and Go ("Gobra" https://www.pm.inf.ethz.ch/research/gobra.html).

I'll definitely be checking out Nagini for my work!

Re: Prusti: Static Analyzer for Rust

#34

Post by wongarsu »

hn92726819 wrote: post #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…

I read that as "verifies (absence of integer overflows) and (panics by proving that statements such as unreachable!() and panic!() are unreachable)".

I think the docs also support this reading, overflow detection and panic detection are listed as separate features [1].

But it is poorly worded, and the readme could certainly be improved.

1: https://viperproject.github.io/prusti-dev/user-guide/verify/...

Re: Prusti: Static Analyzer for Rust

#35

Post by pm215 »

za3faran wrote: 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 find it depends a lot on the static analyzer. (My experience is largely with C code.) In particular, if the analyzer produces a lot of false positives it is dumping a pile of work onto the developers to work through each report and satisfy themselves that it's invalid, and hiding the real bugs under a pile of garbage. If it is more careful to avoid false positives then it's more workable as a development tool (but of course it then finds fewer interesting issues).

The other key static analyzer question is "how easy is it to run and does that happen early in the development cycle?". A static analysis pass built right into the compiler and generating warnings every time you compile has the most chance of having its reports paid attention to. Something that runs at CI time is more annoying. Something that runs only on trunk a week or more behind the leading edge of development and which just lists its reported issues on a webpage somewhere is in grave danger of being outright ignored, or only read by one or two enthusiasts who are forever fixing up other peoples' code...

Re: Prusti: Static Analyzer for Rust

#36

Post by insanitybit »

This is great. I'm building something similar, an effects system for rust, and it looks quite a bit like this. The difference is that my effects system compiles to a seccomp + apparmor profile so that your rust program is sandboxed at runtime based on info at compile time.

I have a notion of purity as well :P

I think the applications of this sort of thing are pretty limitless. Maybe rust has `unsafe` but with further verification extensions to the language we can really push confidence in a working, safe product.

Re: Prusti: Static Analyzer for Rust

#37

Post by Aurel300 »

hn92726819 wrote: post #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…

Yes, we could improve the wording -- suggestions and users are welcome! The tool is indeed much more general purpose than integer overflows: it is a based on a deductive verifier which uses symbolic execution to figure out which nodes in the CFG are reachable and under what conditions. panic!, unreachable!, failed assert!s, etc are all checked. If one can be reached, the error to show to the user is reconstructed from the compiler's span information.

Re: Prusti: Static Analyzer for Rust

#38

Post by turboponyy »

wongarsu wrote: post #12

That looks incredibly useful. Proving the absence of panics and overflows is already great, and with the annotations you can guarantee properties you'd normally write property tests for, like in this example from the docs: impl List { #[ensures(self.len() == old(self.len()) + 1)] pub fn push(&mut self, elem: i32) { // TODO } }

Can't wait for dependently typed type systems

Re: Prusti: Static Analyzer for Rust

#39

Post by mynameisash »

Arch-TK wrote: post #16
pjmlp wrote: 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.

From Microsoft[0]: "As we’ve seen, roughly 70% of the security issues that the MSRC assigns a CVE to are memory safety issues."

And from Google[1]: "memory safety bugs continue to be a top contributor of stability issues, and consistently represent ~70% of Android’s high severity security vulnerabilities."

[0] https://msrc-blog.microsoft.com/2019/07/22/why-rust-for-safe...

[1] https://security.googleblog.com/2021/04/rust-in-android-plat...

Re: Prusti: Static Analyzer for Rust

#40

Post by heywire »

za3faran wrote: 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.

Not sure how relevant my experience is, but I work on a 30+ year old Windows application that started life as a DOS application. It is written in a mix of C and C++. We still do things pretty old school. As part of submitting your work for code review (which is required for every change), you submit the output of cppcheck. When we first introduced cppcheck, there were thousands of warnings and errors that we slowly worked through. Now it is expected that the cppcheck output is empty.
Post reply on HN