Prusti: Static Analyzer for Rust(github.com)
github.com
Prusti: Static Analyzer for Rust
https://github.com/viperproject/prusti-dev
92 comments
> compiles to a seccomp + apparmor profile
That’s a really nice demonstrable and practical impact of using effects!
That’s a really nice demonstrable and practical impact of using effects!
> 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!
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!
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.
> 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
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:
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.
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.
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
- Github : https://github.com/insanitybit
- Twitter: https://twitter.com/InsanityBit
Can it compile to systemd service sandboxing directives? Like described here https://www.ctrl.blog/entry/systemd-service-hardening.html
Any public repo yet? This sounds great.
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.
No need to wait, you can pick Idris today, but it won't be a productive experience versus mainstream development tooling.
This really reminds me of design by contract, which I find absolutely fascinating.
Another library that implements this, albeit at runtime (and optionally using MIRAI is https://docs.rs/contracts/latest/contracts/
Another library that implements this, albeit at runtime (and optionally using MIRAI is https://docs.rs/contracts/latest/contracts/
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!
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!
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.
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.
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.
Yeah it is sidestepping as you say! The distinction is that if you don't sidestep by dereferencing raw pointers, the borrow check still works. Observe that you can cast as raw pointers in safe rust. What unsafe {} changes is that you can dereference them. The borrow checker still works for regularly borrowed values (&var and &mut var etc). This is probably obvious for Rust users, but I find some people take the "turn the borrow checker off" literally by assuming they won't get lifetime errors if the put an unsafe { } around their code.
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
> 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 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/...
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/...
Okay two separate checks, I don't know why my mind couldn't come up with that wording.
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.
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?
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 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.
- 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.
> - 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)
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)
Thanks for your interesting work! I wanted to ask, how are FFI boundaries handled? Are they ignored or is it an error to call FFI functions?
Currently they are not handled. But (you guessed it) we also have a project working on this: attaching trusted specifications to external methods.
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.
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.
Sounds really exciting! Mir interpreter has the same limitation. Have you examined incorporating mir in your analysis?
Our verification is based on symbolic execution, miri is an interpreter (concrete execution). So (at least in theory), our approach is more general. We have considered miri in relation to counterexamples: when Prusti emits an assertion failure and gives an example set of values that would lead to such a failure, we could use miri to make sure the counterexample is not spurious (which could happen with certain loop invariants IIRC). However, we have not implemented anything concrete yet.
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...
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...
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
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
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.
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.
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.
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.
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.
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.
That's what scares a lot of people when they run a static analyzer on code for the first time - all the possible problems.
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.
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.
Big tech uses static analyzers a lot. See for example, these projects:
- 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
- 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
Many of Google's general checks in clang-tidy should be directly available, too. For example, the absl checks seem to be on the list of clang-tidy checks:
https://clang.llvm.org/extra/clang-tidy/checks/list.html
https://clang.llvm.org/extra/clang-tidy/checks/list.html
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...
see tools section in https://learn.microsoft.com/en-us/previous-versions/tn-archi...
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...
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...
When I worked on a big c++ codebase I found them essential for both ci/cd systems and actively debugging an issue. The valgrind suite of tools like cachegrind are very useful for both troubleshooting as well as classic static analysis and I heartily recommend investing some time in learning valgrind if you're writing c/c++ code for a platform valgrind runs on.
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.
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.
> The valgrind suite of tools like cachegrind are very useful for both troubleshooting as well as classic static analysis and I heartily recommend investing some time in learning valgrind
valgrind is not a static analysis tool. But it is a great tool, especially memcheck.
valgrind is not a static analysis tool. But it is a great tool, especially memcheck.
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'.
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.
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 can't even convince my co-workers to use Typescript. :-/
I think it varies by industry though.
I think it varies by industry though.
Static analyzers are free CR in most cases. I highly recommend using it, and do know that in some companies people are unaware of those unfortunately..
We have some critical systems code in C that I'm going to try to run static analysis on for our Hack Week. There are probably 100 engineers at my company and not much interest in anything beyond Google SRE and language specific release updates. We use Bash, Php, Python, Ruby, Node, C, Go, and Rust.
In the typical enterprise projects I work on they are quite typical, usually we tend to use stuff like SonarQube and it breaks the build for specific errors.
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.
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.
A lot of Python teams use a linter that can catch errors like "variable used before defined" as well as matters of code style, and increasingly a static type checker in addition to that (which also does its own set of such checks).
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).
This looks good, I'm going to have to try out their work for Go, Gobra, since that's what I'm mostly writing these days.
Looks like I need to fix my binary search code!
[off-topic] While you're at it, how about integrating D with cargo? D could:
- 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?
- 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?
Sadly, D has its own set of problems and design flaws. It's better than C++ in many ways, but still far from Rust in terms of solid foundation in computer science and language design. Frankly, I see no point in integrating it with Rust.
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.
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.
I admit I do not come from an academic computer science background. What I do bring to programming language design, however, is decades of experience in programming, compilers, and being on the front lines doing tech support on them.
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.
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'm not really qualified to judge what is the right feature set for a build system like dub or cargo.
Was a bit disappointed to discover that the advertised Prusti Assistant VS Code assistant sort of silently sits there waiting ("Checking requirements...") if you don't have Java installed.
I feel like assuming Java is installed doesn't really fit the audience.
I feel like assuming Java is installed doesn't really fit the audience.
We are working on improving the error reporting for the IDE extension. Regardless of the audience, Prusti is based on the Viper verification framework which is mainly implemented in Scala.
Out of curiosity, does anyone know how this compares to something like Liquid Haskell?
Is one more or less powerful than the other?
The two tools address similar problems. The kinds of properties you can prove (automatically) should also be similar, because both Prusti and Liquid Haskell ultimately use an SMT solver to check if assertions hold.
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.
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.
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
... 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?)
> 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?)
Why would you need a static analyzer for a language that promotes itself as safe out of the box.
> safe out of the box
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.
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.
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.
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).
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.
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.
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.
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.
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...
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...
Almost every study of security vulnerabilities concludes that roughly 70% of them are caused by memory unsafety.
A report about Windows written by Microsoft, I think.
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.
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.
- I am pretty sure that static verifiers are a subclass of static analysers.
- 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.
- 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.
Rust claims to make a particular class of bugs more difficult to write. It doesn’t claim to magically eliminate all of them.
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.