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
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
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,
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
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:
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
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:
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.
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.
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.
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
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.
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)
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