Philippa Gardner

Grants

Research Institute in Verified Trustworthy Software Systems (VeTSS)

Amount
£ 654,850
Awarded by
Engineering and Physical Sciences Research Council
From
2017-03-01
To
2022-02-28
Modern software systems comprise components constructed by many parties, ranging from individual open-source developers to companies and government organisations spanning the globe. They are written in multiple, complex languages, depend on the correctness of sophisticated third-party libraries, exploit concurrency and distribution to handle vast data sets, and are developed according to new software design processes that advocate frequent source code updates. Traditional methods for ensuring software reliability are inadequate in this modern context: modern companies move fast, leaving little time for code analysis and testing; traditional testing methods do not work well with concurrent and distributed programs; and the reluctance of users to update mobile apps renders the deployment of software fixes ineffective. Scalable techniques that can provide trust, in the deep technical sense of analysis and verification, are vital not only to support safe software, but also to give stability to this international software infrastructure. The purpose of this new Research Institute in Verified Trustworthy Software Systems (RIVeTSS) is to bring together and support world-class UK academics and industrialists in systems, security and verification, unified by a common interest in program analysis and verification, at the forefront of research developments in fundamental theories and industrial-strength tools, targeting real-world applications. Such analysis of program behaviour is of critical importance to proper management of the rapid evolution of modern software systems.

Funding Extension to Certified Verification of Client-side Web Programs project

Amount
£ 95,173
Awarded by
GCHQ
From
2016-10-01
To
2017-03-31
Additional funding to maintain ongoing research lines in anticipation of long term funding. The funding suports the continuous-integration testing infrastructure for JSRef and JS-2-JSIL, which allows for further testing of the correctness of the JSRef interpreter and JS-2-JSIL compiler against the official ECMAScript Test262 test suite.

Certified Verification of Client-Side Web Programs

Amount
£893,924
Awarded by
Engineering and Physical Sciences Research Council
From
2013-09-30
To
2017-02-28
The Web is evolving at enormous speed from a collection of mainly static web pages to the current huge dynamic ecosystem where the boundary between web pages and software application has become indistinct (e.g. Google maps). This effect is so pronounced that industry is beginning to view the Web as an operating system: e.g., Google's Chrome OS and Firefox OS. This quick transformation has come at a price. We are stuck with dynamic languages developed for the early Web. These languages are unsuited to the development of sophisticated web applications, resulting in modern applications being either overly conservative or needlessly unreliable and insecure. JavaScript is the most widely used language for client-side web programming: that is, in the web browser. Initially, JavaScript was well-suited for the small web-programming tasks being asked of it. With the modern Web however, the demands placed on JavaScript have been huge. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy, untrusted code. This project will provide a certifying verification tool for JavaScript to assert that e.g. a particular web application will maintain the structure of a web page and not leak security information, or that a browser extension will only perform permitted file system operations. Our tool will automatically generate proofs which will be certified (checked) by the well-known Coq proof assistant. Our ambitious aim is to ensure that the software we use to communicate with our banks is at least as reliable as the software as our banks use to communicate with each other.

Facebook Faculty grant

Amount
£27,232/$40,000
Awarded by
Facebook Academics
From
2015-09-01
To
2015-09-01
The Facebook Faculty grants are a one-time unrestricted gift to support researchers working in areas of particular relevance for Facebook.

REMS: Rigorous Engineering for Mainstream Systems

Amount
£1,349,302
Awarded by
Engineering and Physical Sciences Research Council
From
2013-03-01
To
2019-02-28
Computer systems are critical to modern society, from embedded devices and mobile phones through to internet services, but traditional computer engineering cannot produce reliable and secure systems, as we see in the continual stream of errors and security flaws impacting industry and consumers everywhere. Industry relies on informal prose specifications and ad hoc testing, but the complexity and scale of today's systems make it effectively impossible to exclude errors using only these methods (even though perhaps 70\% of development staff in major vendors are devoted to testing) and adversarial exploits all too often turn errors into major security concerns, with huge financial and social costs. Compounding the problem, the industry-wide abstractions around which real systems are built, including the architectural interfaces between multiprocessor hardware and software, and programming languages such as C and C++, are ill-defined, giving rise to ambiguity and error. This is a long-standing problem, motivating extensive research on mathematically rigorous alternatives. Until now, it has been impractical to address mainstream widely-deployed systems with rigorous techniques. Academic research has focussed instead on modest-scale safety critical systems and academic verifications of idealised systems. There has been a deep disconnect between practical industrial engineering and systems research on the one hand, and theoretical research in semantics, verification, and foundations on the other. Now, however, the new approaches that we have, with a pragmatic emphasis on the use of mathematically rigorous models where they can be most effective, finally make it feasible to address industrial-scale systems--- and the commercial and social cost of not doing so is becoming ever greater. It is time for rigorous engineering of mainstream systems, unifying practice and theory. REMS brings together a team of leading theory and systems researchers, with key industrial partners, to establish a new synthesis. We will establish a true engineering mathematics for the construction of more robust and secure computer systems: mathematically rigorous models, verification techniques, and engineering tools applied to the construction of full-scale mainstream computer systems, including key infrastructure in widespread use today (multiprocessors, programming languages, and operating systems). We will couple this with novel programming-language and verification support for future system-building. Developing our recent work with processor vendors and language standards bodies, we will address the technical, engineering and social challenges necessary to bring these techniques into widespread use, enabling a radical improvement in computer engineering as a whole.

Resource Reasoning

Amount
£1,536,661
Awarded by
Engineering and Physical Sciences Research Council
From
2010-01-01
To
2016-06-30
Resource has always been a central concern in computer systems. In classical operating systems for example, processes access system resources such as memory, locks, files, processor time, and network bandwidth; correct resource usage is essential for the overall working of the system. In the World Wide Web, the whole structure can be regarded as a giant, dynamic resource net, with its Uniform ResourceIdentifiers referring to located data and code. Generally, for all kinds of computer system, it is second nature for a programmer to think carefully about the way the system handles resource as part of the programming task in hand. The point of view of this research is that there can be a novel kind of mathematical theory, which we call resource reasoning, which goes hand in hand with programmers' informal thinking about resources. The first stage of such a theory is represented by Separation Logic and its relatives, developments which are suggestive of much more. Our hypothesis is that, just as `resource-oriented thinking' occupies a central position in pre-formal system design, resource is also central to the formal analysis and verification of programs across the modern-day and future computing infrastructure. The challenge is to develop an elegant theory (or theories) of resource reasoning, that both meshes with programmers' and system designers' informal intuitions, and leads to tractable analysis and verification techniques for a range of problem domains such as classic operating systems, the continually-evolving web software, concurrent programming, and even hardware synthesis.The project will provide new theoretical concepts and new prototype tools that will eventually help to make computers that crash less frequently, mishandle our data less frequently, and generally have improved reliability.

Active Web Data

Amount
£171,272
Awarded by
Royal Academy Of Engineering
From
2005-10-01
To
2010-09-30
Fellowship.

Web Data

Amount
£191,000
Awarded by
Microsoft Research Limited
From
2005-10-01
To
2010-09-30

CISBIC / 13

Amount
£155,146
Awarded by
Biotechnology and Biological Sciences Research Council
From
2005-09-01
To
2011-08-31

Smallfoot: Static Assertion Checking for C programs

Awarded by
Engineering and Physical Sciences Research Council
From
2006-11-01
To
2009-10-31
Pointers have long been one of the dark corners of programming languages. Tractable proof and analysis tools are lacking for all but the most simple, shallow, properties of the program heap. A recent theory, separation logic, has shed fresh light on this area, and has generated considerable interest worldwide. It has lead to much simpler by-hand specifications and program proofs than previous formalisms, and it suggests, for the first time, the possibility of scalable analysis methods for expressive heap properties. To date, though, separation logic remains mainly a theoretical advance; there are no tools based on separation logic for any real programming languages.We propose to develop a static assertion checker for C based on separation logic. Separation logic works naturally with a low-level RAM model, and thus appears to be well suited to code that must run close to the hardware without an intermediate abstraction of the kind found in the runtimes of high-level languages such as ML or Java. Much fundamental code of this sort is written in the C programming language, and is outside the effective range of current tools.Our tool, Smallfoot, will accept precondition and postcondition assertions written in separation logic, and programs will be checked using a combination of symbolic execution and specialized proof procedures. Abstract interpretation will be used to alleviate the need to state invariants. We will check structural integrity properties of programs -- such as that data structures are in consistent states, or that resource boundaries are respected -- rather than full functional correctness. In this way we hope to keep specifications simple, and to achieve a high degree of automation. As it is aimed at low-level programs, Smallfoot will be complementary to static assertion checkers for higher-level languages such as the ESC tool for Java and the Spec# tool for C#.Success on the problems in this project could have a significant impact on the use of logic to check properties of systems programs.

CONCUR 2004: Fifteenth International Conference on Concurrency Theory

Amount
£8,174
Awarded by
Engineering and Physical Sciences Research Council
From
2005-01-06
To
2005-04-05
CONCUR 2004 is the fifteenth in a series of annual international conferences devoted to the theory of concurrent computation. Previous venues have been in the USA and various European countries. In 2004 CONCUR will be held in the UK for the first time. The UK has long been a major centre for concurrency research. The conference will disseminate the latest results in concurrency research and will bring together researchers from all over the world to discuss their ideas and plan future work. EPSRC funding for international invited speakers and other expenses will bring down the costs of registration and therefore make it possible for more people to attend, particularly students.CONCUR 2004 will have 11 co-located satellite workshops ranging widely over related and more specialised fields. Particularly important will be the International Workshop on the Foundations of Global Ubiquitous Computing. The intention is to bring together two mostly disjoint research communities - the UK community of Ubiquitous networks research and the community involved with the 'Grand Challenges for Computing Research'by jointly hosting the 3rd edition of an EATCS workshop on the foundations of Global Computing with the 3rd UK Grand Challenge workshop on Global Ubiquitous Computing. EPSRC funding for the Workshop will ensure the maximum possible participation and furtherance of this UK initiative.

Dynamic Net Data: Theory and Experiment

Amount
£241,438
Awarded by
Engineering and Physical Sciences Research Council
From
2004-03-08
To
2007-09-07
Net data, such as XML documents, plays a fundamental role in the exchange of information between globally distributed applications. The analysis techniques, languages and tools associated with such data will be drastically different from conventional ones. This proposal focuses on our distributed model of dynamic net data, consisting of net data with light-weight embedded pi-like processes for updating such data. We will develop a browser for dynamic XML documents, which combines standard languages and tools associated with XML with the ability to interprete and schedule processes. We will contrast our work with Abiteboul's Active XML, an independent related project focusing on web services and service calls rather than processes, which gives us an invaluable opportunity to interact with a highly regarded database research group. We will develop type theories and techniques for reasoning about process behaviour to ensure resource access control and integrity of our data, by extending such reasoning techniques for pi-processes. We will design and implement a distributed update language for dynamic net data, based on our experience with distributed languages based on pi-processes, and pattern-matching languages for analying and manipulating net data. The Grid project provides an invaluable source of example applications. which would inevitably reveal further challenaes to the fundamental theory.

Spatial Logics for Querying Data on the Web

Amount
£171,916
Awarded by
Engineering and Physical Sciences Research Council
From
2003-04-01
To
2006-09-30
The age of the Internet has brought new data management applications and challenges. Data is now accessed over the Web, and is available in a variety of forms including HTML, XML and application-driven formats. To accommodate all types of data, the database research community has introduced the'semi-structured data model', where data is self-describing and irregular. Several practical query languages have been proposed, but their formal foundations and their relationships to logical formalisms are poorly understood, in contrast with the traditional database systems based c the relational model. This proposal focuses on the study of spatial logics for reasoning about semi-structured data, and the application of these logic provide query languages for manipulating such data. We will introduce the'trees with pointers model', a new data structure for representing data on Web. Our model focuses on dangling pointers which we believe occur naturally: for example, a link to a webpage that is currently down. Dangling pointers are used by O'Hearn and Reynolds in their work on pointer arithmetic, but are not emphasised by existing semi-structured data models. V will develop a spatial logic for our model, which allows us to reason locally about disjoint substructures. We will design a query language which integrates well with our model and logic, and compare our approach with existing languages such as XML-QL and XDuce. We will extend our mode to incorporate dynamically-changing structure, as a step towards understanding the dynamic nature of the Web.

AF: Operational Models of Computation

Awarded by
Engineering and Physical Sciences Research Council
From
2000-09-15
To
2002-01-14
Advanced Fellowship

AF: Operational Models of Computation

Awarded by
Engineering and Physical Sciences Research Council
From
2000-04-01
To
2000-09-15
Advanced Fellowship

Calculi for Interactive Systems: Theory and Experiment

Awarded by
Engineering and Physical Sciences Research Council
From
1998-07-01
To
2001-06-30
The biggest current challenge for model-building in computer science is in communications. The Internet, though in use, raises serious behavioural issues regarding, for example, security and the interaction among agents which may travel across links. We shall develop a model whose primary notion is inter-action. We shall start from the pi-calculus, a calculus of mobile processes designed around 1990, and from action calculi, recently introduced to unify the various emerging disciplines of interaction behaviour. The project's two linked strands will together develop a theory of interactive systems based upon experiment. The specific strand will extend the pi-calculus and its sister programming language PICT to describe wide area distributed applications, in which migration and analysis working with a system-design research team. The general strand will develop action calculi theoretically, to integrate techniques for reasoning about interactive behaviour, and to compare and contrast different models of interaction. This general theory will unify specific models such as (extensions of) the pi-calculus, calculi for security, and object-oriented calculi.

Operational Models of Computation

Awarded by
Engineering and Physical Sciences Research Council
From
1997-05-01
To
2000-04-30
Operational models of computation are important for rigorous language design, program development and specification analysis. This proposal studies models of functional and interactive computation, using Milner's action calculi which provides a framework for presenting such models. The proposed research will focus on the theoretical and practical development of action calculi, to achieve a fundamental understanding of the nature of interaction and to integrate techniques for reasoning about functional and interactive behaviour. The proposal consists of three parts: under the generic structure of action calculi, the aim is to develop a logical account of the underlying structure of action calculi and to investigate natural extensions; under semantic models, the aim is to find abstract models which capture the notion of observational behaviour, to provide a setting for comparing action calculi, and to understand the inherent categorical structure contained in the abstract models; and under specification tool and experimentation, the aim is to design and build a specification tool, based on the graphical presentation of action calculi, to help experiment with particular models of computation.