I've fully ported rudra with charon-rudra, all testcases are supported

[zjp-CN]

Forked Rudra repo: os-checker/Charon-Rudra

Disclaimer: I'm not related to charon or Aeneas project. I'm actually the author of os-checker which is a colloction of tool around Rust code analysis¹, helping people focus on the analyses results and information of their Rust code rather than set up analysis tools own their own.

Charon is a kind of data source for static analysis of Rust code. Refer to its paper Charon: An Analysis Framework for Rust for more info.

In my view, charon separates the data from analyses

• charon does the rustc hooking, CLI arguments parsing and data generation work by itself
• analysis tools can just exploit the data (JSON files if you're curious) to analyze Rust code

In charon-rudra

• Rust code is analyzed through ullbc without talking to rustc
• UnsafeWorkflow analysis is done by charon/aeneas people (background)
• UnsafeDrop analysis and SendSyncVariance are implemented by myself (I took some notes, sorry in Chinese)

I think it'd be good to post the information here, because I saw Rudra is open to maintainance by others.

Footnotes

1. "os" in the name is from the background: os-checker aims to apply to any Rust project. ↩

[Qwaz]

Thanks for sharing. It's really exciting to meet people who share similar research interests.

I'm happy to mention the maintained forks in README.

Do you know how Charon-Rudra performs on Rudra-PoC dataset (testing script)? The current version on the main branch is unfortunately broken (#56), and how the forked version performs on the paper's benchmark would be valuable to people who want to compare their works with Rudra.

[zjp-CN]

Awesome!

I'll check out Rudra-PoC, and try to run Charon-Rudra testsuite to find the difference and improve Charon-Rudra.

Stay tuned.