Jacob Ginesin

Jacob Ginesin, Max von Hippel, Cristina Nita-Rotaru

Distributed protocols are the linchpin of the modern internet, underpinning every internet service. This has in turn motivated a massive body of research ensuring the security, reliability, and performance of distributed protocols. In these works, a wide-ranging assumption is that distributed protocols operate over faulty or attacker-controlled channels, where messages can be arbitrarily inserted, dropped, replayed, or reordered. Formal verification work targeting distributed protocols typically defines its own notion of faulty or malicious channels, then constructively proves their protocol is correct with respect to it. In this work we take a fundamentally different approach: we develop a rigorous methodology for automatically conducting channel fault analysis on distributed protocols, and we introduce Tofu, a generalizable tool that implements our methodology. Tofu provides sound, complete analysis, synthesizing channel fault-based attack traces on arbitrary linear temporal logic (LTL) protocol specifications or proving the absence of such through an exhaustive state-space search. We demonstrate the applicability of Tofu by employing it to study TCP.

Jacob Ginesin

Git commit signing is widely entrusted to serve as evidence that a commit hash uniquely and immutably identifies a specific piece of signed content. We show this invariant does not hold. Given any signed commit, an attacker without access to the signing key, and without breaking SHA2 can produce a second, distinct commit with an identical tree, identical metadata, a valid signature, and a ``Verified'' badge from a Git Forge such as Github, differing only in its commit hash. The modified commit cascades to modify the values of all the subsequent, dependent commit hashes, hence we introduce the terminology ``hash chain malleability'' to describe this phenomenon. The malleability in signed Git hashes is feasible due to the inherent malleability present in many of the data representations that make up a commit. In this paper we show three such malleation routes: (i) algebraic inversion s -> n-s for ECDSA; (ii) structural insertion of an unhashed OpenPGP subpacket (RFC4880 5.2.3) for RSA and EdDSA; and (iii) non-canonical DER length re-encoding (X.690 10.1) inside the CMS envelope for S/MIME. Algebraic inversion for ECDSA signatures and subpacket insertion were found to pass local verification (git verify-commit), and all three methods yield a persistent, independent ``Verified'' record on Github. We discuss the consequences of Git hash chain malleation for hash-based commit blocking, dependency pinning (Nixpkgs, Go modules, Github Actions), and reproducible-build systems that treat the commit hash as a content-addressable primary key, and we provide proof-of-concept tooling that automates all three routes.

Georgios Syros, Anshuman Suri, Jacob Ginesin et al.

Large Language Model (LLM)-based agents increasingly interact, collaborate, and delegate tasks to one another autonomously with minimal human interaction. Industry guidelines for agentic system governance emphasize the need for users to maintain comprehensive control over their agents, mitigating potential damage from malicious agents. Several proposed agentic system designs address agent identity, authorization, and delegation, but remain purely theoretical, without concrete implementation and evaluation. Most importantly, they do not provide user-controlled agent management. To address this gap, we propose SAGA, a scalable Security Architecture for Governing Agentic systems, that offers user oversight over their agents' lifecycle. In our design, users register their agents with a central entity, the Provider, that maintains agent contact information, user-defined access control policies, and helps agents enforce these policies on inter-agent communication. We introduce a cryptographic mechanism for deriving access control tokens, that offers fine-grained control over an agent's interaction with other agents, providing formal security guarantees. We evaluate SAGA on several agentic tasks, using agents in different geolocations, and multiple on-device and cloud LLMs, demonstrating minimal performance overhead with no impact on underlying task utility in a wide range of conditions. Our architecture enables secure and trustworthy deployment of autonomous agents, accelerating the responsible adoption of this technology in sensitive environments.