Research Projects

Links Security

Storing state in the client tier (in forms or cookies, for example) improves the efficiency of a web application, but it also renders the secrecy and integrity of stored data vulnerable to untrustworthy clients. We study this general problem in the context of the Links multi-tier web-programming language. Like other systems, Links stores unencrypted application data, including web continuations, on the client tier; hence, Links is open to attacks that expose secrets, and modify control flow and application data. We characterise these attacks as failures of the general principle that security properties of multi-tier applications should follow simply from review of the source code (as opposed to the detailed study of the files compiled for each tier, for example). We propose a secure compilation strategy, which uses authenticated encryption to eliminate these threats, and we implement it as a simple extension to the Links system. We model this compilation strategy as a translation from a core fragment of the language to a concurrent lambda-calculus equipped with a formal representation of cryptography. To formalize source-level reasoning about Links programs, we define a type and effect system for our core language; our implementation can machine-check various integrity properties of the source code. By appeal to a recent system of refinement types for secure implementations, we show that our compilation strategy guarantees all the properties provable by our type and effect system.

Published in TLDI 2009: PDF Full Version: PDF

Data-Driven Declarative
Networking (D3N) for
Pocket Switched Networks

We propose Declarative Networking for Pocket Switched Networks (PSNs): a type of Delay Tolerant Networks (DTNs), which is decentralised and distributed over a multitude of devices that are dynamically networked and carried by people. We envision an emergence of a new type of communication based on physical proximity, where people encounter each other and devices directly communicate within their range. Building an efficient data dissemination and a search mechanism for PSNs are highly influenced by interaction of people, mobility, time, location, and social networks. We introduce declarative networking for PSNs called D3N, which allows applications to construct a protocol description consisting of a reactive behaviour of a distributed node. We exploit functional programming, the middle ground between pure declarative languages and imperative languages. In this paper, we show a snapshot of D3N including a node architecture and several examples demonstrating a power of D3N.

Published in MobiHeld 2009: PDF


This report provides an overview of the final year project undertaken as part of a BSc (Hons) degree in Computer Science at the University of Kent during the academic year 2003-4. The project involved creating a software application that enables multiple physically isolated individuals to collaborate, learn, and give presentations through virtual meetings. The solution produced was entitled jMule, the Java Multi User Learning Environment. This paper outlines the processes, design rationale, implementation and testing that were conducted during this project and offers an exploration of possible future enhancements. It concludes by offering critical evaluation on the overall success of the project.

Project Website:


In this dissertation we present a novel approach for performing model checking of Web Services composition on computational and data Grid infrastructures. Using two theoretical modelling languages for the specification of distributed systems and processes (Petri nets and CCS) we specify composition in an abstract way that is useful for implementations. Finally, we present the design of a prototype tool that implements these ideas and give directions for future research.

Project Website:

Conferences & Summer Schools

Gordon Plotkin Symposium

Dates: Sep 7 - Sep 8, 2006
Location: Edinburgh, UK

A symposium to celebrate the 60th birthday of Gordon Plotkin in Edinburgh.

Symposium Website:


Dates: Aug 21 - Aug 25, 2006
Location: Copenhagen, DK

The one-week GLOBAN summer school gives doctoral students and other young researchers a comprehensive overview of contemporary techniques for analysis and verification of models of global computing systems characterized by concurrency, communication, heterogeneity and distribution. Organised by IMM/DTU in association with the SENSORIA project and the ITMAN PhD school.

School Website:

Trends in Concurrency

Dates: Jul 24 - Jul 29, 2006
Location: Bertinoro, Italy

Concurrency is a pervasive and essential characteristic of modern computer systems. Whether it is the design of new hyperthreading techniques in computer architectures, specification of non-blocking data structures and algorithms, implementation of scalable computer farms for handling massive data sets, or the design of a robust software architecture for distributed business processes, a deep understanding of mechanisms and foundations for expressing and controlling concurrency is required.

The goal of the school is to expose graduate students and young researchers to new ideas in concurrent programming from experts in academia and industry. The school provides a unique opportunity for students to have engaging discussions on cutting-edge research with instructors in a focused environment. The school covers one week and alternates monograph courses of 4/6 hours and short courses of 2/3 hours.

School Website:

BCTCS 2005

Dates: Apr 4 - Apr 7, 2006
Location: Swansea, UK

The purpose of the British Colloquium in Theoretical Computer Science (BCTCS) is to provide a forum in which researchers in theoretical computer science can meet, present research findings, and discuss developments in the field. It also aims to provide an environment in which PhD students can gain experience in presenting their work, and benefit from contact with established researchers.

  • Abstract of my talk (pdf)
  • The presentation (1up)

Colloquium Website:

CSC 2004

Dates: Aug 28 - Sep 11, 2004
Location: Vico Equense, Italy

Since the early eighties CERN has organized every year the CERN School of Computing (CSC), in one of the CERN Member States. CERN Schools of Computing, usually held in August/September, are open to postgraduate students and research workers with a few years of experience in elementary particle physics, in computing or in related fields. The participants come mainly from the CERN Member States or from laboratories in countries associated with CERN. However, a fraction of the students come from outside the particle physics community, generally attracted by the advanced topics that are taught. Attendance ranges from 70 to 80 students, typically of 15 to 25 different nationalities.

During the school I gave a relaxing social talk on "The 7 Sins of Software Engineers in HEP". The initial plan was to speak about the 10 commandments of Software Engineering in HEP but I'd rather avoid commiting Hybris and leave commandments to more Godly figures.

  • Slides for "The 7 Sins of Software Engineers in HEP" 1up 4up

School Website:

Valid HTML 4.01!
Last modified:
Valid CSS!