Cargo Sherlock: An SMT-Based Checker for Software Trust Costs

Hassnain, Muhammad; Basu, Anirudh; Ng, Ethan; Stanford, Caleb; Hassnain, Muhammad; Stanford, Caleb

doi:10.1145/3793656.3793687

mhassnain@ucdavis.edu

I am a third-year Ph.D. student in Computer Science at the University of California, Davis, where I am fortunate to be advised by Dr. Caleb Stanford. Before joining UC Davis, I was at LUMS (BS ‘23). My research focuses broadly on the intersection of security and program analysis. I am currently working on making Rust more secure!

I also run the Computer System Research Club at UC Davis. Every week, we invite faculty, students, or guests to present interesting Computer Systems research. I also developed and maintain the CratesReport website, containing Rust crates and program analysis tool outputs and other relevant security information about them. I also maintain CratesDiff, a website that allows users to compare two versions of a Rust crate and see the differences. It also supports commenting on the differences, which can be useful for code review and collaboration. If you are interested in either presenting or want to contribute to any of the projects, please reach out to me via email .

This website is a collection of my thoughts, research, and other things I find interesting. I am always looking for new opportunities to collaborate, so feel free to reach out if you have any questions or just want to chat.

For encrypted mail, download my GPG public key.

Selected Publications

Cargo Sherlock: An SMT-Based Checker for Software Trust Costs

Muhammad Hassnain, Anirudh Basu, Ethan Ng, and Caleb Stanford

In Proceedings of the IEEE/ACM 14th International Conference on Formal Methods in Software Engineering, Rio de Janeiro, Brazil, 2026

Abs DOI arXiv PDF Code Poster Slides

Supply chain attacks threaten open-source software ecosystems. This paper proposes a formal framework for quantifying trust in third-party software dependencies that is both formally checkable - formalized in satisfiability modulo theories (SMT) - while at the same time incorporating human factors, like the number of downloads, authors, and other metadata that are commonly used to identify trustworthy software in practice. We use data from both software analysis tools and metadata to build a first-order relational model of software dependencies; to obtain an overall "trust cost" combining these factors, we propose a formalization based on the minimum trust problem which asks for the minimum cost of a set of assumptions which can be used to prove that the code is safe. We implement these ideas in Cargo Sherlock, targeted for Rust libraries (crates), incorporating a list of candidate assumptions motivated by quantifiable trust metrics identified in prior work. Our evaluation shows that Cargo Sherlock can be used to identify synthetically generated supply chain attacks and known incidents involving typosquatted and poorly AI-maintained crates, and that its performance scales to Rust crates with many dependencies.
Counterexamples in Safe Rust

Muhammad Hassnain, and Caleb Stanford

In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering Workshops, Sacramento, CA, USA, 2024

Abs DOI PDF Code Slides

The Rust programming language is a prominent candidate for a C and C++ replacement in the memory-safe era. However, Rust’s safety guarantees do not in general extend to arbitrary third-party code. The main purpose of this short paper is to point out that this is true even entirely within safe Rust - which we illustrate through a series of counterexamples. To complement our examples, we present initial experimental results to investigate: do existing program analysis and program verification tools detect or mitigate these risks? Are these attack patterns realizable via input to publicly exposed functions in real-world Rust libraries? And to what extent do existing supply chain attacks in Rust leverage similar attacks? All of our examples and associated data are available as an open source repository on GitHub. We hope this paper will inspire future work on rethinking safety in Rust - especially, to go beyond the safe/unsafe distinction and harden Rust against a stronger threat model of attacks that can be used in the wild.