Rudra
rust-verification-tools
Our great sponsors
Rudra | rust-verification-tools | |
---|---|---|
11 | 2 | |
1,297 | 241 | |
2.4% | - | |
5.5 | 3.1 | |
about 2 months ago | about 2 years ago | |
Rust | Rust | |
Apache License 2.0 | Apache License 2.0 |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
Rudra
- Rudra – static analyzer to detect common undefined behaviors in Rust programs
- Rudra: Finding Memory Safety Bugs in Rust at the Ecosystem Scale [pdf]
-
Does Rust not need extra linting and sanitizing tools like C++?
If you’re writing unsafe Rust, you might consider cargo miri and Rudra as additional static analyzers which can find bugs rustc won’t
-
Open Rust-related systems research problems suitable for PhD?
In my opinion, much of Rust-specific PhD research likely to be publishable and/or high impact either falls into verification (e.g Prusti, Cruesot) or bug-finding (e.g. Rudra, SyRust). Ralf Jung and his collaborators have done exceptional work in the verification space.
-
Introducing Fortify: A simple and convenient way to bundle owned data with a borrowing type
Perhaps Rudra as well.
- Magma, a project I hope will make provably correct software possible for everyone
-
Is There Anyway To Analyze Unsafe Rust Code For Vulnerabilities?
Haven't used it myself, but I remembered a tool called Rudra was recently posted about in the sub
-
Scylla – Real-Time Big Data Database
Not sure proves your point, but maybe doesn't disprove your point strongly enough. I am not qualified to argue from experience about how Rust is ideally suited in the ways you think it is not. But from everything I have seen, it can do a whole lot of what C++ is also good at. Rust safety is not all or nothing and a codebase could definitely prioritize ergonomics over correctness.
Two things that I saw in the last couple weeks that might start to sway you.
https://github.com/sslab-gatech/Rudra#readme
GhostCell: Separating Permissions from Data in Rust
- Rudra, Rust Memory Safety and Undefined Behavior Detection
- Rudra: Rust Memory Safety and Undefined Behavior Detection
rust-verification-tools
-
AdaCore and Ferrous Systems Joining Forces to Support Rust
I hope someone also picks up the work started in https://project-oak.github.io/rust-verification-tools/ - the idea of having a `cargo verify` tool that supports different backends is great for bridging the academic PoCs with something that an average programmer can integrate into the dev workflow.
- Magma, a project I hope will make provably correct software possible for everyone
What are some alternatives?
magmide - A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
misra-rust - An investigation into what adhering to each MISRA-C rule looks like in Rust. The intention is to decipher how much we "get for free" from the Rust compiler.
prusti-dev - A static verifier for Rust, based on the Viper verification infrastructure.
klee - KLEE Symbolic Execution Engine
project-safe-transmute - Project group working on the "safe transmute" feature
electrolysis - Simple verification of Rust programs via functional purification in Lean 2(!)
line-combination-proofs
rust - Rust for the xtensa architecture. Built in targets for the ESP32 and ESP8266
tectonic - A modernized, complete, self-contained TeX/LaTeX engine, powered by XeTeX and TeXLive.
advisory-db - Security advisory database for Rust crates published through crates.io