arXiv subjects

David Sands

Publications and source records attributed to David Sands.

15 recordsLinked to original sources

arXiv2026

The LLMbda Calculus: AI Agents, Conversations, and Information Flow

Large language models are increasingly deployed as agents: they plan, call tools, read untrusted data, and act on the results. This exposes them to prompt injection: data meant only to be read is obeyed as an instruction. The most principled defences replace content inspection with provenance: classifying data by source and keeping trusted and untrusted apart through a separation of duty (the dual-LLM pattern) and information-flow control. Yet the leading systems are hard to fully trust: flow tracking is easy to get wrong, deliberate relaxations are hard to audit, and the dual-LLM pattern is hard-wired into the architecture. We present LLMbda, an untyped call-by-value lambda calculus that makes provenance-based defence both expressible and provably sound, without committing to an architecture. It adds the operational core of agentic systems as first-class constructs: prompt-response conversations that can be forked and cleared, code generation, and dynamic information-flow control in which every value carries a label that every reduction propagates. Isolation becomes a policy a program expresses, and reclassification an explicit, auditable construct. Our central result is a termination-insensitive probabilistic noninterference theorem over the whole calculus, including code-generating agents, with an insulated variant that holds even when the attacker chooses all untrusted inputs. The verified interpreter is itself the harness that calls the model, to our knowledge the first LLM agent harness whose executable is the subject of machine-checked security theorems, so every agent inherits the guarantee. On the AgentDojo banking benchmark, an agent built within LLMbda, enforcement always on, matches the utility of CaMeL, a leading dual-LLM defence, run without its policy checks (which halve its utility), and resists all but two of 1296 attacked runs. Our harness and all proofs are in Lean.

cs.PL↗

arXiv2022

Reconciling Shannon and Scott with a Lattice of Computable Information

This paper proposes a reconciliation of two different theories of information. The first, originally proposed in a lesser-known work by Claude Shannon, describes how the information content of channels can be described qualitatively, but still abstractly, in terms of information elements, i.e. equivalence relations over the data source domain. Shannon showed that these elements form a complete lattice, with the order expressing when one element is more informative than another. In the context of security and information flow this structure has been independently rediscovered several times, and used as a foundation for reasoning about information flow. The second theory of information is Dana Scott's domain theory, a mathematical framework for giving meaning to programs as continuous functions over a particular topology. Scott's partial ordering also represents when one element is more informative than another, but in the sense of computational progress, i.e. when one element is a more defined or evolved version of another. To give a satisfactory account of information flow in programs it is necessary to consider both theories together, to understand what information is conveyed by a program viewed as a channel (\`a la Shannon) but also by the definedness of its encoding (\`a la Scott). We combine these theories by defining the Lattice of Computable Information (LoCI), a lattice of preorders rather than equivalence relations. LoCI retains the rich lattice structure of Shannon's theory, filters out elements that do not make computational sense, and refines the remaining information elements to reflect how Scott's ordering captures the way that information is presented. We show how the new theory facilitates the first general definition of termination-insensitive information flow properties, a weakened form of information flow property commonly targeted by static program analyses.

cs.PL↗

arXiv2018

Monitoring Data Minimisation

Data minimisation is a privacy enhancing principle, stating that personal data collected should be no more than necessary for the specific purpose consented by the user. Checking that a program satisfies the data minimisation principle is not easy, even for the simple case when considering deterministic programs-as-functions. In this paper we prove (im)possibility results concerning runtime monitoring of (non-)minimality for deterministic programs both when the program has one input source (monolithic) and for the more general case when inputs come from independent sources (distributed case). We propose monitoring mechanisms where a monitor observes the inputs and the outputs of a program, to detect violation of data minimisation policies. We show that monitorability of (non) minimality is decidable only for specific cases, and detection of satisfaction of different notions of minimality in undecidable in general. That said, we show that under certain conditions monitorability is decidable and we provide an algorithm and a bound to check such properties in a pre-deployment controlled environment, also being able to compute a minimiser for the given program. Finally, we provide a proof-of-concept implementation for both offline and online monitoring and apply that to some case studies.

cs.LO↗

arXiv2016

Data Minimisation: a Language-Based Approach (Long Version)

Data minimisation is a privacy-enhancing principle considered as one of the pillars of personal data regulations. This principle dictates that personal data collected should be no more than necessary for the specific purpose consented by the user. In this paper we study data minimisation from a programming language perspective. We assume that a given program embodies the purpose of data collection, and define a data minimiser as a pre-processor for the input which reduces the amount of information available to the program without compromising its functionality. In this context we study formal definitions of data minimisation, present different mechanisms and architectures to ensure data minimisation, and provide a procedure to synthesise a correct data minimiser for a given program.

cs.CR↗

arXiv2015

The Anatomy and Facets of Dynamic Policies

Information flow policies are often dynamic; the security concerns of a program will typically change during execution to reflect security-relevant events. A key challenge is how to best specify, and give proper meaning to, such dynamic policies. A large number of approaches exist that tackle that challenge, each yielding some important, but unconnected, insight. In this work we synthesise existing knowledge on dynamic policies, with an aim to establish a common terminology, best practices, and frameworks for reasoning about them. We introduce the concept of facets to illuminate subtleties in the semantics of policies, and closely examine the anatomy of policies and the expressiveness of policy specification mechanisms. We further explore the relation between dynamic policies and the concept of declassification.

cs.CR↗

arXiv2015

Featherweight PINQ

Differentially private mechanisms enjoy a variety of composition properties. Leveraging these, McSherry introduced PINQ (SIGMOD 2009), a system empowering non-experts to construct new differentially private analyses. PINQ is an LINQ-like API which provides automatic privacy guarantees for all programs which use it to mediate sensitive data manipulation. In this work we introduce featherweight PINQ, a formal model capturing the essence of PINQ. We prove that any program interacting with featherweight PINQ's API is differentially private.

cs.PL↗

arXiv2015

Very Static Enforcement of Dynamic Policies

Security policies are naturally dynamic. Reflecting this, there has been a growing interest in studying information-flow properties which change during program execution, including concepts such as declassification, revocation, and role-change. A static verification of a dynamic information flow policy, from a semantic perspective, should only need to concern itself with two things: 1) the dependencies between data in a program, and 2) whether those dependencies are consistent with the intended flow policies as they change over time. In this paper we provide a formal ground for this intuition. We present a straightforward extension to the principal flow-sensitive type system introduced by Hunt and Sands (POPL '06, ESOP '11) to infer both end-to-end dependencies and dependencies at intermediate points in a program. This allows typings to be applied to verification of both static and dynamic policies. Our extension preserves the principal type system's distinguishing feature, that type inference is independent of the policy to be enforced: a single, generic dependency analysis (typing) can be used to verify many different dynamic policies of a given program, thus achieving a clean separation between (1) and (2). We also make contributions to the foundations of dynamic information flow. Arguably, the most compelling semantic definitions for dynamic security conditions in the literature are phrased in the so-called knowledge-based style. We contribute a new definition of knowledge-based termination insensitive security for dynamic policies. We show that the new definition avoids anomalies of previous definitions and enjoys a simple and useful characterisation as a two-run style property.

cs.CR↗

arXiv2014

Type-Directed Compilation for Fault-Tolerant Non-Interference

Environmental noise (e.g.heat, ionized particles, etc.) causes transient faults in hardware, which lead to corruption of stored values. Mission-critical devices require such faults to be mitigated by fault-tolerance --- a combination of techniques that aim at preserving the functional behaviour of a system despite the disruptive effects of transient faults. Fault-tolerance typically has a high deployment cost -- special hardware might be required to implement it -- and provides weak statistical guarantees. It is also based on the assumption that faults are rare. In this paper, we consider scenarios where security, rather than functional correctness, is the main asset to be protected. Our contribution is twofold. Firstly, we develop a theory for expressing confidentiality of data in the presence of transient faults. We show that the natural probabilistic definition of security in the presence of faults can be captured by a possibilistic definition. Furthermore, the possibilistic definition is implied by a known bisimulation-based property, called Strong Security. Secondly, we illustrate the utility of these results for a simple RISC architecture for which only the code memory and program counter are assumed fault-tolerant. We present a type-directed compilation scheme that produces RISC code from a higher-level language for which Strong Security holds --- i.e. well-typed programs compile to RISC code which is secure despite transient faults. In contrast with fault-tolerance solutions, our technique assumes relatively little special hardware, gives formal guarantees, and works in the presence of an active attacker who aggressively targets parts of a system and induces faults precisely.

cs.CR↗

arXiv2013

Reinterpreting Boltzmann's H-theorem in the light of Information Theory

Prompted by the realisation that the statistical entropy of an ideal gas in the micro-canonical ensemble should not fluctuate or change over time, the meaning of the H-theorem is re-interpreted from the perspective of information theory in which entropy is a measure of uncertainty. We propose that the Maxwellian velocity distribution should more properly be regarded as a limiting distribution which is identical with the distribution across particles in the asymptotic limit of large numbers. In smaller systems, the distribution across particles differs from the limiting distribution and fluctuates. Therefore the entropy can be calculated either from the actual distribution across the particles or from the limiting distribution. The former fluctuates with the distribution but the latter does not. However, only the latter represents uncertainty in the sense implied by information theory by accounting for all possible microstates. We also argue that the Maxwellian probability distribution for the velocity of a single particle should be regarded as a limiting distribution. Therefore the entropy of a single particle is well defined, as is the entropy of an N-particle system, regardless of the microstate. We argue that the meaning of the H-theorem is to reveal the underlying distribution in the limit of large numbers. Computer simulations of a hard-sphere fluid are used to demonstrate the ideas.

physics.gen-ph↗

arXiv2012

Gender differences in conceptual understanding of Newtonian mechanics: a UK cross-institution comparison

We present results of a combined study from three UK universities where we investigate the existence and persistence of a performance gender gap in conceptual understanding of Newtonian mechanics. Using the Force Concept Inventory, we find that students at all three universities exhibit a statistically significant gender gap, with males outperforming females. This gap is narrowed but not eliminated after instruction, using a variety of instructional approaches. Furthermore, we find that before instruction the quartile with the lowest performance on the diagnostic instrument comprises a disproportionately high fraction (~50%) of the total female cohort. The majority of these students remain in the lowest-performing quartile post-instruction. Analysis of responses to individual items shows that male students outperform female students on practically all items on the instrument. Comparing the performance of the same group of students on end-of-course examinations, we find no statistically significant gender gaps.

physics.ed-ph↗

arXiv2011

A Semantic Hierarchy for Erasure Policies

We consider the problem of logical data erasure, contrasting with physical erasure in the same way that end-to-end information flow control contrasts with access control. We present a semantic hierarchy for erasure policies, using a possibilistic knowledge-based semantics to define policy satisfaction such that there is an intuitively clear upper bound on what information an erasure policy permits to be retained. Our hierarchy allows a rich class of erasure policies to be expressed, taking account of the power of the attacker, how much information may be retained, and under what conditions it may be retained. While our main aim is to specify erasure policies, the semantic framework allows quite general information-flow policies to be formulated for a variety of semantic notions of secrecy.

cs.CR↗

arXiv2011

Confusion in Thermodynamics

For a long time now, confusion has existed in the minds of many over the meaning of various concepts in thermodynamics. Recently, this point has been brought to people's attention by two articles appearing on the well-known archive (arxiv) web site. The content of these two pieces serves to illustrate many of the problems and has occasioned the construction of this answer to at least some of them. The position of the axiom proposed by Carathéodory is central in this matter and here its position is clarified and secured within the framework of thermodynamics. In particular, its relation to the First Law is examined and justified.

physics.gen-ph↗

arXiv2009

Specification and Verification of Side Channel Declassification

Side channel attacks have emerged as a serious threat to the security of both networked and embedded systems -- in particular through the implementations of cryptographic operations. Side channels can be difficult to model formally, but with careful coding and program transformation techniques it may be possible to verify security in the presence of specific side-channel attacks. But what if a program intentionally makes a tradeoff between security and efficiency and leaks some information through a side channel? In this paper we study such tradeoffs using ideas from recent research on declassification. We present a semantic model of security for programs which allow for declassification through side channels, and show how side-channel declassification can be verified using off-the-shelf software model checking tools. Finally, to make it simpler for verifiers to check that a program conforms to a particular side-channel declassification policy we introduce a further tradeoff between efficiency and verifiability: by writing programs in a particular "manifest form" security becomes considerably easier to verify.

cs.CR↗

arXiv2009

A User Model for Information Erasure

Hunt and Sands (ESOP'08) studied a notion of information erasure for systems which receive secrets intended for limited-time use. Erasure demands that once a secret has fulfilled its purpose the subsequent behaviour of the system should reveal no information about the erased data. In this paper we address a shortcoming in that work: for erasure to be possible the user who provides data must also play his part, but previously that role was only specified informally. Here we provide a formal model of the user and a collection of requirements called erasure friendliness. We prove that an erasure-friendly user can be composed with an erasing system (in the sense of Hunt and Sands) to obtain a combined system which is jointly erasing in an appropriate sense. In doing so we identify stronger requirements on the user than those informally described in the previous work.

cs.CR↗

arXiv2007

Thermodynamic Entropy And The Accessible States of Some Simple Systems

Comparison of the thermodynamic entropy with Boltzmann's principle shows that under conditions of constant volume the total number of arrangements in simple thermodynamic systems with temperature-independent heat capacities is TC/k. A physical interpretation of this function is given for three such systems; an ideal monatomic gas, an ideal gas of diatomic molecules with rotational motion, and a solid in the Dulong-Petit limit of high temperature. T1/2 emerges as a natural measure of the number of accessible states for a single particle in one dimension. Extension to N particles in three dimensions leads to TC/k as the total number of possible arrangements or microstates. The different microstates of the system are thus shown a posteriori to be equally probable, with probability T-C/k, which implies that for the purposes of counting states the particles of the gas are distinguishable. The most probable energy state of the system is determined by the degeneracy of the microstates.

physics.gen-ph↗