61–70 of 93 posts
Why would you need a static analyzer for a language that promotes itself as safe out of the box.
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.
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.
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 w…
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.
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.
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…
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 fro…
Out of curiosity, does anyone know how this compares to something like Liquid Haskell? Is one more or less powerful than the other?
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.
I feel like assuming Java is installed doesn't really fit the audience.
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.
Earlier quoted context omitted.
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.
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++.
Earlier quoted context omitted.
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 fro…
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?
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.
Earlier quoted context omitted.
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