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.
> 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!
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.
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.
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.
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
}
}
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.
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
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.
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
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?
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.
> - 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)
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.
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.
> 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.
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
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.
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.
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.
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:
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...
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.
> 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.
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.
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.
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).
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.
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.
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.
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.
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.
> 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!
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.
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.
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).
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.
I would say at least half of the remaining 30% are eliminated by Rust's stronger type system and borrow checker too. When I'm writing Rust it feels like I write around 10x fewer bugs than in C++.
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."
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.
- 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.
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.