The State of Rust Checkers and My New Contribution: Lockbud

announcements
1

As Rust continues to gain popularity, the need for robust static analysis tools to detect common programming errors and safety issues has become increasingly important. In the Rust ecosystem, there are already several excellent checkers and linters available to help developers write safer and more reliable code.

I collected some of the recent Rust checkers and published it here

I've classified the Rust checkers into four main categories: linters, static checkers, dynamic checkers, and formal verifiers. For each checker, I've included the following information:

  • Links and descriptions (links to code and paper)
  • The intermediate representation (IR) the checker works on (e.g., HIR, MIR)
  • The types of bugs it can detect
  • The underlying technology or approach used
  • The current maintenance status and activity

Additionally, I've noted a few academic papers that propose interesting Rust analysis techniques, even though I haven't been able to locate the publicly available code for those research prototypes.

This comprehensive overview aims to give the Rust community a clear understanding of the available static analysis tools, their capabilities, and the overall state of Rust checker development. By highlighting these details, developers can more easily navigate the ecosystem and choose the right tools for their specific needs.

My New Contribution: Lockbud

In addition to the existing Rust checkers, I'm excited to share a new tool I've developed called "Lockbud". Lockbud is a static analysis tool designed to detect a variety of concurrency and memory safety issues in Rust code, including double-locks, conflicting lock orders, atomicity violations, use-after-free, and more. Lockbud is the research artifact that was developed as part of our recent paper published in the Transactions on Software Engineering (TSE) journal, which I co-authored under the mentorship of Professor Song. This work builds upon our earlier paper presented at the PLDI conference. You can find more information about Lockbud in the GitHub - BurtonQin/lockbud: Statically detect memory, concurrency bugs and possible panic locations for Rust.. Despite being a relatively new tool, Lockbud has already uncovered 96 previously undiscovered bugs across 12 real-world Rust code repositories.

Drawing from my development experience and the insights gained from evaluating these various Rust checkers, I believe there is a strong need for a unified static analysis framework. Such a framework would enable novel detection algorithms to be more seamlessly integrated, further enhancing the overall safety and ease-of-use for the Rust ecosystem.

If you have any other new Rust checker projects, research papers, or suggestions for improving the Rust analysis landscape, please feel free to share them with me. I'm always eager to learn about the latest developments and share them with the community.

7 Likes
2

Ah, so this is academic code... What are the plans to maintain it after the paper is accepted / the conference talk is over / the PhD is done (select whichever is applicable). This is the main issue with academic code in my experience: there is no long term thinking.

3 Likes
3

This is indeed a common issue in academic artifacts. I would like to promote the adoption of the detector within the company where I am employed for an ongoing support. I have created a preliminary to-do list. But I need a well-defined Maintenance Plan for the open-source project, which outlines the time frame and frequency of updates, as well as our commitment to respond to issues and feature requests.

2 Likes
4

I assume you've come across clippy. I understand that it is a linter, but I am curious what more you think a unified static analysis framework brings compared to clippy.

Perhaps it's as simple as a cargo plugin that can be configured to run various static analysis tools for you, with some good sensible defaults.

5

It should be a cargo plugin. Clippy mainly checks HIR while the static analysis framework I mentioned should go further and work on MIR or even LLVM IR. Thus it can check more kinds of bugs than clippy and more precisely.

3 Likes
6

Nice work. I think Flux and RefinedRust could be added to the list; see also Table 1 of the RefinedRust paper:
image
If you intend to maintain the list, you might consider putting it in a repo with a contribution policy. Also, the folks in Zulip #wg-formal-methods would likely be interested in your work if you'd like to share it there.

3 Likes
7

Thanks, I have included RefinedRust and the mentioned verifiers in the list. As for a separate repo, I am working on it. Thanks again for your reply.

8

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.