Prusti: Static Analyzer for Rust
github.com
github.com
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.
That’s a really nice demonstrable and practical impact of using effects!
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!
is this open or proprietary? I'd love a link to a repo
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)
}
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.
- Github : https://github.com/insanitybit
- Twitter: https://twitter.com/InsanityBit
impl List {
#[ensures(self.len() == old(self.len()) + 1)]
pub fn push(&mut self, elem: i32) {
// TODO
}
}Another library that implements this, albeit at runtime (and optionally using MIRAI is https://docs.rs/contracts/latest/contracts/
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!
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.
> 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
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/...
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?
- 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 a contract are assumed to have the precondition `true` and postcondition `true` (in other words, such a method can always be called and makes no guarantees at all about what it did to its mutable arguments or result). For methods declared within the current project, this is fine: if they could panic, Prusti would identify this when verifying them and the user would have to declare a precondition. For external methods (whose implementation is not verified), this is potentially unsound.
- 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.
Making the default precondition for external functions "false" (unless specified otherwise) would be sound but would be quite restrictive. One goal of Prusti is also incremental verification: you should be able to start using Prusti for basic checks then gradually introduce more specifications to get stronger and stronger guarantees about the program's behaviour.
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)
In the long term we might investigate a full integration with external verifiers, e.g. to check that the specifications declared on external methods in Rust is justified by their actual implementation, say in C. This is tricky because the specification language/level of abstraction might differ. It might be necessary to prove program refinement, for example.
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...
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
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.
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.
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.
Some of the possible problems are easy to confirm or deny just by looking at one line of code, but others will require much more analysis.
You need a tool/viewer to show the possible problem and what caused the possible problem. Such a tool improves the user experience dealing with static analyzer results.
- https://fbinfer.com/ (<- This one was a breakthrough in static analysis in its time)
- https://github.com/google/error-prone
- https://github.com/facebook/SPARTA
And many others
see tools section in https://learn.microsoft.com/en-us/previous-versions/tn-archi...
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...
On the other hand commercial tools have been more of a mixed blessing but that is probably because every time ive seen them deployed the budget hasnt included sufficient engineering time, training or prof services to cut down huge numbers of false positives.
valgrind is not a static analysis tool. But it is a great tool, especially memcheck.
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.
I think it varies by industry though.
Usually it doesn't matter if devs themselves don't care, because when devops have the management support, they will care to fix that broken build.
- act as a C/C++ compiler for legacy code,
- shine where Rust is weakest: strings-first apps and apps that benefit from classes,
- get us to a world where the best C++ is a frozen C++
Too tall an order?
And what do you mean by Rust being weakest in these categories anyway, and why do you think it is? What are "string-first apps"? And how is not adopting inheritance-based OOP a weakness? I think, many experienced programmers, especially those familiar with ML family of languages and otherwise well-versed in different paradigms, will argue that this particular flavour of OOP is more harmful than helpful.
In other words, the human factors facet of language design. D does very well as a friendly language from a human factors perspective.
A simple example of this is `+` is commonly used to mean both addition and concatenation, leading to confusion with awkward resolutions. D uses `+` for addition, and `~` for concatenation. It's been working great.
We also regularly correct errors in the design of D.
I feel like assuming Java is installed doesn't really fit the audience.
From what I have seen LH focuses on integrating into the type system (it is Liquid as in the 2008 Liquid Types paper). Generally it is possible to rewrite properties attached to a type to contracts, e.g. a non-zero Int input becomes a precondition that says that argument is non-zero. Checking termination with Prusti is also something we are working on.
> 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<&str>) -> String {
let mut s = String::from("Hello");
if let Some(name) = person_name {
s.push(' ');
s.push_str(name);
}
s.push('!');
s
}
... 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?)
Safe Rust is memory safe and data race safe. There are other forms of safety obviously, like overflow safety, numerous forms of confidentiality and security properties, etc.
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.
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).
The remaining 30% still need to be tracked down.
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...
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.
- Prusti does not require you to write any "properties". I just ran it on a piece of code, which has no annotations for Prusti, and it still found a potential integer overflow. Maybe it has some internal annotations for std, but none for my code.