Review report on EPSRC Grant GR/N24872
(01/10/2000 -- 30/09/2003)
Wide-area programming: Language, Semantics and Infrastructure Design
Peter Sewell, Robin Milner
http://www.cl.cam.ac.uk/users/{pes20,rm135}
1 Summary
This project draws together two major lines of research: the study of
distributed system design and the semantic theory of concurrent
processes and programming languages. Wide area distributed systems
are becoming ubiquitous and critical. System designers require a
clear understanding of their behaviour in the presence of partial
failure, malicious attack, and, increasingly, mobility of hardware and
software components. To support this, we are
designing levels of abstraction for distributed programming with
clear, rigorous semantics. During the period of this grant, we have focussed on the following aspects
of distributed computation:
-
Network Semantics. We are developing accurate behavioural
specifications of the ubiquitous UDP and TCP protocols and the
sockets API, focussing on the behaviour in the presence of failure
but necessarily also dealing with the details of flow- and
congestion-control etc.Work on UDP and sockets is complete; a first-draft TCP
specification is also completed. The models use the HOL proof
assistant; they are being experimentally validated, against captured
traces from a test network, to ensure they
describe the de facto standard of the common deployed
implementations.
- Programming language design: Modularity and Versioning.
In a large-scale distributed system one must deal with many
separately-compiled programs, interacting via communication or
persistent stores. Moreover, it is typically impractical to
synchronise software updates, so there can be many different
coexisting versions. We have proposed language constructs and semantics for
type- and abstraction-safe interaction, which may involve dynamic
rebinding and version change, and for dynamic update of long-running systems.
- Security Policy. Mechanisms for expressing security
policy are necessary infrastructure for large-scale systems, but
there is a tension between expressiveness and tractability. We have
designed a policy language and system, Cassandra, based on Datalog
with a tunable constraint domain, and have carried
out a substantial case study, with a policy for a national
Electronic Health Record system, based on the NHS requirements.
- Anonymity and Privacy. A particular aspect of
large-scale systems, in need of analysis, is the extent to which
they do or can provide anonymity and privacy
properties against attackers, which may be able to monitor the
network in powerful ways. We have carried out several lines of
work on this problem, contributing to the design of new
systems.
- Operational Theory.
Bigraphical reactive systems are a
graphical model of widely distributed mobile interactive systems.
They aim to subsume Pi Calculus, Ambient Calculus and Petri Nets, thus
capturing many forms of structure and mobility. In this project they
have been further developed, with emphasis on providing a sharp
uniform theory of behaviour that recovers previous separate
theories. They also aspire to model systems as diverse as sentient buildings
and signal transduction in biological organisms.
2 Programme of Work
The main items of work are described in turn below.
The project structure is largely as originally envisaged; changes
are discussed in §3.
Network Semantics: The TCP/UDP Semantics
The protocols UDP and TCP are ubiquitous, forming the
basis of almost all communication on the Internet, above the
IP internet protocol. UDP provides unreliable asynchronous messaging;
TCP provides bidirectional streams, with retransmission and flow- and
congestion-control. Both are normally used by application programs
via the sockets API.
These protocols, and the API, involve many complexities, both
contingent and intrinsic.
They have been developed over the last 25 years, with some substantial
incremental changes.
There is no single definitive version; instead, there are many
implementations which differ in subtle ways, but have been tuned to
-- in the common cases -- interoperate successfully.
Further, their behaviour is not well documented, even in informal
prose. Some aspects are described in standards (e.g.POSIX), RFCs, and
well-known texts (e.g.those of Stevens).
However, while collectively
these describe most common behaviour, they are not complete, nor
completely correct -- for the whole, there is nothing better than
reading the source code of the implementations that one is dealing
with. This source is not always available. Where it is, it is
emphatically not arranged for clarity -- instead, it is more-or-less
optimised for performance, and embodies many historical artifacts
arising from incremental change. Analysing the source to determine
what the external behaviour is requires
considerable expertise.
To support the production of reliable software using TCP and UDP
sockets we must address these issues, understanding --with mathematical rigour--
both continuous and discrete properties: not only statistical
properties of traffic,
but also the precise interactions of
API and network events within protocol implementations, the treatment
of different kinds of failure, generation of errors, and so on.
We need models of these that are precise (covering all important
details, including implementation differences), accurate (faithful to the
current deployed implementations), and also usable (as informal
documentation by a wide audience, and as a basis for formal
verification by specialists).
In this task we are developing such a formal model for UDP, TCP, and
sockets.
The model
is based upon the available documentation
in conjunction with the source code of the BSD reference
implementation. Crucially, however, it is being experimentally
validated against the most common implementations, checking that the
specification accurately describes their behaviour. A key part of our
work is the experimental discovery of differences in behaviour between
these implementations.
Our formal semantics of UDP has been published
[1, 2, 3, 4, 5]. The associated software
library has been used by Leifer, at INRIA, in an implementation of
failure detectors.
The UDP work, while of independent use, was essentially an initial
trial, to develop tools and techniques. We then moved onto the much
larger task of TCP, which is still in progress. The first draft of
the TCP model is complete (some 14000 lines of HOL source, or 150 typeset pages).
Much work has gone into untangling the historical accumulation of
modification and extension, yielding a semantics that is (relatively)
intelligible and clear as well as precise.
The models are expressed using operational semantics within the HOL theorem prover. This has
allowed us to verify internal consistency, checking type-correctness
of the model and doing machine-checked proof of various sanity
properties. It is also key for our experimental validation: we have
extended HOL with a special-purpose symbolic model-checker which we apply
to our model in order to validate it against experimentally-captured
traces.
These traces are generated on a test
network with machines running three of the common
implementations (Linux, FreeBSD, Windows XP). We have written a test
harness that allows
remote execution of system calls, remote white-box inspection of
protocol state where possible, network packet injection, and network
packet sniffing, all under the control of a test script; it also logs
all events and generates a trace suitable for input to HOL.
At present we generate some 2625 traces,
chosen to get good coverage of the model.
A good fraction can already be processed by the HOL symbolic
evaluator, but further work is required, both on the evaluator itself
and on correcting the model in the light of its results, to ensure
that it does include all the real-world behaviour.
The large size of our model has also necessitated our making various
improvements to the HOL system.
Once our formal model is complete and validated, we intend to prepare
an annotated version for publication and dissemination. We expect
this to be of use in several ways:
-
as reference documentation for implementators of distributed systems,
especially those
that must be failure-aware,
reliable, and multi-platform ones;
- as a reference for
those building new implementations of, or extensions to, TCP;
- as a basis for formal proofs of properties of higher-level
distributed infrastructure algorithms, allowing verification of
executable code rather than the more usual idealised descriptions
(process calculi, automata or plain informal pseudocode); and
- as a demonstration that precise specification and automated
validation of real-world network protocols is feasible -- and
indeed, might usefully be carried out at the design and
standardization stages, rather than post-hoc.
Expressing Infrastructure Layers: Module systems and Versioning
In this task we turn to programming language issues, looking at
what is communicated, complementing the previous task's focus
on how communication takes place.
High-level programming languages for distributed computation should
allow arbitrary language values to be communicated; most flexibly,
they should provide type-safe marshalling of arbitrary values
to and from byte strings. There are many important issues, which have
received little attention in the literature.
In particular: (1) unmarshalling can
involve rebinding to local resources; (2) values of
abstract types can be communicated, and a globally-coherent
notion of type equality is needed to ensure that unmarshalling respects
abstraction; and (3) interoperation between separately-built programs
with different versions of shared modules must be supported, with
fine-grain version control.
In our early work here [6] (supported partly by this grant
and partly by the overlapping GRL62290), we focussed on abstract types
in the setting of an ML-like module system. We modelled separate
compilation/linking and execution of programs that interact along
typed channels. Interaction may involve communication of values of
abstract types; we proposed some simple fine-grain versioning control
of these types to support interoperation of old and new code. The
system made use of a second-class module system, with singleton kinds
to express type sharing,
and a novel operational semantics for separate compilation/linking and
execution. An implementation was produced as a student project.
Most programming languages adopt static binding, but for distributed
programming an exclusive reliance on static binding is too
restrictive: dynamic binding is required in various guises, eg when a
marshalled value is received from the network, containing identifiers
that must be rebound to local resources. Typically it is provided
only by ad-hoc mechanisms that lack clean semantics.
In [7] we developed core
dynamic rebinding mechanisms as extensions to simply-typed
call-by-value (CBV)
lambda-calculus. To do so we first explored refinements of the
CBV reduction strategy that delay instantiation, to ensure
computations make use of the most recent versions of rebound
definitions. We introduced redex-time and destruct-time
strategies. The latter formed the basis for a lambda-mark calculus
that supports dynamic rebinding of marshalled values, while remaining
as far as possible statically-typed. We extended
lambda-mark with concurrency and communication, giving examples
showing how wrappers for encapsulating untrusted code can be
expressed. Finally, we showed that a high-level semantics for dynamic
updating can also be based on the destruct-time strategy, defining a
lambda-update calculus with simple primitives to provide type-safe,
dynamic updating of code.
We have a direct implementation of the destruct-time lambda semantics,
and are working on realistic compilation strategies.
We thereby established primitives and a
common semantic foundation for a variety of real-world dynamic
rebinding requirements.
In [8, 9] we returned to the question of
abstraction-preserving marshalling,
addressing some pragmatic difficulties in the earlier proposal
of [6].
Here we obtained a namespace for abstract types that is global, i.e.meaningful between programs, by hashing module definitions.
We examined the scenarios in which values of abstract types are
communicated from one program to another, and ensured, by
constructing hashes appropriately, that the dynamic and static
notions of type equality mirror one another.
In many common cases this ensures marshalling/unmarshalling `just
works' as one would wish, without the earlier need to propagate
new-generated type names. Again
we used singleton kinds to express abstraction in the static
semantics; now abstraction is tracked in the dynamic semantics by
coloured brackets. These allowed us to prove preservation, erasure,
and coincidence results. We argued that our proposal is a good basis
for extensions to existing ML-like languages, pragmatically
straightforward for language users and for implementors.
In [10] we looked in more detail at dynamic update of running
systems, e.g.telecomms switches that cannot afford lengthy restarts.
One would like this to be possible in a semantically well-founded way,
rather than by issuing binary patches. To this end, we
defined a small update calculus with precise
mathematical semantics, based on the redex-time lambda-calculus. It
supports updating technology similar to that of the programming
language Erlang. Here new versions of a module can be added to
a running system, and there is fine-grain control for how execution
changes over from old to new code. Work on a second update calculus,
with updating of the implementations of abstract data types,
reminiscent of the language Dynamic ML, is in progress, forming part
of the thesis work of PhD student Gareth Stoyle.
In ongoing work we are considering the integration of marshalling
constructs in the presence of both dynamic rebinding and abstract
types, and also with rich languages of versions and version
constraints. In a paper submitted for publication we discuss the
(large!) design space and also describe an experimental language,
Acute, which we are designing and implementing to carry out
some more substantial experiments.
As a further, internal, experiment, we are developing Acute
above the FreshML of Pitts et al.
It is itself an extension of a fragment of OCaml; a medium-to-long
term goal is to integrate these constructs with the OCaml
distribution; our close contacts with members of INRIA Rocquencourt
(including Leifer, Peskine, and the OCaml development team) may
make this feasible.
We have also considered the integration of lightweight XML support
into a high-level concurrent language, with a simple type system that
guarantees well-formedness but does not involve the complexity of
systems for validity [11]. An implementation was produced as a
student project.
Reasoning
As listed in the Network Semantics section above, semantic models of
distributed systems have several applications, one of which is to
support formal proof about higher-level abstractions.
Such proofs, about executable code rather than idealisations, are
still technically very challenging, so case studies are required to
establish techniques and idioms.
Our initial work on UDP involved hand proof of properties of a simple
heart-beat algorithm, expressed in an OCaml fragment for which we gave
a pen-and-paper operational semantics. It is obviously desirable to
be able to carry out such proofs within a mechanical proof assistant,
to assure that none of the many cases are overlooked. To do so
requires the programming language also to be embedded in the proof
assistant, integrated with the network semantics.
This is being worked on by Michael Compton, a PhD student in the
Automated Reasoning Group. The UDP and language semantics have been
set up, here using the Isabelle proof assistant (the UDP semantics
being semi-automatically ported from HOL), and some properties
established; work is ongoing.
For a larger example, we are working on coding the Chord P2P
algorithm above the TCP semantics, adding the necessary concurrency
primitives to Acute (which already has modules and a TCP
library matching our specification).
Earlier work, proving the correctness of a communication
infrastructure for mobile computation (providing high-level
location-independent messaging between mobile computations, was
completed in the first 18 months of this grant [12, 13];
supported partly by this grant
and partly by the overlapping GRL62290.
Security Policy
Moving to a higher level of abstraction, flexible control of security policy
is needed in large distributed systems.
A number of rule- and role-based systems have been proposed, but there
is an unresolved tension between expressiveness and tractability, and
to our knowledge few large-scale realistic examples have been
developed.
Building on earlier work at Cambridge (the OASIS system) and elsewhere we have
developed Cassandra, a language and system for
expressing policy, and a substantial case study. We
have developed a security policy for a national Electronic Health
Record system, based on the requirements for the ongoing UK National
Health Service procurement exercise.
This is part of the thesis work of PhD student Moritz Becker.
Cassandrapolicies are expressed in a language based on Datalog with
constraints. The expressiveness of the language (and its
computational complexity) can be tuned by choosing an appropriate
constraint domain.
Cassandrais role-based; it supports credential-based access control
(e.g.between administrative domains); and rules can refer to remote
policies (for automatic credential retrieval and trust negotiation).
Moreover, the policy language is small, and it has a formal semantics
for query evaluation and for the access control engine.
For the case study we choose a constraint domain C0 that is
sufficiently expressive to encode many policy idioms. The case study
turns out to require many subtle variants of these; it is important to
express this variety smoothly, rather than add them as ad hoc
features.
By ensuring only a constraint compact fragment of C0 is
used, we guarantee a finite and computable fixed-point model. We use
a top-down evaluation algorithm, for efficiency and to guarantee
termination.
The case study (with some 310 rules and 58 roles) demonstrates that
this language is expressive enough for a real-world application;
preliminary implementation results suggest that the performance should
be acceptable. A paper has been submitted for publication.
A journal version of earlier work on Securing Mobility was
also completed during the project [14]; we are currently
studying how to integrate such primitives, allowing encapsulation of
untrusted code, with the Acute constructs for marshalling.
Anonymity and Privacy
In the last few years new desirable properties of distrubuted systems
have been identified. One of these is massive scalability in the
presence of failures; this has lead to the development of peer-to-peer
systems. Others are anonymity and privacy against a
variety of network adversaries. Indeed, anonymity systems which enable
users to send anonymous email and do anonymous web browsing have been
designed and implemented, many using mix networks. We have made
substantial progress in identifying just how much anonymity these
systems provide. This is the subject of Andrei Serjantov's PhD thesis
work.
We developed a new metric for measuring anonymity,
showed that our new metric is practical (can be calculated for real
anonymity systems) and useful for comparing anonymity properties of
various schemes [15]. This line of work was continued by
looking at various known mixes and identifying some of their anonymity
properties against active and passive attackers [16]. This
work is directly relevant to deployed systems providing strongly
anonymous email. This lead us to a design of a new mix with stronger
properties which also adapts to the traffic load [17]. Finally,
we devised a method for analysing anonymity properties of timed mixes
[18]. More work along this general line of research is in
progress; we have developed a model which enables us to assess the
anonymity of an entire mix network (a complete system) rather than
just its building blocks.
We have also examined the anonymity of real-time connection-based
systems which enable anonymous web browsing. We showed in [19]
that such systems currently provide no anonymity against some
realistic threat models, but can be improved. Furthermore, we noted
that contrary to popular opinion, peer-to-peer anonymity systems
generally provide less anonymity against our threat mdoel than
"classic" designs.
One further line of work is looking at how padding and rerouting
improves the anonymity of systems [20]. Here we took a
slightly different model, showing how to calculate anonymity and the
extent to which padding and rerouting helps on simple examples.
Finally, we noted that anonymity systems can be used as a building
block to provide stronger censorship resistance [21].
Operational Theory
This task is a continuation of a preceding EPSRC project in Cambridge
(investigators Robin Milner, Philippa Gardner and Peter Sewell) on
theoretical models for distributed systems.
Journal versions of earlier Operational Theory work were
completed during the project: work on indexed models for interleaving
and causal semantics of name-passing calculi [22]; and work
on deriving bisimulation congruences from rewrite systems,
without name-binding but with rewriting up to a monoidal parallel operator
and with parametric rewrite rules [23].
Groundwork laid in these journal papers, and by a conference paper
by Leifer and Milner in 2000, took the form of an original theory that
allows a labelled transition system (LTS), and thereby also a variety
of behavioural relations such as the failures preorder or bisimilarity,
to be derived and analysed uniformly over a wide range of models.
Moreover, the uniform method guarantees that these relations are
congruential, i.e. they faithfully characterise the behaviour of
agents in all possible contexts.
In the present project the emphasis has been to apply this work
to models that express the /emphmobility of distributed systems in
the widest possible sense of the word. This includes movement of physical
interactive devices (mobile phones or hand-held computers), of software
among mobile and fixed devices, of links (e.g. URLs) between
hardware and software, and even reconfiguration and data-movement within
a software system. The intention is that within the same frame one can
model computing and communication, both microscopically and macroscopically.
In a series of papers [24, 25, 26, 27, 28, 29, 30, 31] the groundwork has
been both refined abstractly and applied to a specific model,
bigraphical reactive systems. Bigraphs are so called because
they combine two different structures in a system: its placing
(locality) and its linking connectivity. Mobility consists of
reconfiguration of both structures. In the cited work, especially in
the two long Technical Reports, it is shown that various previous
concurrency models are representable, including both the Pi Calculus
and the Ambient Calculus. The papers further show that significant
parts of the Pi behavioural theory of the Pi Calculus are exactly
recovered. Subsequent work (not published) will further investigate
the representation of Ambients and of Petri Nets within the bigraph
model. Thus the model aspires to cover as wide a range of
distributed-system concepts as possible, while retaining a sharp and
tractable theory.
Three PhD students have been involved in this work. The PhD dissertation
of Leifer [29] was mostly done earlier, but completed within
the project period. Ole-Hoegh Jensen is writing
a dissertation on bigraphs for the Pi and Ambient Calculi, while
Alistair Turnbull is working on a linear graphical calculus called
Min, intended as a intemediate language/model for compilation of
interactive languages such as Java.
Other
During the course of the project the PhD thesis of Keith Wansbrough,
on Simple Polymorphic Usage Analysis was completed [32], as was a
tutorial on the p-calculus and its applications [33].
3 Development
The project has developed much as in the original proposal. The main
changes were: (1) emphasis shifted towards the Network Semantics task,
as the value and scale of this work became apparent, and (2) the work
on Anonymity and Privacy was added. In more detail:
The Network Semantics task has expanded substantially from the work
envisaged in the initial proposal, where we considered only rather
idealised process calculi, only loosely based on UDP and TCP and
ignoring the sockets API. Shortly after beginning that work, it
became clear that to really understand communication semantics in the
presence of failure and attack it is necessary to examine more of the
real-world detail, and indeed that a fully-validated model would be of
much wider applicability.
Work on Module Systems and Versioning has also progressed further than
originally envisaged, moving to an experimental implementation,
integrating several of the required features.
In the original proposal more work on reasoning was envisaged. Our
shift of goal in the Network Semantics section, from an idealised
calculus to a real-world accurate and detailed model, has inevitably
delayed the treatment of larger-scale reasoning examples; we hope to
carry them out in the near future.
In the future we hope also to link the work on Security Policy to the
lower-level Network Semantics models, reasoning about the behaviour of
the distributed policy engine in the presence of failure. This link
was envisaged in the original proposal, under Case Study:
OASIS; as it has turned out we have looked at both Network Semantics
and Policy in greater depth, but so far independently.
The task on Anonymity and Privacy was not part of the the original
proposal; it arose as the thesis work of the project student (Andrei
Serjantov) developed in this direction, from his early contributions
to Network Semantics.
Finally, the original proposal contained a task Interworking and
Implementation. Various implementation work has already been
described; for the Module Systems and Versioning work it has been more
fruitful --for the time being-- to study the problems in a clean
setting rather that commit to interoperation with an existing
language, with all the complexities of an existing (and limited) type
system that that entails. We are, however, aiming to develop
primitives that can eventually be smoothly integrated with existing
ML/OCaml implementations.
4 Personnel
The original proposal was coauthored by Peter Sewell (PI), James
Leifer, and Robin Milner (CI); it was intended to employ Leifer as a
Research Associate.
In the event, Leifer took up a position at INRIA Rocquencourt; as the
publications indicate, there has been an active collaboration with him
and with Gilles Peskine, a PhD student there.
Keith Wansbrough has been employed as an RA for the duration of the
project, working on many aspects. Alistair Turnbull was also employed
part-time for 6 months, working on operational theory. Andrei
Serjantov was supported by the project studentship, initially working
on Network Semantics but then turning to the foundations of Anonymity
and Privacy. PhD students Gareth Stoyle and Moritz Becker have also
contributed substantially to this work, looking respectively at programming language
design for dynamic update and at security policy, and Michael Compton,
a PhD student in the automated reasoning group, has begun work on
reasoning above the UDP model.
Two undergraduate interns, Vilhelm Sjöberg and Christian
Steinrücken, were supported during the summer of 2003 to work on
the early stages of the Acute implementation.
Other collaborators include Gavin Bierman (University of Cambridge),
Michael Norrish (National ICT Australia (NICTA), Canberra research
lab), Michael Hicks (University of Maryland, College Park), Ole Jensen
(Aalborg University), George Danezis (University of Cambridge),
Claudia Diaz (K.U.Leuven ESAT-COSIC, Leuven-Heverlee, Belgium),
Richard Newman (CISE Department, University of Florida, Gainesville,
FL), Ira Moskowitz (Naval Research Laboratory Washington, DC), Paul
Syverson (Naval Research Laboratory Washington, DC), and Gian Luca
Cattani (University of Cambridge and DS Data Systems).
5 Wider contribution
Sewell was an invited speaker at a joint EPSRC/DTI Outreach seminar,
and has served on the programme committees for the FWAN workshop
(Foundations of Wide-Area Languages), EXPRESS 02, EXPRESS 03, POPL
04, and ICFP 04. Milner gave invited talks at POPL01, ICATPN01 (Petri
Nets), ICGT02 (Graph Rewriting), and a short course on Bigraphs at the
Advanced Course on Petri Nets, Eichstätt, September 03.
Review report on EPSRC Grant GR/N24872
(01/10/2000 -- 30/09/2003)
Wide-area programming: Language, Semantics and Infrastructure Design
List of Publications
The five publications identified as particularly significant are
[4, 7, 8, 14, 28], indicated by a below.
References
- [1]
-
Andrei Serjantov, Peter Sewell, and Keith Wansbrough.
The UDP calculus: Rigorous semantics for real networking.
Technical Report 515, Computer Laboratory, University of Cambridge,
July 2001.
iv+70pp. Technical Report.
- [2]
-
Andrei Serjantov, Peter Sewell, and Keith Wansbrough.
The UDP calculus: Rigorous semantics for real networking.
In Proceedings of TACS 2001: Theoretical Aspects of Computer
Software (Sendai), LNCS 2215, pages 535--559, October 2001.
Conference; Refereed.
- [3]
-
Peter Sewell, Keith Wansbrough, and Michael Norrish.
Timing UDP: The HOL model.
Available from
http://www.cl.cam.ac.uk/users/pes20/Netsem/index.html, July 2001.
Software.
- [4]
-
Keith Wansbrough, Michael Norrish, Peter Sewell, and Andrei Serjantov.
Timing UDP: mechanized semantics for sockets, threads and failures.
In Proceedings of ESOP 2002: European Symposium on Programming
(Grenoble) LNCS 2305, pages 278--294, April 2002.
Conference; Refereed; .
- [5]
-
Michael Norrish, Peter Sewell, and Keith Wansbrough.
Rigour is good for you, and feasible: reflections on formal
treatments of C and UDP sockets.
In Proceedings of 10th ACM SIGOPS European Workshop
(Saint-Emilion), pages 49--53, September 2002.
Conference; Refereed.
- [6]
-
Peter Sewell.
Modules, abstract types, and distributed versioning.
In Proceedings of POPL 2001: The 28th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (London), pages 236--247,
January 2001.
Conference; Refereed.
- [7]
-
Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, and Keith
Wansbrough.
Dynamic rebinding for marshalling and update, with destruct-time
lambda.
In Proc. ICFP 2003: the 8th International Conference on
Functional Programming, August 2003.
Conference; Refereed; Int. Co-author; .
- [8]
-
James Leifer, Gilles Peskine, Peter Sewell, and Keith Wansbrough.
Global abstraction-safe marshalling with hash types.
In Proc. ICFP 2003: the 8th International Conference on
Functional Programming, August 2003.
Conference; Refereed; Int. Co-author; .
- [9]
-
James Leifer, Gilles Peskine, Peter Sewell, and Keith Wansbrough.
Global abstraction-safe marshalling with hash types.
Technical Report UCAM-CL-TR-569, University of Cambridge Computer
Laboratory, June 2003.
Also published as INRIA Rocquencourt report RR-4851. Technical Report; Int. Co-author.
- [10]
-
Gavin Bierman, Michael Hicks, Peter Sewell, and Gareth Stoyle.
Formalizing dynamic software updating.
In Proceedings of USE 2003: the Second International Workshop on
Unanticipated Software Evolution, April 2003.
Conference; Refereed; Int. Co-author.
- [11]
-
G. M. Bierman and P. Sewell.
Iota: A concurrent XML scripting language with applications to home
area networking.
Technical Report 557, Computer Laboratory, University of Cambridge,
January 2003.
32pp. Technical Report.
- [12]
-
Asis Unyapoth and Peter Sewell.
Nomadic Pict: Correct communication infrastructure for mobile
computation.
In Proceedings of POPL 2001: The 28th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (London), pages 116--127,
January 2001.
Conference, Refereed.
- [13]
-
Asis Unyapoth.
Nomadic Pi Calculi: Expressing and Verifying Infrastructure for
Mobile Computation.
PhD thesis, Computer Laboratory, University of Cambridge, June 2001.
Published as Technical Report 514. PhD Dissertation.
- [14]
-
Peter Sewell and Jan Vitek.
Secure composition of untrusted code: Box-p, wrappers and
causality types.
Journal of Computer Security, 11(2):135--188, 2003.
Journal; Refereed; Int. Co-author; .
- [15]
-
Andrei Serjantov and George Danezis.
Towards an information theoretic metric for anonymity.
In Paul Syverson and Roger Dingledine, editors, Privacy
Enhancing Technologies, volume 2482 of LNCS, San Francisco, CA, April
2002.
Conference; Refereed.
- [16]
-
Andrei Serjantov, Roger Dingledine, and Paul Syverson.
From a trickle to a flood: Active attacks on several mix types.
In Fabien Petitcolas, editor, 5th Workshop on Information
Hiding, volume 2578 of LNCS, pages 36--52. Springer-Verlag, October
2002.
Conference; Refereed; Int. Co-author.
- [17]
-
Claudia Diaz and Andrei Serjantov.
Generalising mixes.
In Roger Dingledine, editor, Proc. PET 2003: the 3rd Privacy
Enhancing Technologies workshop. Springer-Verlag, LNCS 2760, March 2003.
Conference; Refereed; Int. Co-author.
- [18]
-
Andrei Serjantov and Richard E. Newman.
On the anonymity of timed pool mixes.
In Security and Privacy in the Age of Uncertainty, pages
427--434, Athens, Greece, May 2003. Kluwer.
(Workshop on Privacy and Anonymity Issues in Networked and
Distributed Systems) Conference; Refereed; Int. Co-author.
- [19]
-
Andrei Serjantov and Peter Sewell.
Passive attack analysis for connection-based anonymity systems.
In Proc. ESORICS 2003: the 8th European Symposium on Research in
Computer Security, LNCS 2808, October 2003.
Conference; Refereed.
- [20]
-
Richard E. Newman, Ira S. Moskowitz, Paul Syverson, and Andrei Serjantov.
Metrics for traffic analysis prevention.
In Roger Dingledine, editor, Proc. PET 2003: the 3rd Privacy
Enhancing Technologies workshop. Springer-Verlag, LNCS 2760, March 2003.
Conference; Refereed; Int. Co-author.
- [21]
-
Andrei Serjantov.
Anonymizing censorship resistant systems.
In Proc. IPTPS: the 1st International Peer To Peer Systems
Workshop, March 2002.
Conference; Refereed.
- [22]
-
Gian Luca Cattani and Peter Sewell.
Models for name-passing processes: Interleaving and causal.
Information and Computation, page 55pp.
Accepted for publication. Journal; Refereed.
- [23]
-
Peter Sewell.
From rewrite rules to bisimulation congruences.
Theoretical Computer Science, 274(1--2):183--230, March 2002.
Journal; Refereed.
- [24]
-
R. Milner.
Computational flux.
In Proc. 28th ACM SIGACT-SIGPLAN Symposium on Principles of
Programming Languages, pages 220--221, 2001.
Conference, Invited Paper.
- [25]
-
R. Milner.
The flux of interaction.
In Proc. 22nd International Conference on Application and Theory
of Petri Nets, pages 19--22, 2001.
Conference, Invited Paper.
- [26]
-
R. Milner.
Bigraphical reactive systems.
In CONCUR 2001 -- Concurrency Theory, Proc. 12th International
Conference, LNCS2154, pages 16--35, 2001.
Conference, Invited Paper.
- [27]
-
R. Milner.
Bigraphs as a model for mobile interaction.
In ICGT 2002, First International Conference on Graph
Transformation, LNCS2505, pages 8--13, 2002.
Conference, Invited Paper.
- [28]
-
O.-H. Jensen and R. Milner.
Bigraphs and transitions.
In Proc 30th ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages (POPL), page 16pp, 2003.
Conference; Refereed; .
- [29]
-
J. Leifer.
Operational congruences for reactive systems.
Technical Report 521, University of Cambridge Computer Laboratory,
2001.
PhD Dissertation.
- [30]
-
R. Milner.
Bigraphical reactive systems: basic theory.
Technical Report 523, University of Cambridge Computer Laboratory,
September 2001.
87pp, Technical Report.
- [31]
-
O.-H. Jensen and R. Milner.
Bigraphs and mobile processes.
Technical Report 570, University of Cambridge Computer Laboratory,
July 2003.
121pp, Technical Report.
- [32]
-
Keith Wansbrough.
Simple Polymorphic Usage Analysis.
PhD thesis, Computer Laboratory, University of Cambridge, 2002.
PhD Dissertation.
- [33]
-
Peter Sewell.
Chapter 9, Pi Calculus, in the book Formal Methods for
Distributed Processing, A Survey of Object Oriented Approaches,
edited by Howard Bowman and John Derrick, December 2001.
Book Chapter.
This document was translated from LATEX by
HEVEA.