[HN Gopher] Prusti: Static Analyzer for Rust
___________________________________________________________________
Prusti: Static Analyzer for Rust
Author : aviramha
Score : 226 points
Date : 2022-10-13 13:55 UTC (9 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| piterdevries wrote:
| Why would you need a static analyzer for a language that promotes
| itself as safe out of the box.
| IshKebab wrote:
| 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.
| jerf wrote:
| 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.
| a_humean wrote:
| 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.
| umanwizard wrote:
| Rust claims to make a particular class of bugs more difficult
| to write. It doesn't claim to magically eliminate all of them.
| the-lazy-guy wrote:
| 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.
| kibwen wrote:
| 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.
| cesarb wrote:
| > 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).
| iudqnolq wrote:
| But Rust is still memory safe because unsafe code
| "morally" is unsound if it assumes something like that
| can't happen.
| naasking wrote:
| > 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.
| pjmlp wrote:
| 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.
| Arch-TK wrote:
| I wonder where you got those numbers from.
| davidatbu wrote:
| Almost every study of security vulnerabilities concludes
| that roughly 70% of them are caused by memory unsafety.
| dcsommer wrote:
| https://alexgaynor.net/2019/aug/12/introduction-to-memory-
| un...
| Vecr wrote:
| A report about Windows written by Microsoft, I think.
| mynameisash wrote:
| 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...
| IshKebab wrote:
| 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++.
| pjmlp wrote:
| Even formal methods and verification have bugs.
| za3faran wrote:
| 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.
| heywire wrote:
| 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.
| johnny-lee wrote:
| 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.
| solomatov wrote:
| 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
| johnny-lee wrote:
| 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...
| boulos wrote:
| 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
| Agingcoder wrote:
| 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'.
| ainar-g wrote:
| 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.
| smaddox wrote:
| Could you comment on the others you use? I would like to
| start using a lot more static analysis at $job.
| ainar-g wrote:
| Luckily for you, it's all open-source, heh.
|
| https://github.com/AdguardTeam/AdGuardDNS/blob/master/scrip
| t...
|
| https://github.com/AdguardTeam/AdGuardDNS/blob/master/scrip
| t...
|
| There's some mess in there, but if you only need a list of
| analysers and examples of usage, these should be enough.
| haskellandchill wrote:
| 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.
| nerdponx wrote:
| 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).
| pm215 wrote:
| 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...
| IshKebab wrote:
| I can't even convince my co-workers to use Typescript. :-/
|
| I think it varies by industry though.
| pjmlp wrote:
| 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.
| aviramha wrote:
| 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..
| drwoland wrote:
| 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.
| wyldfire wrote:
| > 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.
| Ericson2314 wrote:
| 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).
| Klasiaster wrote:
| 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.
| Aurel300 wrote:
| 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.
| epilys wrote:
| 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.
| nine_k wrote:
| 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.
| zozbot234 wrote:
| 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.
| WalterBright wrote:
| Looks like I need to fix my binary search code!
| haskellandchill wrote:
| 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.
| nerdponx wrote:
| 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!
| hn92726819 wrote:
| 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
| Aurel300 wrote:
| 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.
| hn92726819 wrote:
| 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?
| Aurel300 wrote:
| 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.
| epilys wrote:
| 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?
| Aurel300 wrote:
| 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.
| wongarsu wrote:
| 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/...
| hn92726819 wrote:
| Okay two separate checks, I don't know why my mind couldn't
| come up with that wording.
| kibwen wrote:
| 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...
| hn92726819 wrote:
| > 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...
| Ericson2314 wrote:
| 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.
| hn92726819 wrote:
| 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
| wongarsu wrote:
| 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 }
| }
| turboponyy wrote:
| Can't wait for dependently typed type systems
| Yoric wrote:
| 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.
| dochtman wrote:
| 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.
| Aurel300 wrote:
| 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.
| insanitybit wrote:
| 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.
| littlestymaar wrote:
| > 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!
| insanitybit wrote:
| 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.
| jahewson wrote:
| > compiles to a seccomp + apparmor profile
|
| That's a really nice demonstrable and practical impact of using
| effects!
| fire wrote:
| > 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
| insanitybit wrote:
| 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.
| fire wrote:
| what's your twitter/gh? Could you add them to your hn
| profile?
| littlestymaar wrote:
| 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
| insanitybit wrote:
| Thanks, yes. I'll add those to my profile.
| fire wrote:
| Nice, followed you on both
| temp123789246 wrote:
| Out of curiosity, does anyone know how this compares to something
| like Liquid Haskell? Is one more or less powerful than the other?
| Aurel300 wrote:
| 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.
___________________________________________________________________
(page generated 2022-10-13 23:00 UTC)