David Aspinall

TCS Journal 2018 Journal Article

Foreword

• Martin Hofmann
• David Aspinall
• Brian Campbell
• Ian Stark
• Perdita Stevens

EAAI Journal 2018 Journal Article

Secure information sharing in social agent interactions using information flow analysis

• Shahriar Bijani
• David Robertson
• David Aspinall

When we wish to coordinate complex, cooperative tasks in open multi-agent systems, where each agent has autonomy and the agents have not been designed to work together, we need a way for the agents themselves to determine the social norms that govern collective behaviour. An effective way to define social norms for agent communication is through the use of interaction models such as those expressed in the Lightweight Coordination Calculus (LCC), a compact executable specification language based on logic programming and pi-calculus. Open multi-agent systems have experienced growing popularity in the multi-agent community and gain importance as large scale distributed systems become more widespread. A major practical limitation to such systems is security, because the very openness of such systems opens the doors to adversaries to exploit vulnerabilities introduced through acceptance of social norms. This paper addresses a key vulnerability of security of open multi-agent systems governed by formal models of social norms (as exemplified by LCC). A fundamental limitation of conventional security mechanisms (e. g. access control and encryption) is the inability to prevent information from being propagated. Focusing on information leakage in choreography systems using LCC, we suggest a framework to detect insecure information flows. A novel security-typed LCC language is proposed to prevent information leakage. Both static (design-time) and dynamic (run-time) security type checking are employed to guarantee no information leakage can occur in annotated agent interaction models. The proposed security type system is discussed and then formally evaluated by proving its properties. Two disadvantages of the pure dynamic analysis are its late detection and its inability to detect implicit information flows. We overcome these issues by performing static analysis. The proposed security type system supports non-interference, i. e. high-security input to the program never affect low-security output. However, it disregards information leaks due to the termination of the program.

TCS Journal 2007 Journal Article

A program logic for resources

• David Aspinall
• Lennart Beringer
• Martin Hofmann
• Hans-Wolfgang Loidl
• Alberto Momigliano

We introduce a reasoning infrastructure for proving statements about resource consumption in a fragment of the Java Virtual Machine Language (JVML). The infrastructure is based on a small hierarchy of program logics, with increasing levels of abstraction: at the top there is a type system for a high-level language that encodes resource consumption. The infrastructure is designed to be used in a proof-carrying code (PCC) scenario, where mobile programs can be equipped with formal evidence that they have predictable resource behaviour. This article focuses on the core logic in our infrastructure, a VDM-style program logic for partial correctness, which can make statements about resource consumption alongside functional behaviour. We establish some important results for this logic, including soundness and completeness with respect to a resource-aware operational semantics for the JVML. We also present a second logic built on top of the core logic, which is used to express termination; it too is shown to be sound and complete. We then outline how high-level language type systems may be connected to these logics. The entire infrastructure has been formalized in Isabelle/HOL, both to enhance the confidence in our meta-theoretical results, and to provide a prototype implementation for PCC. We give examples to show the usefulness of this approach, including proofs of resource bounds on code resulting from compiling high-level functional programs.

IJCAI Conference 2005 Conference Paper

Proof General / Eclipse: A Generic Interface for Interactive Proof

• Daniel Winterstein
• David Aspinall
• Christoph Lüth

TCS Journal 2001 Journal Article

Subtyping dependent types

• David Aspinall
• Adriana Compagnoni

The need for subtyping in type systems with dependent types has been realized for some years. But it is hard to prove that systems combining the two features have fundamental properties such as subject reduction. Here we investigate a subtyping extension of the system λP, which is an abstract version of the type system of the Edinburgh Logical Framework LF. By using an equivalent formulation, we establish some important properties of the new system λP ⩽, including subject reduction. Our analysis culminates in a complete and terminating algorithm which establishes the decidability of type-checking.