I did not get very far yet to produce quite meaningful results apart from knowing that we don’t have panics in our on-chain code base (which is something I guess). My next step will be to write conditions around the code base to do more meaningful verification.
If anyone else is also interested in code analysis, would be great if you could share your experience.
Hi @dom. Just to already share our RFP here. Let me know if you know someone who might want to work on this. Or if you want to work on it yourself.
Bhargav, who mainly wrote it, also will reply here. In the meantime, you can take a look at his example here. We are also quite interested in this, and I think it would be super useful for the ecosystem.
Hi @dom
Thanks for sharing the blog, quite interesting.
We at W3F have been working on a feasibility study on Static Analysers for Rust. The objectives are two-fold:
Determine interesting classes of bugs/vulnerabilities which can be detected using static analysis and verification techniques with reasonable soundness guarantees.
Identify robust tools on top of which Substrate-specific static analysis features can be built on.
This is still WIP, but so far our experience has been quite positive with MIRAI (abstract interpreter) and Crux-MIR (symbolic execution engine). Here is my fork of MIRAI tuned for Substrate.
MIRAI throws several warnings related to unsafe math operations, and potential memory-related panics. However, the false positive rate is significant (on a small sample). To reduce False positives, we ideally want to develop a hybrid tool that performs Symbolic execution on the warnings generated by abstract interpretation. This will also give us concrete tests that trigger the warnings and also help in triaging the bug.
Another line of work is to use the Tag and Taint analysis framework of MIRAI. Several susbtrate specific vulnerabilities could be modelled as sink-source dataflow properties, and the custom tags can be defined to track its flow. This RFP provides more information. We have been in touch with developers of MIRAI and they are willing to support specific request on the tool side, if any.
Fully agree with your goals. To me, there are two parts to the verification aspect that are of particular interest:
Absence of common vulnerabilities. That seems very close to what your RFP is looking for. Trail of Bits also just released common vulnerabilities they found in substrate: Substrate - Building Secure Contracts. The out-of-the-box MIRAI actually did not give me false positives on our runtime crates. Will take a look at your fork next.
Hey @dom! I’m curious about what sort of interface you would like for verification.
We’re working on a project to build a Rust verification tool based on verifying MIR. So far, we’ve been thinknig that we plug into property testing framework at Rust level (like what HydraDX is using), so that users can write property tests that are fuzzed at the rust level, then verified using our tools and symbolic execution.
Interface-wise, I was thinking mostly along the lines of something that runs in the rust toolchain (like MIRAIs cargo mirai) and writing the checks in rust itself.
I also work on the project with @ehildenb, I wonder what your thoughts are on an interface with refinement types. There already exists a tool Flux that provides refinement types as annotations to Rust projects.