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

51–60 of 93 posts

Re: Prusti: Static Analyzer for Rust

#51

Post by Aurel300 »

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.

Re: Prusti: Static Analyzer for Rust

#52

Post by insanitybit »

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

> my effects system compiles to a seccomp + apparmor profile so that your rust program is sandboxed at runtime based on info at compile time. is this open or proprietary? I'd love a link to a repo

I'll see if I can open source it this weekend. I'm not trying to be the "like and subscribe for updates" but if you want to see it when it's open source I'd suggest following me on Twitter (or Github? Does Github have a follow thing?) cause I won't remember to reply on HN.

Here's a little snippet:

    #[effect::declare(
      args=(inner_tmp as I)
      returns=("/tmp/" + I)
    )]
    fn tmp_dir(inner_tmp: Path) -> Path {
      Path::from("tmp/").join(inner_tmp)
    }
So it can reason about that Path's constraints. When that Path gets used by, say, "File::create(path)", it gets turned into a rule and added to an apparmor policy.

Apparmor doesn't support a "hey I'm a process, please sandbox me" so I have to write a privileged daemon that manages that bit.

I also have a way to apply effects to functions you don't own, mutating functions, functions that branch, etc. None of that is implemented yet, just designed.

Re: Prusti: Static Analyzer for Rust

#53

Post by fire »

insanitybit wrote: post #52
fire wrote: post #47

Earlier quoted context omitted.

> my effects system compiles to a seccomp + apparmor profile so that your rust program is sandboxed at runtime based on info at compile time. is this open or proprietary? I'd love a link to a repo

I'll see if I can open source it this weekend. I'm not trying to be the "like and subscribe for updates" but if you want to see it when it's open source I'd suggest following me on Twitter (or Github? Does Github have a follow thing?) cause I won't remember to reply on HN. Here's a little snippet: #[effect::declare( args=(inner_tmp as I) returns=("/tmp/" + I) )] fn tmp_dir(inner_tmp: Path) -> Path { Path::from("tmp/"…

what's your twitter/gh? Could you add them to your hn profile?

Re: Prusti: Static Analyzer for Rust

#54

Post by cesarb »

kibwen wrote: post #30
the-lazy-guy wrote: post #10

Earlier quoted context omitted.

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.

> so an overflowing index variable panics anyway.

Unless it overflows all the way to a valid index. Which might lead to unexpected results if the code does not expect to be using a smaller index (for instance, a code trying to access index i+2 might not be expecting it to suddenly access indexes 0 or 1).

Re: Prusti: Static Analyzer for Rust

#55

Post by littlestymaar »

fire wrote: post #53
insanitybit wrote: post #52

Earlier quoted context omitted.

I'll see if I can open source it this weekend. I'm not trying to be the "like and subscribe for updates" but if you want to see it when it's open source I'd suggest following me on Twitter (or Github? Does Github have a follow thing?) cause I won't remember to reply on HN. Here's a little snippet: #[effect::declare( args=(inner_tmp as I) returns=("/tmp/" + I) )] fn tmp_dir(inner_tmp: Path) -> Path { Path::from("tmp/"…

what's your twitter/gh? Could you add them to your hn profile?

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

Re: Prusti: Static Analyzer for Rust

#56

Post by littlestymaar »

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 be available at compile time!

Re: Prusti: Static Analyzer for Rust

#57

Post by iudqnolq »

cesarb wrote: post #54
kibwen wrote: post #30

Earlier quoted context omitted.

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.

> so an overflowing index variable panics anyway. Unless it overflows all the way to a valid index. Which might lead to unexpected results if the code does not expect to be using a smaller index (for instance, a code trying to access index i+2 might not be expecting it to suddenly access indexes 0 or 1).

But Rust is still memory safe because unsafe code "morally" is unsound if it assumes something like that can't happen.

Re: Prusti: Static Analyzer for Rust

#58

Post by ainar-g »

smaddox wrote: post #48
ainar-g wrote: post #25

Earlier quoted context omitted.

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.

Could you comment on the others you use? I would like to start using a lot more static analysis at $job.

Luckily for you, it's all open-source, heh.

https://github.com/AdguardTeam/AdGuardDNS/blob/master/script...

https://github.com/AdguardTeam/AdGuardDNS/blob/master/script...

There's some mess in there, but if you only need a list of analysers and examples of usage, these should be enough.

Re: Prusti: Static Analyzer for Rust

#59

Post by johnny-lee »

solomatov wrote: post #4
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.

Big tech uses static analyzers a lot. See for example, these projects: - https://fbinfer.com/ ( - https://github.com/google/error-prone - https://github.com/facebook/SPARTA And many others

Microsoft bought and adapted PREfix and created a simpler, faster version called PREfast (and the Visual Studio -analyzer switch for C/C++/C# code).

see tools section in https://learn.microsoft.com/en-us/previous-versions/tn-archi...

Re: Prusti: Static Analyzer for Rust

#60

Post by IshKebab »

piterdevries wrote: post #8

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

This is a fair question really. Calling it a static analyser is misleading and seems to be editorialised. It's not like static analysers in C++.

It's actually a formal verification tool. They call it a "static verifier" not a "static analyser".

Most static analysis tools seek to find potential problems in your code - generally common mistakes - but they aren't proving anything usually. They have false positives and negatives. Formal verification requires you to write properties about your code and then it proves it.

Post reply on HN