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

TL;DR

Cargo Sherlock is a formal SMT-based tool for quantifying and verifying trust in third-party Rust software dependencies, incorporating both technical and human trust factors to identify supply chain risks.

Contribution

It introduces a formal trust cost framework for software dependencies using SMT, integrating human factors and metadata, and implements it in a practical tool for Rust crates.

Findings

Successfully identifies synthetic supply chain attacks

Detects real-world typosquatting and poorly maintained crates

Scales efficiently to large dependency graphs

Abstract

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.