Publications

2026

1. 

   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.

2025

1. 

   Open-Source LLMs for Technical Q&A: Lessons from StackExchange

   Zeerak Babar, Nafiz Imtiaz Khan, Muhammad Hassnain, and Vladimir Filkov

   In SEET—Software Engineering for Emerging Technologies, 2025

   Abs DOI PDF Code Slides

   In the rapidly evolving domain of software engineering (SE), Large Language Models (LLMs) are increasingly leveraged to automate developer support. Open source LLMs have grown competitive with proprietary models such as GPT-4 and Claude-3, without the associated financial and accessibility constraints. This study investigates whether state of the art open source LLMs including Solar-10.7B, CodeLlama-7B, Mistral-7B, Qwen2-7B, StarCoder2-7B, and LLaMA3-8B can generate responses to technical queries that align with those crafted by human experts. Leveraging retrieval augmented generation (RAG) and targeted fine tuning, we evaluate these models across critical performance dimensions, such as semantic alignment and contextual fluency. Our results show that Solar-10.7B, particularly when paired with RAG and fine tuning, most closely replicates expert level responses, offering a scalable and cost effective alternative to commercial models. This vision paper highlights the potential of open-source LLMs to enable robust and accessible AI-powered developer assistance in software engineering.

2024

1. 

   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.