FormaliSE 2026
Sun 12 - Mon 13 April 2026 Rio de Janeiro, Brazil
co-located with ICSE 2026

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.

Sun 12 Apr

Displayed time zone: Brasilia, Distrito Federal, Brazil change

16:00 - 17:30
Session 3: Formal Modeling, Specification & SemanticsResearch Track / FormaliSE Program at Oceania VIII
16:00
30m
Talk
A Compositional Approach to Mapping BPMN to DCR for Cross-Paradigm Process Modeling
Research Track
Yue Zhou , Hugo A. López Technical University of Denmark
16:30
30m
Talk
Cargo Sherlock: An SMT-Based Checker for Software Trust Costs
Research Track
Muhammad Hassnain University of California, Davis, Anirudh Basu University of California, Davis, Ethan Ng University of California, Davis, Caleb Stanford University of California, Davis
17:00
15m
Talk
Spectabular: Interactive Tabular Requirements Specifications (Research Ideas Paper)
Research Track
Emil Sekerinski McMaster University, Canada
17:15
15m
Talk
Towards Modeling IoT Applications: Specification, Animation and Reasoning in Anemone
Research Track
Manel Barkallah University of Namur, Jean-Marie Jacquet University of Namur