arXiv subjects

John C. Mitchell

Publications and source records attributed to John C. Mitchell.

12 recordsLinked to original sources

arXiv2025

What Is Your Agent's GPA? A Framework for Evaluating Agent Goal-Plan-Action Alignment

We introduce the Agent GPA (Goal-Plan-Action) framework, driven by the fundamental insight that critical agent failures emerge at the intersections of setting goals, devising plans, and executing actions. We operationalize the framework with a factorized suite of LLM judges designed to measure distinct elements of Goal-Plan-Act alignment. To make this methodology scalable and generalizable across diverse agent architectures and datasets, we use state-of-the-art automated prompt optimization techniques to systematically generate domain-specific evaluation criteria. We validate this approach across three benchmarks: a multi-agent research setting (TRAIL/GAIA), a single coding agent setting (TRAIL/SWE-bench), and a private, enterprise data-agent setting (Snowflake Intelligence). Extensive evaluation on TRAIL/GAIA demonstrates the core validity of the framework, which identifies a broad range of agent failures (95% of human-annotated errors), localizes errors to enable targeted debugging (86% of human-annotated errors), and exhibits strong agreement with human evaluators. Crucially, by applying our automated methodology to both public datasets, we demonstrate that our GPA judges generally achieve the highest error coverage (ranging from 76% to 86%) in comparison to manual prompting approaches. We also leverage an evolutionary coding agent to improve judge consistency by up to 38% through iterative refinement of evaluation rubrics. Overall, Agent GPA provides a rigorous and generalizable paradigm for targeted agent evaluation.

cs.AI↗

arXiv2025

Analyzing and Exploiting Branch Mispredictions in Microcode

We present uSpectre, a new class of transient execution attacks that exploit microcode branch mispredictions to transiently leak sensitive data. We find that many long-known and recently-discovered transient execution attacks, which were previously categorized as Spectre or Meltdown variants, are actually instances of uSpectre on some Intel microarchitectures. Based on our observations, we discover multiple new uSpectre attacks and present a defense against uSpectre vulnerabilities, called uSLH.

cs.CR↗

arXiv2024

ChatCollab: Exploring Collaboration Between Humans and AI Agents in Software Teams

We explore the potential for productive team-based collaboration between humans and Artificial Intelligence (AI) by presenting and conducting initial tests with a general framework that enables multiple human and AI agents to work together as peers. ChatCollab's novel architecture allows agents - human or AI - to join collaborations in any role, autonomously engage in tasks and communication within Slack, and remain agnostic to whether their collaborators are human or AI. Using software engineering as a case study, we find that our AI agents successfully identify their roles and responsibilities, coordinate with other agents, and await requested inputs or deliverables before proceeding. In relation to three prior multi-agent AI systems for software development, we find ChatCollab AI agents produce comparable or better software in an interactive game development task. We also propose an automated method for analyzing collaboration dynamics that effectively identifies behavioral characteristics of agents with distinct roles, allowing us to quantitatively compare collaboration dynamics in a range of experimental conditions. For example, in comparing ChatCollab AI agents, we find that an AI CEO agent generally provides suggestions 2-4 times more often than an AI product manager or AI developer, suggesting agents within ChatCollab can meaningfully adopt differentiated collaborative roles. Our code and data can be found at: https://github.com/ChatCollab.

cs.HC↗

arXiv2023

Serberus: Protecting Cryptographic Code from Spectres at Compile-Time

We present Serberus, the first comprehensive mitigation for hardening constant-time (CT) code against Spectre attacks (involving the PHT, BTB, RSB, STL and/or PSF speculation primitives) on existing hardware. Serberus is based on three insights. First, some hardware control-flow integrity (CFI) protections restrict transient control-flow to the extent that it may be comprehensively considered by software analyses. Second, conformance to the accepted CT code discipline permits two code patterns that are unsafe in the post-Spectre era. Third, once these code patterns are addressed, all Spectre leakage of secrets in CT programs can be attributed to one of four classes of taint primitives--instructions that can transiently assign a secret value to a publicly-typed register. We evaluate Serberus on cryptographic primitives in the OpenSSL, Libsodium, and HACL* libraries. Serberus introduces 21.3% runtime overhead on average, compared to 24.9% for the next closest state-of-the-art software mitigation, which is less secure.

cs.CR↗

arXiv2020

Resources: A Safe Language Abstraction for Money

Smart contracts are programs that implement potentially sophisticated transactions on modern blockchain platforms. In the rapidly evolving blockchain environment, smart contract programming languages must allow users to write expressive programs that manage and transfer assets, yet provide strong protection against sophisticated attacks. Addressing this need, we present flexible and reliable abstractions for programming with digital currency in the Move language [Blackshear et al. 2019]. Move uses novel linear [Girard 1987] resource types with semantics drawing on C++11 [Stroustrup 2013] and Rust [Matsakis and Klock 2014]: when a resource value is assigned to a new memory location, the location previously holding it must be invalidated. In addition, a resource type can only be created or destroyed by procedures inside its declaring module. We present an executable bytecode language with resources and prove that it enjoys resource safety, a conservation property for program values that is analogous to conservation of mass in the physical world.

cs.PL↗

arXiv2020

Model Checking Bitcoin and other Proof-of-Work Consensus Protocols

The Bitcoin Backbone Protocol [GKL15] is an abstraction of the bitcoin proof-of-work consensus protocol. We use a model-checking tool (UPPAALSMC) to examine the concrete security of proof-ofwork consensus by varying protocol parameters and using an adversary that leverages the selfish mining strategy introduced in [GKL15]. We provide insights into modeling proof-of-work protocols and demonstrate tradeoffs between operating parameters. Applying this methodology to protocol design options, we show that the uniform tie-breaking rule from [ES18] decreases the failure rate of the chain quality property, but increases the failure rate of the common prefix property. This tradeoff illustrates how design decisions affect protocol properties, within a range of concrete operating conditions, in a manner that is not evident from prior asymptotic analysis.

cs.CR↗

arXiv2016

Data Representation and Compression Using Linear-Programming Approximations

We propose `Dracula', a new framework for unsupervised feature selection from sequential data such as text. Dracula learns a dictionary of $n$-grams that efficiently compresses a given corpus and recursively compresses its own dictionary; in effect, Dracula is a `deep' extension of Compressive Feature Learning. It requires solving a binary linear program that may be relaxed to a linear program. Both problems exhibit considerable structure, their solution paths are well behaved, and we identify parameters which control the depth and diversity of the dictionary. We also discuss how to derive features from the compressed documents and show that while certain unregularized linear models are invariant to the structure of the compressed dictionary, this structure may be used to regularize learning. Experiments are presented that demonstrate the efficacy of Dracula's features.

cs.LG↗

arXiv2016

Privacy-Preserving Shortest Path Computation

Navigation is one of the most popular cloud computing services. But in virtually all cloud-based navigation systems, the client must reveal her location and destination to the cloud service provider in order to learn the fastest route. In this work, we present a cryptographic protocol for navigation on city streets that provides privacy for both the client's location and the service provider's routing data. Our key ingredient is a novel method for compressing the next-hop routing matrices in networks such as city street maps. Applying our compression method to the map of Los Angeles, for example, we achieve over tenfold reduction in the representation size. In conjunction with other cryptographic techniques, this compressed representation results in an efficient protocol suitable for fully-private real-time navigation on city streets. We demonstrate the practicality of our protocol by benchmarking it on real street map data for major cities such as San Francisco and Washington, D.C.

cs.CR↗

arXiv2015

A Symbolic Logic with Concrete Bounds for Cryptographic Protocols

We present a formal logic for quantitative reasoning about security properties of network protocols. The system allows us to derive concrete security bounds that can be used to choose key lengths and other security parameters. We provide axioms for reasoning about digital signatures and random nonces, with security properties based on the concrete security of signature schemes and pseudorandom number generators (PRG). The formal logic supports first-order reasoning and reasoning about protocol invariants, taking concrete security bounds into account. Proofs constructed in our logic also provide conventional asymptotic security guarantees because of the way that concrete bounds accumulate in proofs. As an illustrative example, we use the formal logic to prove an authentication property with concrete bounds of a signature-based challenge-response protocol.

cs.LO↗

arXiv2015

IFC Inside: Retrofitting Languages with Dynamic Information Flow Control (Extended Version)

Many important security problems in JavaScript, such as browser extension security, untrusted JavaScript libraries and safe integration of mutually distrustful websites (mash-ups), may be effectively addressed using an efficient implementation of information flow control (IFC). Unfortunately existing fine-grained approaches to JavaScript IFC require modifications to the language semantics and its engine, a non-goal for browser applications. In this work, we take the ideas of coarse-grained dynamic IFC and provide the theoretical foundation for a language-based approach that can be applied to any programming language for which external effects can be controlled. We then apply this formalism to server- and client-side JavaScript, show how it generalizes to the C programming language, and connect it to the Haskell LIO system. Our methodology offers design principles for the construction of information flow control systems when isolation can easily be achieved, as well as compositional proofs for optimized concrete implementations of these systems, by relating them to their isolated variants.

cs.PL↗

arXiv2012

Flexible Dynamic Information Flow Control in the Presence of Exceptions

We describe a new, dynamic, floating-label approach to language-based information flow control. A labeled IO monad, LIO, keeps track of a current label and permits restricted access to IO functionality. The current label floats to exceed the labels of all data observed and restricts what can be modified. Unlike other language-based work, LIO also bounds the current label with a current clearance that provides a form of discretionary access control. Computations may encapsulate and pass around the results of computations with different labels. In addition, the LIO monad offers a simple form of labeled mutable references and exception handling. We give precise semantics and prove confidentiality and integrity properties of a call-by-name λ-calculus and provide an implementation in Haskell.

cs.CR↗

arXiv2009

A Learning-Based Approach to Reactive Security

Despite the conventional wisdom that proactive security is superior to reactive security, we show that reactive security can be competitive with proactive security as long as the reactive defender learns from past attacks instead of myopically overreacting to the last attack. Our game-theoretic model follows common practice in the security literature by making worst-case assumptions about the attacker: we grant the attacker complete knowledge of the defender's strategy and do not require the attacker to act rationally. In this model, we bound the competitive ratio between a reactive defense algorithm (which is inspired by online learning theory) and the best fixed proactive defense. Additionally, we show that, unlike proactive defenses, this reactive strategy is robust to a lack of information about the attacker's incentives and knowledge.

cs.CR↗