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

71–80 of 93 posts

Re: Prusti: Static Analyzer for Rust

#71

Post by insanitybit »

littlestymaar wrote: post #56
insanitybit wrote: post #36

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…

> 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. That's awesome! I started working to sandbox my Rust program using seccomp-BPF, and I was quickly frustrated about having to run my program with strace to find out what syscalls I should allow for my program, when it sounded like this information should b…

I've wanted to do this for years and I've tried doing it a few times in some weird ways. I'm finally doing it in a hacky but more straightforward way and it's going well.

Re: Prusti: Static Analyzer for Rust

#72

Post by nine_k »

epilys wrote: post #63
Aurel300 wrote: post #51

Earlier quoted context omitted.

This is an active research topic in our group. Within unsafe Rust code you lose the guarantees of the Rust ownership type system, which are important for framing (figuring out which parts of the memory _could_ be affected by the given operations). As a result, for e.g. pointer-manipulating unsafe code, the code will probably need to be annotated more heavily, to track which values are "owned" by whom etc.

Nitpick, unsafe doesn't turn off the borrow checker. It just allows you to dereference raw pointers which are the things you must be careful about by reasoning about the actual safety yourself as a programmer. Everything else that uses safe pointers (references and mutable references) remain safe.

But how passing around a (constant) raw pointer is not sidestepping borrow checker? Since the pointer (AFAICT) does need to be borrowed, because it's manifestly immutable, it could be passed into several functions that alter the pointed-at memory in arbitrary order.

Re: Prusti: Static Analyzer for Rust

#73

Post by fire »

insanitybit wrote: post #70
littlestymaar wrote: post #55

Earlier quoted context omitted.

Can't be certain, but given the content I'm pretty sure that it's these ones: - Github : https://github.com/insanitybit - Twitter: https://twitter.com/InsanityBit

Thanks, yes. I'll add those to my profile.

Nice, followed you on both

Re: Prusti: Static Analyzer for Rust

#74

Post by zozbot234 »

Aurel300 wrote: post #51
Klasiaster wrote: post #45

It doesn't mention unsafe in the README but the website says: The first versions of our tools are under development, and target a small but interesting fragment of Rust without unsafe features; in the future, we plan to extend our work to tackle a large portion of the language, including certain patterns of unsafe Rust code. I wonder if this can be used to prove that unsafe code is memory safe.

This is an active research topic in our group. Within unsafe Rust code you lose the guarantees of the Rust ownership type system, which are important for framing (figuring out which parts of the memory _could_ be affected by the given operations). As a result, for e.g. pointer-manipulating unsafe code, the code will probably need to be annotated more heavily, to track which values are "owned" by whom etc.

It's worth noting that the GhostCell and similar patterns are already powerful enough to safely express some code that would normally require pointer manipulation or other unsafe features. Of course GhostCell itself is quite unidiomatic and unintuitive, but adding a more idiomatic annotation syntax seems like it might be a sensible goal.

Re: Prusti: Static Analyzer for Rust

#75

Post by Yoric »

turboponyy wrote: post #38
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

I've written code with dependently typed languages. It's very powerful, but it really is time-consuming. That won't be appropriate for all developments/developers.

Re: Prusti: Static Analyzer for Rust

#76

Post by Animats »

That's nice. Classic verification. Someday the compiler should do this as part of optimizing run-time checks. Most of the time, either overflow is impossible, or you really needed a run time check.

The static analysis I'd like for Rust is deadlock analysis. If you lock things in different orders in different threads, you can deadlock. That is, if thread A locks X, then Y, and thread B locks Y, then X, there is a potential deadlock. Whole-program static analysis can detect that. It's a good check to have, because infrequent deadlocks of this type may pass testing.

Re: Prusti: Static Analyzer for Rust

#77

Post by nine_k »

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.

Our CI test run includes mypy; even in the mode where it skips certain checks, it finds subtle, non-obvious bugs time and again.

I run mypy as a part of Emacs flycheck mode for Python.

Switching on a static analyzer is usually somehow painful, because old code does not typecheck, or has issues that static analysis discovers but which never get triggered in real life. You have to face constant (and rightful) nagging until you fix all key parts of your code so that the static analyzer no longer has concerns.

In his regard, Python is noticeably behind Typescript, because TS's type system and other amenities allow for more complete and precise descriptions of invariants that hold in the program, and which static analysis tools check.

Re: Prusti: Static Analyzer for Rust

#78

Post by nextaccountic »

Here's a 2020 overview of Rust verification tools https://alastairreid.github.io/rust-verification-tools/ - it says

> Auto-active verification tools

> While automatic tools focus on things not going wrong, auto-active verification tools help you verify some key properties of your code: data structure invariants, the results of functions, etc. The price that you pay for this extra power is that you may have to assist the tool by adding function contracts (pre/post-conditions for functions), loop invariants, type invariants, etc. to your code.

> The only auto-active verification tool that I am aware of is Prusti. Prusti is a really interesting tool because it exploits Rust’s unusual type system to help it verify code. Also Prusti has the slickest user interface: a VSCode extension that checks your code as you type it!

> https://marketplace.visualstudio.com/items?itemName=viper-ad...

Now, on that list, there is also https://github.com/facebookexperimental/MIRAI that, alongside the crate https://crates.io/crates/contracts (with the mirai_assertion feature enabled) enables writing code like this

    #[ensures(person_name.is_some() -> ret.contains(person_name.unwrap()))]
    fn geeting(person_name: Option) -> String {
        let mut s = String::from("Hello");
        if let Some(name) = person_name {
            s.push(' ');
            s.push_str(name);
        }
        s.push('!');
        s
    }
And have it checked at compile time that the assertion holds! Which is a bit like Liquid Haskell in capability: https://ucsd-progsys.github.io/liquidhaskell/

... and now I just noticed that prusti has a crate prusti_contracts that can do the same thing!! https://github.com/viperproject/prusti-dev/blob/master/prust...

Now I'm wondering which tool is more capable (as I understand, they leverage a SMT solver like Z3 to discharge the proof obligations, right?)

Re: Prusti: Static Analyzer for Rust

#79

Post by nextaccountic »

Aurel300 wrote: post #49
hn92726819 wrote: post #42

Earlier quoted context omitted.

If I'm reading your comment correctly, then this is so much cooler than I thought :D. Closest thing to this would be https://docs.rs/no-panic/latest/no_panic/ I believe, and the error message leaves much to be desired. I will definitely be trying this out, but one last question: std can panic when doing tons of things (slice indexing, str.split_at, etc). Can this be used to make never-panicing programs?

The short answer is: it could be used for that. But there's a couple of things to say: - Prusti is doing _modular_ verification: every method is verified in isolation, and all calls in that method's code only use the contracts declared on the call targets. This is good for scalability and caching and it means that a method's signature + contract is the entire API (you don't depend on its internals). - Methods without…

> - However, we are in the process of creating a library of specifications for stdlib methods. We use a large-scale analysis framework (rust-corpus/qrates) to evaluate which methods are used most often. We try to specify such methods first to cover real-world Rust code usages.

I asked somewhere else about the difference of prusti and mirai but, could mirai also make use of this specification?

I see that prusti_contracts and the contracts crate have a different syntax, but many contracts written for one could be translated for other, right? (IOW I don't know how much their semantics differ)

Re: Prusti: Static Analyzer for Rust

#80

Post by Grimburger »

insanitybit wrote: post #36

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…

Any public repo yet? This sounds great.
Post reply on HN