@article{physics4,
author = {M. E. Woods and B. J. Hopkins and G. F. Matthews and
G. M. McCracken and
P. M. Sewell and H. Fahrang},
title = {An Investigation of the Secondary-Electron Emission
of Carbon Samples Exposed to a Hydrogen Plasma},
journal = {J. Physics D: Applied Physics},
year = {1987},
volume = {20},
optnumber = {},
pages = {1136--1142},
optmonth = {},
note = {},
topic = {plasma_physics},
url = {http://iopscience.iop.org/article/10.1088/0022-3727/20/9/008},
abstract = {Measurements of secondary-electron-emission (SEE) yield are reported for samples of clean 5890 PT graphite and for the same material exposed for some months in the JET Tokamak. The samples exposed in the JET Tokamak give substantially higher values than the clean samples. Controlled experiments show that both implantation with H2+ ions and deposition of thin metal films increase the SEE yield. The experimental data have been integrated over a 3D Maxwellian distribution to obtain the values of effective SEE yield expected from a plasma as a function of electron temperature. From these SEE yields, theoretical values of sheath potential and sheath energy transmission factor have been calculated. The implications for ion sputtering and power loss are discussed.}
}
@article{physics1,
author = {G. F. Matthews and P. C. Stangeby and P. M. Sewell},
title = {Investigation of the Wake Due to a Large Probe, using
a Spatially Scanning {L}angmuir Probe},
journal = {J. Nucl. Mater.},
year = {1987},
volume = {145--147},
optnumber = {},
pages = {220--224},
month = feb,
note = {},
topic = {plasma_physics},
url = {https://inis.iaea.org/search/search.aspx?orig_q=RN:19052803},
abstract = {This paper describes direct experimental investigation of the region of plasma perturbed by a probe. Two adjacent probes have been mounted on the DITE tokamak. The large 'disturber' probe is a rectangular graphite plate that creates the main particle flow pattern and can be biased with respect to the torus. The smaller 'search' Langmuir probe is located 0.5 m away on the same magnetic field line. It can be swept back and forth mechanically through the shadow of the main probe many times during each discharge. Through measurements of ion saturation current at many distinct radii, a complete map of the perturbed region has been built up and transformed into radial and poloidal coordinates. A numerical solution of the two-dimensional diffusion equations is compared with experimental data in the limiter shadow. Two zones of substantially different interconnection length are included in the model. The assumption of equal radial and poloidal cross-field diffusion coefficients (Dperpendicularto = 0.18 m2 s-1) is found to give a good fit with the data. (orig.)}
}
@article{physics2,
author = {G. F. Matthews and G. M. McCracken and P. C. Stangeby
and C. S. Pitcher and
P. M. Sewell and D. H. J. Goodall},
title = {The Optimisation of Limiter Geometry to Reduce
Impurity Influx in {T}okamaks},
journal = {Plasma Physics and Controlled Fusion},
year = {1987},
volume = {29},
number = {2},
pages = {189--203},
month = feb,
note = {},
topic = {plasma_physics},
url = {http://iopscience.iop.org/article/10.1088/0741-3335/29/2/005},
abstract = {The authors discuss the impurity control limiter (ICL) which has an inverted geometry. The ICL shape is designed to direct the impurities towards the wall. They present the results from a two-dimensional neutral particle code which maps the ionisation of carbon physically sputtered by deuterons from a carbon limiter. This ionisation source is coupled to a one-dimensional impurity transport code which calculates the implied central impurity density. The results demonstrate that the ICL achieves impurity control in two ways. Firstly, many of the sputtered impurities directed towards the wall are not ionised and return to the wall as neutrals. Secondly, much of the ionisation which does occur is located in the scrape-off layer. They conclude that a reduction in central impurity density of a factor of 10 is possible in a Tokamak such as DITE provided that the limiter is the main source of impurities.}
}
@article{physics3,
author = {G. F. Matthews and G. M. McCracken and P. M. Sewell
and M. E. Woods and B. J. Hopkins},
title = {The Determination of Sheath Potential from Retarding
Field Analyser Measurements in {T}okamak Edge Plasmas},
journal = {J. Nucl. Mater.},
year = {1987},
volume = {145--147},
optnumber = {},
pages = {225--230},
month = feb,
note = {},
topic = {plasma_physics},
url = {https://doi.org/10.1016/0022-3115(87)90332-1},
abstract = {Experimental measurements of the energy distributions of ions and electrons arriving at a surface in the boundary layer of a tokamak have been made with a retarding field analyser. The analyser uses a 9 μm entrance slit which is less than the Debye length for the plasma conditions investigated. The electron energy distributions are Maxwellian and the ion energy distributions are displaced Maxwellians, as expected. The sheath potential is derived from the ion energy distribution and found to be ∼2kTe, slowly decreasing with electron temperature. Measurements of secondary electron emission yield have been made on materials exposed in a tokamak as functions of incident electron energy and angle. This data have been integrated to obtain the effective yield of a full three-dimensional Maxwellian distribution. Using these results the theoretical sheath potentials have been calculated as functions of electron temperature and have been found in good agreement with the values that were measured directly.}
}
@inproceedings{Sew94,
author = {Peter M. Sewell},
title = {Bisimulation is Not Finitely (First-Order) Equationally Axiomatisable},
conf = {LICS 1994},
booktitle = {Proceedings of the 9th IEEE Symposium on Logic in Computer Science (Paris)},
year = {1994},
opteditor = {},
pages = {62--70},
organization = {IEEE},
optpublisher = {},
optaddress = {},
month = jul,
note = {Subsumed by the APAL 1997 paper},
url = {https://doi.org/10.1007/3-540-63141-0},
doi = {10.1007/3-540-63141-0},
pdf = {http://www.cl.cam.ac.uk/users/pes20/lics-nonax.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/lics-nonax.ps},
abstract = {This paper considers the existence of finite equational axiomatisations of bisimulation over a calculus of finite state processes. To express even simple properties such as mu X E=mu X E[E/X] equationally it is necessary to use some notation for substitutions. Accordingly the calculus is embedded in a simply typed lambda calculus, allowing axioms such as the above to be written as equations of higher type rather than as equation schemes. Notions of higher order transition system and bisimulation are then defined and using them the nonexistence of finite axiomatisations containing at most first order variables is shown.
The same technique is then applied to calculi of star expressions containing a zero process --- in contrast to the positive result given in [FZ93] for BPA*, which differs only in that it does not contain a zero.},
topic = {axiomatisability}
}
@phdthesis{Sew95,
author = {Peter Michael Sewell},
title = {The Algebra of Finite State Processes},
school = {University of Edinburgh},
year = {1995},
optcrossref = {},
optkey = {},
optaddress = {},
month = oct,
opttype = {},
note = {Dept. of Computer Science technical report CST-118-95, also published as LFCS-95-328},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/users/pes20/thesischarter.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/thesischarter.ps},
pscmr = {http://www.cl.cam.ac.uk/~pes20/thesiscmr.ps},
abstract = {This thesis is concerned with the algebraic theory of finite state processes. The processes we focus on are those given by a signature with prefix, summation and recursion, considered modulo strong bisimulation. We investigate their equational and implicational theories.
We first consider the existence of finite equational axiomatisations. In order to express an interesting class of equational axioms we embed the processes into a simply typed lambda calculus, allowing equation schemes with metasubstitutions to be expressed by pure equations. Two equivalences over the lambda terms are defined, an extensional equality and a higher order bisimulation. Under a restriction to first order variables these are shown to coincide and an examination of the coincidence shows that no finite equational axiomatisation of strong bisimulation can exist. We then encode the processes of Basic Process Algebra with iteration and zero (BPA_\delta^*) into this lambda calculus and show that it too is not finitely equationally axiomatisable, in sharp contrast to the extant positive result for the fragment without zero.
For the implicational theory, we show the existence of finite computable complete sets of unifiers for finite sets of equations between processes (with zero order variables). It follows that the soundness of sequents over these is decidable.
Some applications to the theories of higher order process calculi and non-well-founded sets are made explicit.},
topic = {axiomatisability}
}
@inproceedings{Sew96b,
optnote = {Sew96-brief},
author = {Peter Sewell},
title = {Design Rules and Abstractions (from branching and
real time)},
conf = {DCC96},
booktitle = {Proceedings of the
3rd Workshop on Designing Correct Circuits
(B{\aa}stad, Sweden)},
optcrossref = {},
optkey = {},
editor = {S. Singh and M. Sheeran},
optvolume = {},
optnumber = {},
series = {Electronic Workshops in Computing},
year = {1996},
optorganization = {},
publisher = {Springer-Verlag},
optaddress = {},
month = sep,
optpages = {},
note = {ISBN 3--540--76102--0. The links are to an extended version},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/users/pes20/ab.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/ab.ps},
abstract = {Three simple models of synchronous hardware are given; using linear discrete, branching discrete and branching real time. A simple notion of abstraction is introduced, motivated by the need to ultimately view such models as scientific theories that make empirical predictions. It makes the significance of design rules explicit.
Two abstractions from the branching discrete to the linear discrete model are given. They shed some light on the roles of consistency, deadlock and determinacy. The stronger of the two depends on a notion of dynamic type for processes which ensures deadlock freedom.
A reasonably strong abstraction from the branching real to the branching discrete model is given. This depends on a finer notion of type which is a reasonably physically plausible formalisation of the timing properties of certain real components.},
topic = {hardware_model_abstraction}
}
@inproceedings{Sew97a,
author = {Peter Sewell},
title = {On Implementations and Semantics of a Concurrent Programming
Language},
conf = {CONCUR 1997},
booktitle = {Concurrency Theory (Warsaw). LNCS 1243},
optcrossref = {},
optkey = {},
opteditor = {Antoni Mazurkiewicz and J{\'o}zef Winkowski},
optvolume = {},
optnumber = {},
optseries = {},
year = {1997},
optorganization = {},
publisher = {Springer-Verlag},
optaddress = {},
month = jul,
pages = {391--405},
pscmr = {http://www.cl.cam.ac.uk/~pes20/pict10-crc11ptcmr.ps},
optannote = {},
url = {https://doi.org/10.1007/3-540-63141-0},
doi = {10.1007/3-540-63141-0},
pdf = {http://www.cl.cam.ac.uk/users/pes20/pict9-crc11pt.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/pict9-crc11pt.ps},
abstract = {The concurrency theory literature contains many proposals for models of process algebras. We consider an example application of the pi-calculus, the programming language Pict of Pierce and Turner, primarily in order to see how far it is possible to argue, from facts about the application, that some model is the most appropriate. We discuss informally the sense in which the semantics of Pict relates to the behaviour of actual implementations. Based on this we give an operational model of the interactions between a Pict implementation (considered as the abstract behaviour of a C program) and its environment (modelling an operating system and user). We then give a class of abstract machines and a definition of abstract machine correctness, using an adapted notion of testing, and prove that a sample abstract machine is indeed correct. We briefly discuss the standard of correctness appropriate for program transformations and the induced precongruence. Many of the semantic choices do indeed turn out to be determined by facts about Pict.},
topic = {observational_language_semantics}
}
@techreport{Sew97c,
author = {Peter Sewell},
title = {Global/Local Subtyping for a Distributed $\pi$-calculus},
institution = {Computer Laboratory, University of Cambridge},
year = {1997},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-435},
optaddress = {},
month = aug,
note = {57pp. },
pdf = {http://www.cl.cam.ac.uk/~pes20/globallocal.ch.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/globallocal.ch.ps},
pscmr = {http://www.cl.cam.ac.uk/~pes20/globallocal.cmr.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-435.html},
abstract = {In the design of mobile agent programming languages there is a tension between the implementation cost and the expressiveness of the communication mechanisms provided. This paper gives a static type system for a distributed pi-calculus in which the input and output capabilities of channels may be either global or local. This allows compile-time optimization where possible but retains the expressiveness of channel communication. Subtyping allows all communications to be invoked uniformly. Recursive types and products are included. The distributed pi-calculus used integrates location and migration primitives from the Distributed Join Calculus with asynchronous pi communication, taking a simple reduction semantics. Some alternative calculi are discussed. },
topic = {locality_typing}
}
@article{Sew97b,
author = {Peter Sewell},
title = {Nonaxiomatisability of Equivalences over Finite State
Processes},
journal = {Annals of Pure and Applied Logic},
year = {1997},
optkey = {},
volume = {90},
optnumber = {},
month = dec,
pages = {163--191},
note = {Invited submission from LICS '94},
optannote = {},
url = {https://doi.org/10.1016/S0168-0072(97)00036-5},
doi = {10.1016/S0168-0072(97)00036-5},
pdf = {http://www.cl.cam.ac.uk/users/pes20/nonax.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/nonax.ps},
url = {http://www.sciencedirect.com/science/article/pii/S0168007297000365},
abstract = {
This paper considers the existence of finite equational axiomatisations of behavioural equivalences over a calculus of finite state processes. To express even simple properties such as mu x E = mu x E[E/x] some notation for substitutions is required. Accordingly the calculus is embedded in a simply typed lambda calculus, allowing such schemas to be expressed as equations between terms containing first order variables. A notion of first order trace congruence over such terms is introduced and used to show that no finite set of such equations is sound and complete for any reasonable equivalence finer than trace equivalence. The intermediate results are then applied to give two nonaxiomatisability results over calculi of regular expressions.},
topic = {axiomatisability}
}
@inproceedings{SWP98,
author = {Peter Sewell and Pawe{\l} T. Wojciechowski
and Benjamin C. Pierce},
title = {Location Independence for Mobile Agents},
conf = {WIPL 1998},
booktitle = {Proceedings of the Workshop on Internet Programming Languages (Chicago), in conjunction with ICCL},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {1998},
optorganization = {},
optpublisher = {},
optaddress = {},
month = may,
note = {6pp},
optpages = {6pp},
optnote = {},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/users/pes20/lima-draft.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/lima-draft.ps},
workshopurl = {http://www.math.luc.edu/iccl98/ipl-cfp.html},
topic = {nomadic_pict},
project = {http://www.cl.cam.ac.uk/~pes20/nomadicpict.html}
}
@techreport{Sew98b,
author = {Peter Sewell},
title = {From Rewrite Rules to Bisimulation Congruences},
institution = {University of Cambridge},
year = {1998},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-444},
optaddress = {},
month = jun,
note = {72pp. },
pdf = {http://www.cl.cam.ac.uk/~pes20/labels-long.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/labels-long.ps},
pscmr = {http://www.cl.cam.ac.uk/~pes20/labels-long-cmr.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-444.html},
abstract = {The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be given tractable definitions or characterisations using a labelled transition semantics. This paper considers calculi with arbitrary reduction semantics of three simple classes, firstly ground term rewriting, then left-linear term rewriting, and then a class which is essentially the action calculi lacking substantive name binding. General definitions of labelled transitions are given in each case, uniformly in the set of rewrite rules, and without requiring the prescription of additional notions of observation. They give rise to bisimulation congruences. As a test of the theory it is shown that bisimulation for a fragment of CCS is recovered. The transitions generated for a fragment of the Ambient Calculus of Cardelli and Gordon, and for SKI combinators, are also discussed briefly. },
topic = {rewrites_to_congruences}
}
@inproceedings{Sew97d,
author = {Peter Sewell},
title = {Global/Local Subtyping and Capability Inference for a Distributed $\pi$-calculus},
conf = {ICALP 1998},
booktitle = {Proceedings of the 25th International Colloquium on Automata, Languages and Programming (Aalborg). LNCS 1443},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {1998},
optorganization = {},
publisher = {Springer-Verlag},
optaddress = {},
month = jul,
pages = {695--706},
note = {The ps link is to an extended version},
optannote = {},
url = {https://doi.org/10.1007/BFb0055094},
doi = {10.1007/BFb0055094},
pdf = {http://www.cl.cam.ac.uk/users/pes20/globallocal-medium-cmr.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/globallocal-medium-cmr.ps},
abstract = {
This paper considers how locality restrictions on the use of capabilities can be enforced by a static type system. A distributed $\pi$-calculus with a simple reduction semantics is introduced, integrating location and migration primitives from the Distributed Join Calculus with asynchronous $\pi$ communication. It is given a type system in which the input and output capabilities of channels may be either global, local or absent. This allows compile-time optimization where possible but retains the expressiveness of channel communication. Subtyping allows all communications to be invoked uniformly. We show that the most local possible capabilities for internal channels can be inferred automatically.},
topic = {locality_typing}
}
@inproceedings{Sew98a,
author = {Peter Sewell},
title = {From Rewrite Rules to Bisimulation Congruences},
conf = {CONCUR 1998},
booktitle = {Proceedings of Concurrency Theory (Nice). LNCS 1466},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {1998},
optorganization = {},
publisher = {Springer-Verlag},
optaddress = {},
month = sep,
pages = {269--284},
note = {Subsumed by the TCS 2002 paper},
optannote = {},
url = {https://doi.org/10.1007/BFb0055628},
doi = {10.1007/BFb0055628},
pdf = {http://www.cl.cam.ac.uk/users/pes20/labels-medium.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/labels-medium.ps},
abstract = {The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be given tractable definitions or characterisations using a labelled transition semantics. This paper considers calculi with arbitrary reduction semantics of three simple classes, firstly ground term rewriting, then left-linear term rewriting, and then a class which is essentially the action calculi lacking substantive name binding. General definitions of labelled transitions are given in each case, uniformly in the set of rewrite rules, and without requiring the prescription of additional notions of observation. They give rise to bisimulation congruences. As a test of the theory it is shown that bisimulation for a fragment of CCS is recovered. The transitions generated for a fragment of the Ambient Calculus of Cardelli and Gordon, and for SKI combinators, are also discussed briefly.},
topic = {rewrites_to_congruences}
}
@techreport{SV99a,
author = {Peter Sewell and Jan Vitek},
title = {Secure Composition of Insecure Components},
institution = {Computer Laboratory, University of Cambridge},
year = {1999},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-463},
optaddress = {},
month = apr,
note = {44pp. },
optannote = {},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-463.html},
pdf = {http://www.cl.cam.ac.uk/~pes20/wrap-tr.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/wrap-tr.ps},
abstract = {Software systems are becoming heteroheneous: instead of a small number of large programs from well-established sources, a user’s desktop may now consist of many smaller components that interact in intricate ways. Some components will be downloaded from the network from sources that are only partially trusted. A user would like to know that a number of security properties hold, e.g. that personal data is not leaked to the net, but it is typically infaesible to verify that such components are well-behaved. Instead they must be executed in a secure environment, or wrapper, that provides fine-grain control of the allowable interactions between them, and between components and other system resources.
In this paper we study such wrappers, focussing on how they can be expressed in a way that enables their security properties to be stated and proved rigorously. We introduce a model programming language, the box-$\pi$ calculus, that supports composition of software components and the enforcement of security policies. Several example wrappers are expressed using the calculus; we explore the delicate security properties they guarantee.},
topic = {secure_encapsulation}
}
@techreport{SWP99a,
author = {Peter Sewell and Pawe{\l} T. Wojciechowski
and Benjamin C. Pierce},
title = {Location-Independent Communication for Mobile Agents: a Two-Level Architecture},
institution = {Computer Laboratory, University of Cambridge},
year = {1999},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-462},
optaddress = {},
month = apr,
note = {31pp. },
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/wipl-tr.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/wipl-tr.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-462.html},
abstract = {We study communication primitives for interaction between mobile agents. They can be classified into two groups. At a low level there are location dependent primitives that require a programmer to know the current site of a mobile agent in order to communicate with it. At a high level there are location independent primitives that allow communication with a mobile agent irrespective of its current site and of any migrations. Implementation of these requires delicate distributed infrastructure. We propose a simple calculus of agents that allows implementation of such distributed infrastructure algorithms to be expressed as encodings, or compilations, of the whole calculus into the fragment with only location dependent communication. These encodings give executable descriptions of the algorithms, providing a clean implementation strategy for prototype languages. The calculus is equipped with a precise semantics, providing a solid basis for understanding the algorithms and reasoning about their correctness and robustness. Two sample infrastructure algorithms are presented as encodings.},
topic = {nomadic_pict},
project = {http://www.cl.cam.ac.uk/~pes20/nomadicpict.html}
}
@inproceedings{SV99b,
author = {Peter Sewell and Jan Vitek},
title = {Secure Composition of Insecure Components},
conf = {CSFW 1999},
booktitle = {Proceedings of the 12th IEEE Computer Security Foundations Workshop (Mordano)},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {1999},
optorganization = {},
publisher = {IEEE Computer Society},
optaddress = {},
month = jun,
pages = {136--150},
note = {},
optannote = {},
url = {https://doi.org/10.1109/CSFW.1999.779769},
doi = {10.1109/CSFW.1999.779769},
pdf = {http://www.cl.cam.ac.uk/users/pes20/wrap-csfw.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/wrap-csfw.ps},
workshopurl = {http://www2.csl.sri.com/csfw/},
abstract = {Software systems are becoming heterogeneous: instead
of a small number of large programs from well-established
sources, a user's desktop may now consist of many smaller
components that interact in intricate ways. Some components will be downloaded from the network from sources
that are only partially trusted. A user would like to know
that a number of security properties hold, e.g. that personal
data is not leaked to the net, but it is typically infeasible to
verify that such components are well-behaved. Instead, they
must be executed in a secure environment, or wrapper, that
provides fine-grain control of the allowable interactions between them, and between components and other system resources.
In this paper we study such wrappers, focusing on how
they can be expressed in a way that enables their security
properties to be stated and proved rigorously. We introduce
a model programming language, the box-pi calculus, that
supports composition of software components and the enforcement of security policies. Several example wrappers
are expressed using the calculus; we explore the delicate
security properties they guarantee.
},
topic = {secure_encapsulation}
}
@inproceedings{WS99,
author = {Pawe{\l} T. Wojciechowski and Peter Sewell},
title = {{N}omadic {P}ict: Language and Infrastructure Design for Mobile Agents},
conf = {ASA/MA 1999},
booktitle = {Proceedings of First International Symposium on Agent Systems and Applications/Third International Symposium on Mobile Agents (Palm Springs)},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {1999},
optorganization = {},
optpublisher = {},
optaddress = {},
month = oct,
pages = {2--12},
note = {Best paper award. },
optannote = {},
url = {https://doi.org/10.1109/ASAMA.1999.805388},
doi = {10.1109/ASAMA.1999.805388},
pdf = {http://www.cl.cam.ac.uk/users/pes20/asama.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/asama.ps},
abstract = {We study the distributed infrastructures required for
location-independent communication between migrating
agents. These infrastructures are problematic: different applications may have very different patterns of migration and
communication, and require different performance and robustness properties; algorithms must be designed with these
in mind. To study this problem we introduce an agent programming language --- Nomadic Pict. It is designed to allow
infrastructure algorithms to be expressed as clearly as possible, as translations from a high-level language to a low
level. The levels are based on rigorously-defined process
calculi, they provide sharp levels of abstraction. In this paper we describe the language and use it to develop an infrastructure for an example application. The language and
examples have been implemented; we conclude with a description of the compiler and runtime.
},
topic = {nomadic_pict},
project = {http://www.cl.cam.ac.uk/~pes20/nomadicpict.html}
}
@inbook{SWP99b,
author = {Peter Sewell and Pawe{\l} T. Wojciechowski
and Benjamin C. Pierce},
title = {Location-Independent Communication for Mobile Agents: a Two-Level Architecture},
booktitle = {Internet Programming Languages, LNCS 1686},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {1999},
optorganization = {},
publisher = {Springer-Verlag},
optaddress = {},
month = oct,
pages = {1--31},
note = {},
optannote = {},
opturl = {https://doi.org/10.1007/3-540-47959-7_1},
doi = {10.1007/3-540-47959-7_1},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-462.html},
pdf = {http://www.cl.cam.ac.uk/~pes20/wipl-tr.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/wipl-tr.ps},
abstract = {We study communication primitives for interaction between mobile agents. They can be classified into two groups. At a low level there are location dependent primitives that require a programmer to know the current site of a mobile agent in order to communicate with it. At a high level there are location independent primitives that allow communication with a mobile agent irrespective of its current site and of any migrations. Implementation of these requires delicate distributed infrastructure. We propose a simple calculus of agents that allows implementation of such distributed infrastructure algorithms to be expressed as encodings, or compilations, of the whole calculus into the fragment with only location dependent communication. These encodings give executable descriptions of the algorithms, providing a clean implementation strategy for prototype languages. The calculus is equipped with a precise semantics, providing a solid basis for understanding the algorithms and reasoning about their correctness and robustness. Two sample infrastructure algorithms are presented as encodings.},
topic = {nomadic_pict},
project = {http://www.cl.cam.ac.uk/~pes20/nomadicpict.html}
}
@techreport{SV99c,
author = {Peter Sewell and Jan Vitek},
title = {Secure Composition of Untrusted Code:
Wrappers and Causality Types},
institution = {Computer Laboratory, University of Cambridge},
year = {1999},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-478},
optaddress = {},
month = nov,
note = {36pp. },
pdf = {http://www.cl.cam.ac.uk/~pes20/wraptypes-tr.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/wraptypes-tr.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-478.html},
abstract = {We consider the problem of assembling concurrent software systems from untrusted or partially trusted off-the-shelf components, using wrapper programs to encapsulate components and enforce security policies. In previous work we introduced the box-π process calculus with constrained interaction to express wrappers and discussed the rigorous formulation of their security properties. This paper addresses the verification of wrapper information flow properties. We present a novel causal type system that statically captures the allowed flows between wrapped possibly-badly-typed components; we use it to prove that a unidirectional-flow wrapper enforces a causal flow property.},
topic = {secure_encapsulation}
}
@article{WS00,
author = {Pawe{\l} T. Wojciechowski and Peter Sewell},
title = {{N}omadic {P}ict: Language and Infrastructure Design for Mobile Agents},
journal = {{IEEE} {C}oncurrency},
year = {2000},
optkey = {},
volume = {8},
number = {2},
month = {April--June},
pages = {42--52},
note = {Invited submission for ASA/MA 99. },
url = {https://doi.org/10.1109/4434.846193},
doi = {10.1109/4434.846193},
optannote = {},
abstract = {Location-independent communication between migrating agents requires a distributed infrastructure. The authors describe their Nomadic Pict distributed programming language and use it to develop an infrastructure for an example application.},
topic = {nomadic_pict},
project = {http://www.cl.cam.ac.uk/~pes20/nomadicpict.html}
}
@inproceedings{CS00,
author = {Gian Luca Cattani and Peter Sewell},
title = {Models for Name-Passing Processes: Interleaving and Causal (Extended Abstract)},
conf = {LICS 2000},
booktitle = {Proceedings of the 15th IEEE Symposium on Logic in Computer Science (Santa Barbara) },
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {2000},
optorganization = {},
optpublisher = {},
optaddress = {},
month = jun,
pages = {322--333},
note = {},
optannote = {},
url = {https://doi.org/10.1109/LICS.2000.855781},
doi = {10.1109/LICS.2000.855781},
pdf = {http://www.cl.cam.ac.uk/users/pes20/indexing.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/indexing.ps},
abstract = {We study syntax-free models for name-passing processes.
For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual $\pi$-calculus operations, defining Indexed Labelled Transition Systems. For non-interleaving causal semantics we define Indexed Labelled Asynchronous Transition Systems, smoothly generalizing both our interleaving
model and the standard Asynchronous Transition Systems
model for CCS-like calculi. In each case we relate a denotational semantics to an operational view, for bisimulation
and causal bisimulation respectively. This is a first step towards a uniform understanding of the semantics and operations of name-passing calculi.
},
topic = {models_for_name_passing}
}
@inproceedings{SV00a,
author = {Peter Sewell and Jan Vitek},
title = {Secure Composition of Untrusted Code: Wrappers and Causality Types},
conf = {CSFW 2000},
booktitle = {Proceedings of the 13th IEEE Computer Security Foundations Workshop (Cambridge)},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {2000},
optorganization = {},
publisher = {IEEE Computer Society},
optaddress = {},
month = jul,
pages = {269--284},
note = {},
optannote = {},
url = {https://doi.org/10.1109/CSFW.2000.856943},
doi = {10.1109/CSFW.2000.856943},
pdf = {http://www.cl.cam.ac.uk/users/pes20/wraptypes.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/wraptypes.ps},
abstract = {
We consider the problem of assembling concurrent software systems from untrusted or partially trusted off-the-shelf components, using wrapper programs to encapsulate
components and enforce security policies. In previous work
we introduced the box-$\pi$ process calculus with constrained
interaction to express wrappers and discussed the rigorous
formulation of their security properties. This paper addresses the verification of wrapper information flow properties. We present a novel causal type system that statically captures the allowed flows between wrapped possiblybadly-typed components; we use it to prove that an example
unidirectional-flow wrapper enforces a causal flow property.
},
topic = {secure_encapsulation}
}
@techreport{Sew00pi-tr,
author = {Peter Sewell},
title = {Applied $\pi$ -- A Brief Tutorial},
institution = {Computer Laboratory, University of Cambridge},
year = {2000},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-498},
optaddress = {},
month = aug,
note = {65pp. },
optannote = {},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-498.html},
pdf = {http://www.cl.cam.ac.uk/~pes20/apppi.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/apppi.ps},
abstract = {This note provides a brief introduction to $\pi$-calculi and their application to concurrent and distributed programming. Chapter 1 introduces a simple $\pi$-calculus and discusses the choice of primitives, operational semantics (in terms of reductions and of indexed early labelled transitions), operational equivalences, Pict-style programming and typing. Chapter 2 goes on to discuss the application of these ideas to distributed systems, looking informally at the design of distributed $\pi$-calculi with grouping and interaction primitives. Chapter 3 returns to typing, giving precise definitions for a simple type system and soundness results for the labelled transition semantics. Finally, Chapters 4 and 5 provide a model development of the metatheory, giving first an outline and then detailed proofs of the results stated earlier. The note can be read in the partial order 1.(2+3+4.5).},
topic = {pi_tutorial}
}
@techreport{Sew00,
author = {Peter Sewell},
title = {Modules, Abstract Types, and Distributed Versioning},
institution = {University of Cambridge},
year = {2000},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-506},
optaddress = {},
month = sep,
note = {46pp. },
optannote = {},
errata = {http://www.cl.cam.ac.uk/~pes20/versions-errata.txt},
ps = {http://www.cl.cam.ac.uk/~pes20/versions-tr.ps},
pdf = {http://www.cl.cam.ac.uk/~pes20/versions-tr.pdf},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-506.html},
abstract = {In a wide-area distributed system it is often impractical to synchronise software updates, so one must deal with many coexisting versions. We study static typing support for modular wide-area programming, modelling separate compilation/linking and execution of programs that interact along typed channels. Interaction may involve communication of values of abstract types; we provide the developer with fine-grain versioning control of these types to support interoperation of old and new code. The system makes use of a second-class module system with singleton kinds; we give a novel operational semantics for separate compilation/linking and execution and prove soundness.},
topic = {distributed_types}
}
@techreport{CS00b,
author = {Gian Luca Cattani and Peter Sewell},
title = {Models for Name-Passing Processes: Interleaving and Causal},
institution = {Computer Laboratory, University of Cambridge},
year = {2000},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-505},
optaddress = {},
month = sep,
note = {42pp. },
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/indexing-tr.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/indexing-tr.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-505.html},
abstract = {We study syntax-free models for name-passing processes. For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual $\pi$-calculus operations, defining Indexed Labelled Transition Systems. For noninterleaving causal semantics we define Indexed Labelled Asynchronous Transition Systems, smoothly generalizing both our interleaving model and the standard Asynchronous Transition Systems model for CCS-like calculi. In each case we relate a denotational semantics to an operational view, for bisimulation and causal bisimulation respectively. We establish completeness properties of, and adjunctions between, categories of the two models. Alternative indexing structures and possible applications are also discussed. These are first steps towards a uniform understanding of the semantics and operations of name-passing calculi.},
topic = {models_for_name_passing}
}
@inproceedings{Sew01a,
author = {Peter Sewell},
title = {Modules, Abstract Types, and Distributed Versioning},
conf = {POPL 2001},
booktitle = {Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (London)},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {2001},
optorganization = {},
optpublisher = {},
optaddress = {},
month = jan,
pages = {236--247},
note = {},
optannote = {},
errata = {http://www.cl.cam.ac.uk/~pes20/versions-errata.txt},
url = {http://doi.acm.org/10.1145/360204.360225},
doi = {10.1145/360204.360225},
pdf = {http://www.cl.cam.ac.uk/users/pes20/versions-popl.pdf},
abstract = {
In a wide-area distributed system it is often impractical to
synchronise software updates, so one must deal with many
coexisting versions. We study static typing support for modular wide-area programming, modelling separate compilation/linking and execution of programs that interact along
typed channels. Interaction may involve communication of
values of abstract types; we provide the developer with finegrain versioning control of these types to support interoperation of old and new code. The system makes use of a
second-class module system with singleton kinds; we give a
novel operational semantics for separate compilation/linking
and execution and prove soundness.
},
topic = {distributed_types}
}
@inproceedings{US01,
author = {Asis Unyapoth and Peter Sewell},
title = {Nomadic {P}ict: Correct Communication Infrastructure for Mobile Computation},
conf = {POPL 2001},
booktitle = {Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (London)},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {2001},
optorganization = {},
optpublisher = {},
optaddress = {},
month = jan,
pages = {116--127},
note = {},
optannote = {},
url = {http://doi.acm.org/10.1145/360204.360214},
doi = {10.1145/360204.360214},
pdf = {http://www.cl.cam.ac.uk/users/pes20/nproofs-popl.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/nproofs-popl.ps},
abstract = {This paper addresses the design and verification of infrastructure for mobile computation. In particular, we
study language primitives for communication between mobile agents. They can be classified into two groups. At a low
level there are location dependent primitives that require a
programmer to know the current site of a mobile agent in
order to communicate with it. At a high level there are
location independent primitives that allow communication
with a mobile agent irrespective of any migrations. Implementation of the high level requires delicate distributed infrastructure algorithms. In earlier work with
Wojciechowski
and Pierce we made the two levels precise as process calculi, allowing such algorithms to be expressed as encodings
of the high level into the low level; we built Nomadic Pict,
a distributed programming language for experimenting with
such encodings. In this paper we turn to semantics, giving
a definition of the core language and proving correctness of
an example infrastructure. This requires novel techniques:
we develop equivalences that take migration into account,
and reasoning principles for agents that are temporarily immobile (eg. waiting on
a lock elsewhere in the system).
},
topic = {nomadic_pict},
project = {http://www.cl.cam.ac.uk/~pes20/nomadicpict.html}
}
@techreport{SSW01b,
author = {Andrei Serjantov and Peter Sewell and Keith Wansbrough},
title = {The {UDP} Calculus: Rigorous Semantics for Real Networking},
institution = {Computer Laboratory, University of Cambridge},
year = {2001},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-515},
optaddress = {},
month = jul,
note = {iv+70pp. },
pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/udp-long.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/Netsem/udp-long.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-515.html},
abstract = {Network programming is notoriously hard to understand: one has to deal with a variety of protocols (IP, ICMP, UDP, TCP, etc.), concurrency, packet loss, host failure, timeouts, the complex sockets interface to the protocols, and subtle protability issues. Moreover, the behavioural properties of operating systems and the network are not well documented.
A few of these issues have been addressed in the process calculus and distributed algorithm communities, but there remains a wide gulf between what has been captured in semantic models and what is required for a precise understanding of the behaviour of practical distributed programs that use these protocols.
In this paper we demonstrate (in a preliminary way) that the gulf can be bridged. We give an operational model for socket programming with a substantial fraction of UDP and ICMP, including loss and failure. The model has been validated by experiment against actual systems. It is not tied to a particular programming language, but can be used with any language equipped with an operational semantics for system calls – here we give such a language binding for an OCaml fragment. We illustrate the model with a few small network programs.
},
topic = {netsem},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}
@inproceedings{SSW01a,
author = {Andrei Serjantov and Peter Sewell and Keith Wansbrough},
title = {The {UDP} Calculus: Rigorous Semantics for Real Networking},
conf = {TACS 2001},
booktitle = {Proceedings of Theoretical Aspects of Computer Software (Sendai), LNCS 2215},
optcrossref = {},
optkey = {},
pages = {535--559},
year = {2001},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = oct,
optorganization = {},
optpublisher = {},
note = {},
optannote = {},
url = {https://doi.org/10.1007/3-540-45500-0_27},
doi = {10.1007/3-540-45500-0_27},
pdf = {http://www.cl.cam.ac.uk/users/pes20/Netsem/udp-short.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/Netsem/udp-short.ps},
abstract = {Network programming is notoriously hard to understand:
one has to deal with a variety of protocols (IP, ICMP, UDP, TCP etc),
concurrency, packet loss, host failure, timeouts, the complex sockets interface
to the protocols, and subtle portability issues. Moreover, the behavioural prope
rties of operating systems and the network are not well
documented.
A few of these issues have been addressed in the process calculus and
distributed algorithm communities, but there remains a wide gulf between what ha
s been captured in semantic models and what is required
for a precise understanding of the behaviour of practical distributed programs t
hat use these protocols.
In this paper we demonstrate (in a preliminary way) that the gulf can
be bridged. We give an operational model for socket programming with
a substantial fraction of UDP and ICMP, including loss and failure. The
model has been validated by experiment against actual systems. It is not
tied to a particular programming language, but can be used with any
language equipped with an operational semantics for system calls - here
we give such a language binding for an OCaml fragment. We illustrate
the model with a few small network programs.
},
topic = {netsem},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}
@inbook{Sew00pi,
author = {Peter Sewell},
title = {Chapter 9, {P}i {C}alculus, in the book {F}ormal {M}ethods for {D}istributed {P}rocessing, {A} {S}urvey of {O}bject {O}riented
{A}pproaches, edited by {H}oward {B}owman and {J}ohn {D}errick},
publisher = {Cambridge University Press},
year = {2001},
optkey = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
optedition = {},
month = dec,
pages = {177--197},
opttype = {},
note = {ISBN 0521771846. The links are to the TR498 extended version of the book chapter.},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/apppi.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/apppi.ps},
abstract = {This note provides a brief introduction to $\pi$-calculi and their application to concurrent and distributed programming. Chapter 1 introduces a simple $\pi$-calculus and discusses the choice of primitives, operational semantics (in terms of reductions and of indexed early labelled transitions), operational equivalences, Pict-style programming and typing. Chapter 2 goes on to discuss the application of these ideas to distributed systems, looking informally at the design of distributed $\pi$-calculi with grouping and interaction primitives. Chapter 3 returns to typing, giving precise definitions for a simple type system and soundness results for the labelled transition semantics. Finally, Chapters 4 and 5 provide a model development of the metatheory, giving first an outline and then detailed proofs of the results stated earlier. The note can be read in the partial order 1.(2+3+4.5).},
topic = {pi_tutorial}
}
@article{Sew99a,
author = {Peter Sewell},
title = {From Rewrite Rules to Bisimulation Congruences},
journal = {Theoretical Computer Science},
year = {2002},
optkey = {},
volume = 274,
number = {1--2},
month = mar,
pages = {183--230},
note = {Invited submission for a CONCUR 98 special issue. },
optannote = {},
url = {http://dx.doi.org/10.1016/S0304-3975(00)00309-1},
doi = {10.1016/S0304-3975(00)00309-1},
pdf = {http://www.cl.cam.ac.uk/users/pes20/labels-tcs-final.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/labels-tcs-final.ps},
abstract = {The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be given tractable definitions or characterisations using a labelled transition semantics. This paper considers calculi with arbitrary reduction semantics of three simple classes, firstly ground term rewriting, then left-linear term rewriting, and then a class which is essentially the action calculi lacking substantive name binding. General definitions of labelled transitions are given in each case, uniformly in the set of rewrite rules, and without requiring the prescription of additional notions of observation. They give rise to bisimulation congruences. As a test of the theory it is shown that bisimulation for a fragment of CCS is recovered. The transitions generated for a fragment of the Ambient Calculus of Cardelli and Gordon, and for SKI combinators, are also discussed briefly.},
topic = {rewrites_to_congruences}
}
@inproceedings{WNSS01,
author = {Keith Wansbrough and Michael Norrish and Peter Sewell and Andrei Serjantov},
title = {Timing {UDP}: mechanized semantics for sockets, threads and failures},
conf = {ESOP 2002},
booktitle = {Proceedings of the 11th European Symposium on Programming (Grenoble), LNCS 2305},
optcrossref = {},
optkey = {},
pages = {278--294},
year = {2002},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = apr,
optorganization = {},
optpublisher = {},
note = {},
optannote = {},
url = {https://doi.org/10.1007/3-540-45927-8_20},
doi = {10.1007/3-540-45927-8_20},
ps = {http://www.cl.cam.ac.uk/users/pes20/Netsem/timing-udp-a4.ps},
pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/timing-udp-a4.pdf},
abstract = {This paper studies the semantics of failure in distributed
programming. We present a semantic model for distributed programs
that use the standard sockets interface; it covers message loss, host failure
and temporary disconnection, and supports reasoning about distributed
infrastructure. We consider interaction via the UDP and ICMP protocols.
To do this, it has been necessary to: $\bullet$ construct an experimentallyvalidated
post-hoc specification of the UDP/ICMP sockets interface;
$\bullet$ develop a timed operational semantics with threads, as such programs
are typically multithreaded and depend on timeouts; $\bullet$ model the behaviour
of partial systems, making explicit the interactions that the infrastructure
offers to applications; $\bullet$ integrate the above with semantics
for an executable fragment of a programming language (OCaml) with OS
library primitives; and $\bullet$ use tool support to manage complexity, mechanizing
the model with the HOL theorem prover. We illustrate the whole
with a module providing na¨ıve heartbeat failure detection.},
topic = {netsem},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}
@inproceedings{NSW02,
author = {Michael Norrish and Peter Sewell and Keith Wansbrough},
title = {Rigour is good for you, and feasible: reflections on formal treatments of {C} and {UDP} sockets. },
conf = {SIGOPS EW 2002},
booktitle = {Proceedings of the 10th ACM SIGOPS European Workshop (Saint-Emilion)},
optcrossref = {},
optkey = {},
pages = {49--53},
year = {2002},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = sep,
optorganization = {},
optpublisher = {},
note = {},
optannote = {},
url = {http://doi.acm.org/10.1145/1133373.1133383},
doi = {10.1145/1133373.1133383},
pdf = {http://www.cl.cam.ac.uk/users/pes20/Netsem/sigops-ew2002.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/Netsem/sigops-ew2002.ps},
abstract = {We summarise two projects that formalised complex real
world systems: UDP and its sockets API, and the C programming language. We describe their goals and the techniques used in both. We conclude by discussing how such
techniques might be applied to other system software and
by describing the benefits this may bring.},
topic = {netsem},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}
@article{SV-jcs,
author = {Peter Sewell and Jan Vitek},
title = {Secure Composition of Untrusted Code: Box-$\pi$, Wrappers and Causality Types},
journal = {Journal of Computer Security},
year = {2003},
optkey = {},
volume = {11},
number = {2},
optmonth = {},
pages = {135-188},
note = {Invited submission for a CSFW 00 special issue.},
optannote = {},
url = {http://content.iospress.com/articles/journal-of-computer-security/jcs165},
pdf = {http://www.cl.cam.ac.uk/users/pes20/wrapall.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/wrapall.ps},
abstract = {Software systems are becoming heterogeneous: instead of a small number of
large programs from well-established sources, a user's desktop may now consist
of many smaller components that interact in intricate ways. Some components
will be downloaded from the network from sources that are only partially trusted.
A user would like to know that a number of security properties hold, e.g.~that
personal data is not leaked to the net, but it is typically infeasible to verify that
such components are well-behaved. Instead, they must be executed in a secure
environment that provides fine-grain control of the allowable interactions between
them, and between components and other system resources.
In this paper, we consider the problem of assembling concurrent software systems from untrusted or partially trusted off-the-shelf components, using wrapper
programs to encapsulate components and enforce security policies. We introduce
a model programming language, the box-ss calculus, that supports composition of
software components and the enforcement of information flow security policies.
Several example wrappers are expressed using the calculus; we explore the delicate security properties they guarantee. We present a novel causal type system
that statically captures the allowed flows between wrapped possibly-badly-typed
components; we use it to prove that an example ordered pipeline wrapper enforces
a causal flow property.
},
topic = {secure_encapsulation}
}
@techreport{BS03,
author = {G. M. Bierman and P. Sewell},
title = {Iota: A concurrent {XML} scripting language with applications to Home Area Networking},
institution = {Computer Laboratory, University of Cambridge},
year = {2003},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-557},
optaddress = {},
month = jan,
note = {32pp. },
pdf = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-557.pdf},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-557.html},
abstract = {Iota is a small and simple concurrent language that provides native support for
functional XML computation and for typed channel-based communication. It has
been designed as a domain-specific language to express device behaviour within the
context of Home Area Networking.
In this paper we describe Iota, explaining its novel treatment of XML and describing
its type system and operational semantics. We give a number of examples
including Iota code to program Universal Plug 'n' Play (UPnP) devices.},
topic = {iota}
}
@inproceedings{BHSS03,
author = {Gavin Bierman and Michael Hicks and Peter Sewell and Gareth Stoyle},
title = {Formalizing Dynamic Software Updating},
conf = {USE 2003},
booktitle = {Proceedings of the Second International Workshop on Unanticipated Software
Evolution (Warsaw), in conjunction with ETAPS},
optcrossref = {},
optkey = {},
optpages = {},
year = {2003},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = apr,
optorganization = {},
optpublisher = {},
note = {17pp},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/formalUpdate.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/formalUpdate.ps},
abstract = {Dynamic software updating (DSU) enables running programs to be
updated with new code and data without interrupting their execution. A
number of DSU systems have been designed, but there is still little rigorous und
erstanding of how to use DSU technology so that updates are
safe. As a first step in this direction, we introduce a small update calculus
with a precise mathematical semantics. The calculus is formulated as an
extension of a typed lambda calculus, and supports updating technology
similar to that of the programming language Erlang [2]. Our goal is to
provide a simple yet expressive foundation for reasoning about dynamically updat
eable software. In this paper, we present the details of the
calculus, give some examples of its expressive power, and discuss how it
might be used or extended to guarantee safety properties.},
topic = {dynamic_update}
}
@techreport{LPSW03-tr,
author = {James Leifer and Gilles Peskine and Peter Sewell and Keith Wansbrough},
title = {Global abstraction-safe marshalling with hash types},
institution = {University of Cambridge Computer Laboratory},
year = {2003},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-569},
optaddress = {},
month = jun,
note = {Also published as INRIA Rocquencourt report RR-4851. 86pp.},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-569.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/hashtypes.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-569.html},
abstract = {Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent stores. In this paper we combine the two, developing compile-time and run-time semantics for marshalling, that guarantee abstraction-safety between separately-built programs.
We obtain a namespace for abstract types that is global, ie meaningful between programs, by hashing module declarations. We examine the scenarios in which values of abstract types are communicated from one program to another, and ensure, by constructing hashes appropriately, that the dynamic and static notions of type equality mirror each other. We use singleton kinds to express abstraction in the static semantics; abstraction is tracked in the dynamic semantics by coloured brackets. These allow us to prove preservation, erasure, and coincidence results. We argue that our proposal is a good basis for extensions to existing ML-like languages, pragmatically straightforward for language users and for implementors.},
topic = {distributed_types}
}
@inproceedings{LPSW03,
author = {James Leifer and Gilles Peskine and Peter Sewell and Keith Wansbrough},
title = {Global abstraction-safe marshalling with hash types},
conf = {ICFP 2003},
booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (Uppsala)},
optcrossref = {},
optkey = {},
pages = {87--98},
year = {2003},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = aug,
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
url = {http://doi.acm.org/10.1145/944746.944714},
doi = {10.1145/944746.944714},
pdf = {http://www.cl.cam.ac.uk/~pes20/hashtypes.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/hashtypes.ps},
abstract = {Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or
persistent stores. In this paper we combine the two, developing
compile-time and run-time semantics for marshalling, that guarantee abstraction-safety between separately-built programs.
We obtain a namespace for abstract types that is global, i.e.
meaningful between programs, by hashing module declarations.
We examine the scenarios in which values of abstract types are
communicated from one program to another, and ensure, by constructing hashes appropriately, that the dynamic and static notions
of type equality mirror each other. We use singleton kinds to express abstraction in the static semantics; abstraction is tracked in
the dynamic semantics by coloured brackets. These allow us to
prove preservation, erasure, and coincidence results. We argue that
our proposal is a good basis for extensions to existing ML-like languages, pragmatically straightforward for language users and for
implementors.},
topic = {distributed_types}
}
@inproceedings{BHSSW03,
author = {Gavin Bierman and Michael Hicks and Peter Sewell and Gareth Stoyle and Keith Wansbrough},
title = {Dynamic Rebinding for Marshalling and Update, with Destruct-time lambda},
conf = {ICFP 2003},
booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (Uppsala)},
optcrossref = {},
optkey = {},
pages = {99--110},
year = {2003},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = aug,
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
url = {http://doi.acm.org/10.1145/944746.944715},
doi = {10.1145/944746.944715},
pdf = {http://www.cl.cam.ac.uk/~pes20/dynbind2-short.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/dynbind2-short.ps},
abstract = {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, for example 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 this paper we adopt a foundational approach, developing core dynamic rebinding mechanisms as extensions to simply-typed call-by-value lambda-calculus. To do so we must first explore refinements of the call-by-value reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduce redex-time and destruct-time strategies.
The latter forms the basis for a lambda-marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically-typed. We sketch an extension of lambda-marsh with concurrency and communication, giving examples showing how
wrappers for encapsulating untrusted code can be expressed. Finally, we show 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 updating of
running code. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding
requirements.
},
topic = {distributed_types_and_update}
}
@inproceedings{SS03,
author = {Andrei Serjantov and Peter Sewell},
title = {Passive Attack Analysis for Connection-Based Anonymity Systems},
conf = {ESORICS 2003},
booktitle = {Proceedings of the 8th European Symposium on Research in Computer Security (Gj{\o}vik), LNCS 2808},
optcrossref = {},
optkey = {},
pages = {116--131},
year = {2003},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = oct,
optorganization = {},
optpublisher = {},
note = {},
optannote = {},
url = {https://doi.org/10.1007/s10207-004-0059-3},
doi = {10.1007/s10207-004-0059-3},
pdf = {http://www.cl.cam.ac.uk/users/pes20/conn_sys.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/conn_sys.ps},
abstract = {In this paper we consider low latency connection-based anonymity system which
can be used for applications like web browsing or SSH. Although several such sys
tems have been designed and built, their anonymity has so far not been adequatel
y
evaluated.
We analyse the anonymity of connection-based systems against passive adversaries. We give a precise description of two attacks, evaluate their effectiveness,
and calculate the amount of traffic necessary to render the attacks useless.
},
topic = {anonymity}
}
@techreport{BHSSW04-tr,
author = {Gavin Bierman and Michael Hicks and Peter Sewell and Gareth Stoyle and Keith Wansbrough},
title = {Dynamic Rebinding for Marshalling and Update, with Destruct-time $\lambda$},
institution = {University of Cambridge Computer Laboratory},
year = {2004},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-568},
optaddress = {},
month = feb,
note = {85pp},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/UCAM-CL-TR-568.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/dynbind2-long-draft.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-568.html},
abstract = {
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, for example 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 this paper we adopt a foundational approach, developing core dynamic rebinding mechanisms as extensions to the simply-typed call-by-value λ-calculus. To do so we must first explore refinements of the call-by-value reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduce redex-time and destruct-time strategies. The latter forms the basis for a λ-marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically-typed. We sketch an extension of λ-marsh with concurrency and communication, giving examples showing how wrappers for encapsulating untrusted code can be expressed. Finally, we show that a high-level semantics for dynamic updating can also be based on the destruct-time strategy, defining a λ-update calculus with simple primitives to provide type-safe updating of running code. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding requirements.
},
topic = {distributed_types_and_update}
}
@inproceedings{LNSW04,
author = {James Leifer and Michael Norrish and Peter Sewell and Keith Wansbrough},
title = {Acute and {TCP}: specifying and developing abstractions for global computation},
optcrossref = {},
optkey = {},
conf = {APPSEM II Workshop, 2004},
booktitle = {Proceedings of the APPSEM II Workshop (Tallinn)},
pages = {},
year = {2004},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = apr,
optorganization = {},
optpublisher = {},
note = {2pp},
optannote = {},
topic = {distributed_types}
}
@article{CS00c,
author = {Gian Luca Cattani and Peter Sewell},
title = {Models for Name-Passing Processes: Interleaving and Causal},
journal = {Information and Computation},
year = {2004},
optkey = {},
volume = {190},
number = {2},
pages = {136--178},
month = may,
optnote = {},
optannote = {},
url = {https://doi.org/10.1016/j.ic.2003.12.003},
doi = {10.1016/j.ic.2003.12.003},
abstract = {We study syntax-free models for name-passing processes. For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual π-calculus operations, defining Indexed Labelled Transition Systems. For non-interleaving causal semantics we define Indexed Labelled Asynchronous Transition Systems, smoothly generalizing both our interleaving model and the standard Asynchronous Transition Systems model for CCS-like calculi. In each case we relate a denotational semantics to an operational view, for bisimulation and causal bisimulation respectively. We establish completeness properties of, and adjunctions between, categories of the two models. Alternative indexing structures and possible applications are also discussed. These are first steps towards a uniform understanding of the semantics and operations of name-passing calculi.},
topic = {models_for_name_passing}
}
@inproceedings{BS04a,
author = {Moritz Y. Becker and Peter Sewell},
title = {Cassandra: Distributed Access Control Policies with Tunable Expressiveness},
optcrossref = {},
optkey = {},
conf = {POLICY 2004},
booktitle = {Proceedings of the 5th IEEE International Workshop on Policies for Distributed Systems and Networks (Yorktown Heights)},
optpages = {},
year = {2004},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = jun,
optorganization = {},
optpublisher = {},
optannote = {},
note = {},
url = {https://doi.org/10.1109/POLICY.2004.1309162},
doi = {10.1109/POLICY.2004.1309162},
pdf = {http://www.cl.cam.ac.uk/users/pes20/policy-policy04.pdf},
abstract = {
We study the specification of access control policy in
large-scale distributed systems. Our work on real-world
policies has shown that standard policy idioms such as role
hierarchy or role delegation occur in practice in many subtle variants. A policy specification language should therefore be able to express this variety of features smoothly,
rather than add them as specific features in an ad hoc way,
as is the case in many existing languages.
We present Cassandra, a role-based trust management
system with an elegant and readable policy specification
language based on Datalog with constraints. The expressiveness (and computational complexity) of the language
can be adjusted by choosing an appropriate constraint domain. With just five special predicates, we can easily express a wide range of policies including role hierarchy,
role delegation, separation of duties, cascading revocation, automatic credential discovery and trust negotiation.
Cassandra has a formal semantics for query evaluation and
for the access control enforcement engine. We use a goal-oriented distributed policy evaluation algorithm that is efficient and guarantees termination. Initial performance results for our prototype implementation have been promising.
},
topic = {security_policy}
}
@inproceedings{BS04b,
author = {Moritz Y. Becker and Peter Sewell},
title = {Cassandra: Flexible Trust Management, Applied to Electronic Health Records},
optcrossref = {},
optkey = {},
conf = {CSFW 2004},
booktitle = {Proceedings of the 17th IEEE Computer Security Foundations Workshop (Asilomar)},
pages = {139--154},
year = {2004},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = jun,
optorganization = {},
optpublisher = {},
optnote = {For more details, including the complete example policy, see \url{http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-628.html} and Moritz Becker's PhD Thesis at \url{http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-648.html}.},
optannote = {},
url = {http://doi.ieeecomputersociety.org/10.1109/CSFW.2004.7},
doi = {10.1109/CSFW.2004.7},
pdf = {http://www.cl.cam.ac.uk/users/pes20/policy-csfw04.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/policy-csfw04.ps},
abstract = {We study the specification of access control policy in large-scale distributed systems. We present
Cassandra, a
language and system for expressing policy, and the results of a substantial case study, a security policy for a national
Electronic Health Record system, based on the requirements
for the ongoing UK National Health Service procurementexercise.
Cassandra policies 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.
Cassandra is
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 thatis 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 results suggest that the per-formance should be acceptable.
},
topic = {security_policy}
}
@techreport{SLWAZHV04,
author = {Peter Sewell and
James J. Leifer and
Keith Wansbrough and
Mair Allen-Williams and
Zappa Nardelli, Francesco and
Pierre Habouzit and
Viktor Vafeiadis},
title = {Acute: High-level programming language design for distributed
computation. Design rationale and language definition},
institution = {University of Cambridge Computer Laboratory},
year = {2004},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-605},
optaddress = {},
month = oct,
note = {Also published as INRIA RR-5329. 193pp},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/acute/UCAM-CL-TR-605.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/acute/acute2-long.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-605.html},
abstract = {
This paper studies key issues for distributed programming in high-level languages. We discuss the design space and describe an experimental language, Acute, which we have defined and implemented.
Acute extends an OCaml core to support distributed development, deployment, and execution, allowing type-safe interaction between separately-built programs. It is expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs, disentangling the language runtime from communication.
This requires a synthesis of novel and existing features:
(1) type-safe marshalling of values between programs;
(2) dynamic loading and controlled rebinding to local resources;
(3) modules and abstract types with abstraction boundaries that are respected by interaction;
(4) global names, generated either freshly or based on module hashes: at the type level, as runtime names for abstract types; and at the term level, as channel names and other interaction handles;
(5) versions and version constraints, integrated with type identity;
(6) local concurrency and thread thunkification; and
(7) second-order polymorphism with a namecase construct.
We deal with the interplay among these features and the core, and develop a semantic definition that tracks abstraction boundaries, global names, and hashes throughout compilation and execution, but which still admits an efficient implementation strategy.
},
topic = {distributed_types},
project = {http://www.cl.cam.ac.uk/~pes20/acute/}
}
@inproceedings{SHBSN05,
author = {Gareth Stoyle and
Michael Hicks and
Gavin Bierman and
Peter Sewell and
Iulian Neamtiu},
title = {\textit{Mutatis Mutandis}: Safe and Predictable Dynamic Software Updating},
optcrossref = {},
optkey = {},
conf = {POPL 2005},
booktitle = {Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Long Beach)},
pages = {183--194},
year = {2005},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = jan,
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
url = {http://doi.acm.org/10.1145/1255450.1255455},
doi = {10.1145/1255450.1255455},
pdf = {http://www.cl.cam.ac.uk/users/pes20/update-popl-2005.pdf},
abstract = {
Dynamic software updates can be used to fix bugs or add features
to a running program without downtime. Essential for some applications and convenient for others, low-level dynamic updating has
been used for many years. Perhaps surprisingly, there is little high-level understanding or language support to help programmers write
dynamic updates effectively.
To bridge this gap, we present Proteus, a core calculus for dynamic software updating in C-like languages that is flexible, safe,
and predictable. Proteus supports dynamic updates to functions
(even active ones), to named types and to data, allowing on-line
evolution to match source-code evolution as we have observed it
in practice. We ensure updates are type-safe by checking for a
property we call ``con-freeness'' for updated types t at the point
of update. This means that non-updated code will not use t concretely beyond that point (concrete usages are via explicit coercions) and thus t's representation can safely change. We show how
con-freeness can be enforced dynamically for a particular program
state. We additionally define a novel and efficient static updateability analysis to establish con-freeness statically, and can thus automatically infer program points at which all future (well-formed)
updates will be type-safe. We have implemented our analysis for C
and tested it on several well-known programs.
},
topic = {dynamic_update}
}
@techreport{TCP:tr,
optkey = {},
author = {Steven Bishop and Matthew Fairbairn and Michael Norrish and
Peter Sewell and Michael Smith and Keith Wansbrough},
title = {{TCP}, {UDP}, and {S}ockets: rigorous and experimentally-validated
behavioural specification. {V}olume 1: Overview},
institution = {Computer Laboratory, University of Cambridge},
number = {UCAM-CL-TR-624},
note = {88pp},
optnote = {Available at \url{http://www.cl.cam.ac.uk/users/pes20/Netsem/}},
month = mar,
year = {2005},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/tr.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/Netsem/tr.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-624.html},
abstract = {
We have developed a mathematically rigorous and experimentally-validated post-hoc specification of the behaviour of TCP, UDP, and the Sockets API. It characterises the API and network-interface interactions of a host, using operational semantics in the higher-order logic of the HOL automated proof assistant. The specification is detailed, covering almost all the information of the real-world communications: it is in terms of individual TCP segments and UDP datagrams, though it abstracts from the internals of IP. It has broad coverage, dealing with arbitrary API call sequences and incoming messages, not just some well-behaved usage. It is also accurate, closely based on the de facto standard of (three of) the widely-deployed implementations. To ensure this we have adopted a novel experimental semantics approach, developing test generation tools and symbolic higher-order-logic model checking techniques that let us validate the specification directly against several thousand traces captured from the implementations.
The resulting specification, which is annotated for the non-HOL-specialist reader, may be useful as an informal reference for TCP/IP stack implementors and Sockets API users, supplementing the existing informal standards and texts. It can also provide a basis for high-fidelity automated testing of future implementations, and a basis for design and formal proof of higher-level communication layers. More generally, the work demonstrates that it is feasible to carry out similar rigorous specification work at design-time for new protocols. We discuss how such a design-for-test approach should influence protocol development, leading to protocol specifications that are both unambiguous and clear, and to high-quality implementations that can be tested directly against those specifications.
This document (Volume 1) gives an overview of the project, discussing the goals and techniques and giving an introduction to the specification. The specification itself is given in the companion Volume 2 (UCAM-CL-TR-625), which is automatically typeset from the (extensively annotated) HOL source. As far as possible we have tried to make the work accessible to four groups of intended readers: workers in networking (implementors of TCP/IP stacks, and designers of new protocols); in distributed systems (implementors of software above the Sockets API); in distributed algorithms (for whom this may make it possible to prove properties about executable implementations of those algorithms); and in semantics and automated reasoning.},
topic = {netsem},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}
@techreport{TCP:spec,
optkey = {},
author = {Steven Bishop and Matthew Fairbairn and Michael Norrish and
Peter Sewell and Michael Smith and Keith Wansbrough},
title = {{TCP}, {UDP}, and {S}ockets: rigorous and experimentally-validated
behavioural specification. {V}olume 2: The
Specification.},
institution = {Computer Laboratory, University of Cambridge},
number = {UCAM-CL-TR-625},
note = {386pp},
optnote = { Available at \url{http://www.cl.cam.ac.uk/users/pes20/Netsem/}},
month = mar,
year = {2005},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/alldoc.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/Netsem/alldoc.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-625.html},
abstract = {See Volume 1 (UCAM-CL-TR-624).},
topic = {netsem},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}
@inproceedings{poplmark,
author = {Brian E. Aydemir and Aaron Bohannon and Matthew Fairbairn
and J. Nathan Foster and Benjamin C. Pierce and Peter
Sewell and Dimitrios Vytiniotis and Geoffrey Washburn and
Stephanie Weirich and Steve Zdancewic},
title = {Mechanized metatheory for the masses: {T}he {POPL}mark
{C}hallenge},
year = 2005,
month = aug,
optcrossref = {},
optkey = {},
conf = {TPHOLs 2005},
booktitle = {Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (Oxford), LNCS 3603},
pages = {50--65},
optyear = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
optmonth = {},
optorganization = {},
optpublisher = {},
note = {},
optannote = {},
optpdf = {http://www.cis.upenn.edu/group/proj/plclub/mmm/poplmark/poplmark.pdf},
project = {http://www.seas.upenn.edu/~plclub/poplmark/},
url = {https://doi.org/10.1007/11541868_4},
doi = {10.1007/11541868_4},
pdf = {http://www.cl.cam.ac.uk/~pes20/poplmark.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/poplmark.ps},
abstract = {
How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs?
We propose an initial set of benchmarks for measuring progress in this
area. Based on the metatheory of System F<:, a typed lambda-calculus
with second-order polymorphism, subtyping, and records, these benchmarks embody many aspects of programming languages that are challenging to formalize: variable binding at both the term and type levels,
syntactic forms with variable numbers of components (including binders),
and proofs demanding complex induction principles. We hope that these
benchmarks will help clarify the current state of the art, provide a basis
for comparing competing technologies, and motivate further research.
},
topic = {poplmark}
}
@inproceedings{TCP:paper,
optkey = {},
author = {Steven Bishop and Matthew Fairbairn and Michael Norrish and
Peter Sewell and Michael Smith and Keith Wansbrough},
title = {Rigorous specification and conformance testing techniques for network protocols, as applied to {TCP}, {UDP}, and {S}ockets},
year = {2005},
optnote = {12pp},
optcrossref = {},
optkey = {},
conf = {SIGCOMM 2005},
booktitle = {Proceedings of the ACM Conference on Computer Communications (Philadelphia), \emph{published as Vol.~35, No.~4 of} {{Computer Communication Review}}},
pages = {265--276},
optyear = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = aug,
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
url = {http://doi.acm.org/10.1145/1080091.1080123},
doi = {10.1145/1080091.1080123},
pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/paper.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/Netsem/paper.ps},
abstract = {
Network protocols are hard to implement correctly. Despite the
existence of RFCs and other standards, implementations often
have subtle differences and bugs. One reason for this is that the
specifications are typically informal, and hence inevitably contain
ambiguities. Conformance testing against such specifications is
challenging.
In this paper we present a practical technique for rigorous
protocol specification that supports specification-based testing. We
have applied it to TCP, UDP, and the Sockets API, developing
a detailed ‘post-hoc’ specification that accurately reflects the
behaviour of several existing implementations (FreeBSD 4.6,
Linux 2.4.20-8, and Windows XP SP1). The development process
uncovered a number of differences between and infelicities in these
implementations.
Our experience shows for the first time that rigorous specification
is feasible for protocols as complex as TCP.
We argue
that the technique is also applicable ‘pre-hoc’, in the design
phase of new protocols. We discuss how such a design-for-test approach should influence protocol development, leading to
protocol specifications that are both unambiguous and clear, and
to high-quality implementations that can be tested directly against
those specifications.
},
topic = {netsem},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}
@inproceedings{SLWZAHV05,
optnote = {SLWAZHV04-paper},
author = {Peter Sewell and
James J. Leifer and
Keith Wansbrough and
Zappa Nardelli, Francesco and
Mair Allen-Williams and
Pierre Habouzit and
Viktor Vafeiadis},
title = {Acute: High-level programming language design for distributed
computation},
optcrossref = {},
optkey = {},
conf = {ICFP 2005},
booktitle = {Proceedings of the 10th ACM SIGPLAN International Conference on
Functional Programming (Tallinn)},
pages = {15--26},
year = {2005},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = sep,
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
url = {http://doi.acm.org/10.1145/1086365.1086370},
doi = {10.1145/1086365.1086370},
pdf = {http://www.cl.cam.ac.uk/~pes20/acute/acute2-short.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/acute/acute2-short.ps},
abstract = {
Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there
may be interaction between multiple instances of many distinct pro-grams, sharing some (but not necessarily all) of their module structure, and with some instances rebuilt with new versions of certain modules as time goes on. In this paper we discuss programming language support for su
ch systems, focussing on their typing and naming issues.
We describe an experimental language, Acute, which extends an
ML core to support distributed development, deployment, and execution, allowing type-safe interaction between separately-built
programs. The main features are: (1) type-safe marshalling of arbitrary values; (2) type names that are generated (freshly and by
hashing) to ensure that type equality tests suffice to protect the invariants of abstract types, across the entire distributed system; (3)
expression-level names generated to ensure that name equality tests suffice for type-safety of associated values, e.g.~values carried on
named channels; (4) controlled dynamic rebinding of marshalled values to local resources; and (5) thunkification of threads and mutexes to support computation mobility.
These features are a large part of what is needed for typeful
distributed programming. They are a relatively lightweight extension of
ML, should be efficiently implementable, and are expressive enough to enable a wide variety of distributed infrastructure layers
to be written as simple library code above the byte-string network and persistent store APIs. This disentangles the language runtime
from communication intricacies. This paper highlights the main design choices in
Acute. It is supported by a full language definition (of typing, compilation, and operational semantics), by a prototype
implementation, and by example distribution libraries.
},
topic = {distributed_types},
project = {http://www.cl.cam.ac.uk/~pes20/acute/}
}
@inproceedings{PSWZ05,
author = {Benjamin C. Pierce and Peter Sewell and
Stephanie Weirich and Steve Zdancewic},
title = {It is Time to Mechanize Programming
Language Metatheory},
conf = {VSTTE 2005},
booktitle = {Verified Software: Theories, Tools, Experiments (Z\"urich)},
year = 2005,
optaddress = {, Switzerland},
month = oct,
note = {5pp},
url = {https://doi.org/10.1007/978-3-540-69149-5_3},
doi = {10.1007/978-3-540-69149-5_3},
pdf = {http://vstte.ethz.ch/Files/pierce-sewell-weirich-zdancewic.pdf},
abstract = {How close are we to a world in which mechanically verified
software is commonplace? A world in which theorem proving technology
is used routinely by both software developers and programming language
researchers alike? One crucial step towards achieving these goals is mechanized
reasoning about language metatheory. The time has come to bring
together the theorem proving and programming language communities
to address this problem. We have proposed the POPLMark challenge
as a concrete set of benchmarks intended both for measuring progress in
this area and for stimulating discussion and collaboration. Our goal is
to push the boundaries of existing technology to the point where we can
achieve mechanized metatheory for the masses.},
topic = {poplmark},
project = {http://www.seas.upenn.edu/~plclub/poplmark/}
}
@article{SS05,
author = {Andrei Serjantov and Peter Sewell},
title = {Passive-attack analysis for connection-based anonymity systems},
journal = {International Journal of Information Security},
year = {2005},
optkey = {},
volume = {4},
number = {3},
pages = {172--180},
month = jun,
note = {Special issue on ESORICS 2003},
optannote = {},
url = {https://doi.org/10.1007/s10207-004-0059-3},
doi = {10.1007/s10207-004-0059-3},
abstract = {In this paper we consider low-latency connection-based anonymity systems which can be used for applications like web browsing or SSH. Although several such systems have been designed and built, their anonymity has so far not been adequately evaluated.
We analyse the anonymity of connection-based systems against global passive adversaries. We give a precise description of a packet-counting attack which requires a very low degree of precision from the adversary, evaluate its effectiveness against connection-based systems depending on their size, architecture and configuration, and calculate the amount of traffic necessary to provide a minimum degree of protection. We then present a second attack based on tracking connection starts which gives us another lower bound on traffic volumes required to provide at least some anonymity.
},
topic = {anonymity}
}
@inproceedings{TCP:techpaper,
optkey = {},
author = {Steven Bishop and Matthew Fairbairn and Michael Norrish and
Peter Sewell and Michael Smith and Keith Wansbrough},
title = {Engineering with Logic: {HOL} Specification and Symbolic-Evaluation Testing for {TCP} Implementations},
year = {2006},
pages = {55--66},
optcrossref = {},
optkey = {},
conf = {POPL 2006},
booktitle = {Proceedings of The 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Charleston)},
optpages = {},
optyear = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = jan,
optorganization = {},
optpublisher = {},
optnote = {To appear.},
optannote = {},
url = {http://doi.acm.org/10.1145/1111037.1111043},
doi = {10.1145/1111037.1111043},
pdf = {http://www.cl.cam.ac.uk/users/pes20/Netsem/tech-paper.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/Netsem/tech-paper.ps},
topic = {netsem},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}
@article{DBLP:journals/entcs/Sewell06,
author = {Peter Sewell},
title = {Process Calculi: The End of the Beginning? (From Thought
Experiments to Experimental Semantics)},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {162},
year = {2006},
pages = {317-321},
url = {https://doi.org/10.1016/j.entcs.2006.01.033},
doi = {10.1016/j.entcs.2006.01.033},
bibsource = {DBLP, http://dblp.uni-trier.de},
abstract = {
This note reflects, from a Process Calculus point of view, on lessons learned during research modelling the real-world TCP and UDP network protocols.},
topic = {misc}
}
@inproceedings{BSSS06,
author = {John Billings and Peter Sewell and Mark Shinwell and Rok Strni\v sa},
title = {Type-Safe Distributed Programming for {OCaml}},
optcrossref = {},
optkey = {},
conf = {ML 2006},
booktitle = {Proceedings of the 2006 ACM SIGPLAN Workshop on ML},
pages = {20--31},
year = {2006},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = sep,
optorganization = {},
optpublisher = {},
optannote = {},
project = {http://www.cl.cam.ac.uk/~pes20/hashcaml/index.html},
url = {http://doi.acm.org/10.1145/1159876.1159881},
doi = {10.1145/1159876.1159881},
pdf = {http://www.cl.cam.ac.uk/~pes20/hashcaml/paper.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/hashcaml/paper.ps},
abstract = {
Existing ML-like languages guarantee type-safety, ensuring memory safety and protecting the invariants of abstract types, but only
within single executions of single programs. Distributed programming is becoming ever more important, and should benefit even
more from such guarantees. In previous work on theoretical calculi and the Acute prototype language we outlined techniques to
provide them for simple languages.
In this paper we put these ideas into practice, describing the
HashCaml extension to the OCaml bytecode compiler, which supports type-safe and abstraction-safe marshalling, together with related naming constructs. Our contribution is threefold: (1) We show how to define globally meaningful runtime type names for key
OCaml type constructs that were not covered in our previous work, dealing with the generativity issues involved: user-defined variant and record types, substructures, functors, arbitrary ascription,separate compilation, and external C functions. (2) We support
marshalling within polymorphic functions by type-passing, requiring us to build compositional runtime type names and revisit the
OCaml relaxed value restriction. We show that with typed marshalling one must fall back to the SML97 value restriction. (3) We
show how the above can be implemented with reasonable performance as an unintrusive modification to the existing OCaml language, implementation, and standard libraries. An alpha release of HashCaml, capable of bootstrapping itself, is available, along with
an example type-safe distributed communication library written in the language.
},
topic = {distributed_types},
project = {http://www.cl.cam.ac.uk/~pes20/hashcaml/}
}
@inproceedings{BDJRS06,
author = {Adam Biltcliffe and Michael Dales and Sam Jansen and Thomas Ridge and Peter Sewell},
title = {Rigorous Protocol Design in Practice: An Optical Packet-Switch {MAC} in {HOL}},
optcrossref = {},
optkey = {},
conf = {ICNP 2006},
booktitle = {Proceedings of the 14th IEEE International Conference on Network Protocols (Santa Barbara)},
optpages = {},
year = {2006},
pages = {117--126},
numpages = {10},
opturl = {http://dx.doi.org/10.1109/ICNP.2006.320205},
url = {https://doi.org/10.1109/ICNP.2006.320205},
doi = {10.1109/ICNP.2006.320205},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = nov,
optorganization = {},
optpublisher = {},
optannote = {},
note = {See also the SWIFT MAC Protocol: HOL Specification at \url{http://www.cl.cam.ac.uk/~pes20/optical/spec.pdf}},
pdf = {http://www.cl.cam.ac.uk/~pes20/optical/root.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/optical/root.ps},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem/index.html},
abstract = {
This paper reports on an experiment in network
protocol design: we use novel rigorous techniques in the design
process of a new protocol, in a close collaboration between
systems and theory researchers.
The protocol is a Media Access Control (MAC) protocol for
the SWIFT optical network, which uses optical switching and
wavelength striping to provide very high bandwidth packet-switched interconnects. The use of optical switching (and the
lack of optical buffering) means that the protocol must control
the switch within hard timing constraints.
We use higher-order logic to express the protocol design,
in the general-purpose HOL automated proof assistant. The specification is thus completely precise, but still concise, readable, and without accidental overspecification. Further, we test
conformance between the specification and two implementations
of the protocol: an NS-2 simulation model and the VHDL code of
the network hardware. This involves: (1) proving, within HOL,
that the specification is equivalent to an algorithmically-checkable
version; (2) using automatic code-extraction to generate a testing
oracle; and (3) applying that oracle to traces of the implementation.
This design-time use of rigorous methods has resulted in a
protocol that is better specified and more correct than it would
otherwise be, with relatively little effort.
},
topic = {netsem},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}
@article{SHBSN-toplas,
optnote = {1255455},
author = {Gareth Stoyle and Michael Hicks and Gavin Bierman and Peter Sewell and Iulian Neamtiu},
title = {Mutatis Mutandis: Safe and predictable dynamic software updating},
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
optjournal = {ACM TOPLAS},
volume = {29},
number = {4},
year = {2007},
month = aug,
issn = {0164-0925},
pages = {70pp},
optnote = {70pp},
doi = {http://doi.acm.org/10.1145/1255450.1255455},
publisher = {ACM Press},
address = {New York, NY, USA},
pdf = {http://portal.acm.org/ft_gateway.cfm?id=1255455&type=pdf&coll=portal&dl=ACM&CFID=5852982&CFTOKEN=74490170},
abstract = {This article presents Proteus, a core calculus that models dynamic software updating, a service for fixing bugs and adding features to a running program. Proteus permits a program's type structure to change dynamically but guarantees the updated program remains type-correct by ensuring a property we call con-freeness. We show how con-freeness can be enforced dynamically, and how it can be approximated via a novel static analysis. This analysis can be used to assess the implications of a program's structure on future updates in order to make update success more predictable. We have implemented Proteus for C, and briefly discuss our implementation which we have tested on several well-known programs.},
topic = {dynamic_update}
}
@article{SLWZAHV-jfp,
author = {Peter Sewell and
James J. Leifer and
Keith Wansbrough and
Zappa Nardelli, Francesco and
Mair Allen-Williams and
Pierre Habouzit and
Viktor Vafeiadis},
title = {Acute: High-level programming language design for distributed
computation},
optjournal = {J. Functional Programming},
journal = {Journal of Functional Programming},
year = {2007},
optkey = {},
volume = {17},
number = {4--5},
pages = {547--612},
month = jul,
note = {Invited submission for an ICFP 2005 special issue},
optannote = {},
project = {http://www.cl.cam.ac.uk/~pes20/acute/index.html},
pdf = {http://www.cl.cam.ac.uk/~pes20/acute/paper3.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/acute/paper3.ps},
url = {https://doi.org/10.1017/S0956796807006442},
doi = {10.1017/S0956796807006442},
abstract = {
Existing languages provide good support for typeful programming of stand-alone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct programs, sharing some (but not necessarily all) of their module structure, and with some instances rebuilt with new versions of certain modules as time goes on. In this paper, we discuss programming-language support for such systems, focussing on their typing and naming issues. We describe an experimental language, Acute, which extends an ML core to support distributed development, deployment, and execution, allowing type-safe interaction between separately built programs. The main features are (1) type-safe marshalling of arbitrary values; (2) type names that are generated (freshly and by hashing) to ensure that type equality tests suffice to protect the invariants of abstract types, across the entire distributed system; (3) expression-level names generated to ensure that name equality tests suffice for type safety of associated values, for example, values carried on named channels; (4) controlled dynamic rebinding of marshalled values to local resources; and (5) thunkification of threads and mutexes to support computation mobility. These features are a large part of what is needed for typeful distributed programming. They are a relatively lightweight extension of ML, should be efficiently implementable, and are expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs. This disentangles the language run-time from communication intricacies. This paper highlights the main design choices in Acute. It is supported by a full language definition (of typing, compilation, and operational semantics), by a prototype implementation, and by example distribution libraries.},
topic = {distributed_types},
project = {http://www.cl.cam.ac.uk/~pes20/acute/}
}
@inproceedings{ott-sub,
author = {Peter Sewell and Zappa Nardelli, Francesco and Scott Owens and Gilles Peskine and Thomas Ridge and Susmit Sarkar and Rok Strni\v sa},
title = {{Ott}: Effective Tool Support for the Working Semanticist},
optcrossref = {},
optkey = {},
conf = {ICFP 2007},
booktitle = {Proceedings of {the 12th ACM SIGPLAN International Co
nference on Functional Programming (Freiburg)}},
pages = {1--12},
numpages = {12},
opturl = {http://doi.acm.org/10.1145/1291151.1291155},
doi = {10.1145/1291151.1291155},
year = {2007},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = oct,
optorganization = {},
optpublisher = {},
note = {ACM SIGPLAN Most Influential ICFP Paper Award 2017 (for 2007)},
optannote = {},
project = {http://www.cl.cam.ac.uk/~pes20/ott/},
pdf = {http://www.cl.cam.ac.uk/~pes20/ott/paper.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/ott/paper.ps},
abstract = {It is rare to give a semantic definition of a full-scale programming language, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics - usually either LaTeX for informal mathematics, or the formal mathematics of a proof assistant - make it much harder than necessary to work with large definitions.
We present a metalanguage specifically designed for this problem, and a tool, ott, that sanity-checks such definitions and compiles them into proof assistant code for Coq, HOL, Isabelle, and (in progress) Twelf, together with LaTeX code for production-quality typesetting, and OCaml boilerplate. The main innovations are:(1) metalanguage design to make definitions concise, and easy to read and edit;(2) an expressive but intuitive metalanguage for specifying binding structures; and (3) compilation to proof assistant code.
This has been tested in substantial case studies, including modular specifications of calculi from the TAPL text, a Lightweight Java with Java JSR 277/294 module system proposals, and a large fragment of OCaml (around 306 rules), with machine proofs of various soundness results. Our aim with this work is to enable a phase change: making it feasible to work routinely, without heroic effort, with rigorous semantic definitions of realistic languages.},
topic = {ott}
}
@inproceedings{ljam-sub,
author = {Rok {Strni\v sa} and Peter Sewell and Matthew Parkinson},
title = {The {J}ava {M}odule {S}ystem: core design and semantic definition},
optcrossref = {},
optkey = {},
conf = {OOPSLA 2007},
booktitle = {Proceedings of the {22nd ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages and Applications (Montre{\'a}l)}},
optpages = {15 pp},
pages = {499--514},
numpages = {16},
opturl = {http://doi.acm.org/10.1145/1297027.1297064},
doi = {10.1145/1297027.1297064},
year = {2007},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = oct,
optorganization = {},
optpublisher = {},
optannote = {},
project = {http://www.cl.cam.ac.uk/~rs456/ljam/},
pdf = {http://www.cl.cam.ac.uk/~rs456/ljam/paper.pdf},
abstract = {
Java has no module system. Its packages only subdivide the class name space, allowing only a very limited form of component-level information hiding and reuse. Two Java Community Processes have started addressing this problem: one describes the runtime system and has reached an early draft stage, while the other considers the developer's view and only has a straw-man proposal. Both are natural language documents, which inevitably contain ambiguities.
In this work we design and formalize a core module system for Java. Where the JCP documents are complete, we follow them closely; elsewhere we make reasonable choices. We define the syntax, the type system, and the operational semantics of an LJAM language, defining these rigorously in the Isabelle/HOL automated proof assistant. Using this formalization, we identify various issues with the module system. We highlight the underlying design decisions, and discuss several alternatives and their benefits. Our Isabelle/HOL definitions should provide a basis for further consideration of the design alternatives, for reference implementations, and for proofs of soundness.},
topic = {java_modules}
}
@inproceedings{SSZ07,
author = {Susmit Sarkar and Peter Sewell and Zappa Nardelli, Francesco},
title = {Specifying real-world binding structures},
optcrossref = {},
optkey = {},
conf = {WMM 2007},
booktitle = {Proceedings of the 2nd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory
(Freiburg), in conjunction with ICFP},
year = {2007},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = oct,
optorganization = {},
optpublisher = {},
note = {1pp},
optannote = {},
project = {http://www.cl.cam.ac.uk/~pes20/ott/},
pdf = {http://www.cl.cam.ac.uk/~pes20/wmm07.pdf}
}
@article{BHSSW-jfp,
author = {Peter Sewell and Gareth Stoyle and Michael Hicks and Gavin Bierman and Keith Wansbrough},
title = {Dynamic Rebinding for Marshalling and Update, via Redex-time and Destruct-time Reduction},
journal = {Journal of Functional Programming},
year = {2008},
optkey = {},
volume = {18},
number = {4},
pages = {437--502},
optmonth = {},
optnote = {66pp.},
optannote = {},
doi = {https://doi.org/10.1017/S0956796807006600},
pdf = {http://www.cl.cam.ac.uk/~pes20/jfp2008.pdf},
abstract = {
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, for example, 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 this paper, we adopt a foundational approach, developing core dynamic rebinding mechanisms as extensions to the simply typed call-by-value lambda calculus. To do so, we must first explore refinements of the call-by-value reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduce redex-time and destruct-time strategies. The latter forms the basis for a lambda-marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically typed. We sketch an extension of lambda-marsh with concurrency and communication, giving examples showing how wrappers for encapsulating untrusted code can be expressed. Finally, we show 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 updating of running code. We show how the ideas of this simple calculus extend to more real-world, module-level dynamic updating in the style of Erlang. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding requirements.},
topic = {distributed_types_and_update}
}
@inproceedings{RNS08,
author = {Tom Ridge and Michael Norrish and Peter Sewell},
title = {A rigorous approach to networking: {TCP}, from implementation to protocol to service},
optcrossref = {},
optkey = {},
conf = {FM 2008},
booktitle = {Proceedings of the 15th International Symposium on Formal Methods (Turku, Finland), LNCS 5014},
pages = {294--309},
year = 2008,
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = may,
optorganization = {},
optpublisher = {},
optnote = {To appear},
optannote = {},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem/index.html},
url = {https://doi.org/10.1007/978-3-540-68237-0_21},
doi = {10.1007/978-3-540-68237-0_21},
pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/stream_spec.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/Netsem/stream_spec.ps},
abstract = {Despite more then 30 years of research on protocol specification, the major protocols deployed in the Internet, such as TCP, are described only in informal prose RFCs and executable code. In part this is because the scale and complexity of these protocols makes them challenging targets for formalization.
In this paper we show how these difficulties can be addressed. We develop a high-level specification for TCP and the Sockets API, expressed in the HOL proof assistant, describing the byte-stream service that TCP provides to users. This complements our previous low-level specification of the protocol internals, and makes it possible for the first time to state what it means for TCP to be correct: that the protocol implements the service. We define a precise abstraction function between the models and validate it by testing, using verified testing infrastructure within HOL. This is a pragmatic alternative to full proof, providing reasonable confidence at a relatively low entry cost.
Together with our previous validation of the low-level model, this shows how one can rigorously tie together concrete implementations, low-level protocol models, and specifications of the services they claim to provide, dealing with the complexity of real-world protocols throughout.},
topic = {netsem},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}
@inproceedings{npict-r2d2,
author = {Peter Sewell and Pawe{\l} Wojciechowski},
title = {Verifying Overlay Networks for Relocatable Computations
(or: {Nomadic Pict}, relocated)},
optcrossref = {},
optkey = {},
conf = {RRDD Workshop, 2008},
booktitle = {Proceedings of the workshop on The Rise and Rise of the Declarative Datacentre, Microsoft Research Technical Report MSR-TR-2008-61},
pages = {43--46},
year = {2008},
opteditor = {Karthikeyan Bhargavan, Andrew Gordon, Tim Harris, and Peter Toft},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = may,
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/r2d2.pdf},
abstract = {In the late 1990s we developed a calculus, Nomadic Pict, in which
to express and verify overlay networks, for reliable communication
between relocatable computations. Then, efficient system support
for relocation was rare, and the calculus was reified in a prototype
high-level programming language. Now, relocatable computation
is a pervasive reality, though at the level of virtual machines rather
than high-level languages. One can ask whether the semantic theory
and algorithms developed for Nomadic Pict can be applied (or
adapted) to infrastructure for communication between these virtual
machines.},
topic = {nomadic_pict},
project = {http://www.cl.cam.ac.uk/~pes20/nomadicpict.html}
}
@inproceedings{tphols09,
author = {Scott Owens and Susmit Sarkar and Peter Sewell},
title = {A better x86 memory model: {x86-TSO}},
conf = {TPHOLs 2009},
booktitle = {Proceedings of Theorem Proving in Higher Order Logics, LNCS 5674},
pages = {391--407},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-03359-9_27},
doi = {10.1007/978-3-642-03359-9_27},
pdf = {http://www.cl.cam.ac.uk/~pes20/weakmemory/x86tso-paper.tphols.pdf},
abstract = {Real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have relaxed memory models, typically described in
ambiguous prose, which lead to widespread confusion. These are prime
targets for mechanized formalization. In previous work we produced a rigorous x86-CC model, formalizing the Intel and AMD architecture specifications of the time, but those turned out to be unsound with respect
to actual hardware, as well as arguably too weak to program above.
We discuss these issues and present a new x86-TSO model that suffers
from neither problem, formalized in HOL4. We believe it is sound with
respect to real processors, reflects better the vendor’s intentions, and is
also better suited for programming. We give two equivalent definitions of
x86-TSO: an intuitive operational model based on local write buffers, and
an axiomatic total store ordering model, similar to that of the SPARCv8.
Both are adapted to handle x86-specific features. We have implemented
the axiomatic model in our memevents tool, which calculates the set of all
valid executions of test programs, and, for greater confidence, verify the
witnesses of such executions directly, with code extracted from a third,
more algorithmic, equivalent version of the definition.
},
topic = {x86}
}
@inproceedings{damp09,
optkey = {},
author = {Jade Alglave and Anthony Fox and Samin Ishtiaq and Magnus O. Myreen and Susmit Sarkar and Peter Sewell and Zappa Nardelli, Francesco},
title = {The Semantics of {Power} and {ARM} Multiprocessor Machine Code},
year = {2009},
optpages = {},
optcrossref = {},
optkey = {},
conf = {DAMP 2009},
booktitle = {Proceedings of the 4th Workshop on Declarative Aspects of Multicore Programming},
isbn = {978-1-60558-417-1},
location = {Savannah, GA, USA},
optnote = {553091},
publisher = {ACM},
address = {New York, NY, USA},
optpages = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = jan,
optorganization = {},
optpublisher = {},
optnote = {To appear},
optannote = {},
opturl = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/weakmemory/draft-ppc-arm.pdf},
doi = {10.1145/1481839.1481842},
abstract = {We develop a rigorous semantics for Power and ARM multiprocessor programs, including their relaxed memory model and the behaviour of reasonable fragments of their instruction sets. The semantics is mechanised in the HOL proof assistant. This should provide a good basis for informal reasoning and formal verification of low-level code for these weakly consistent architectures, and, together with our x86 semantics, for the design and compilation of high-level concurrent languages.},
topic = {Power_and_ARM}
}
@inproceedings{x86popl,
optkey = {},
optauthor = {S. Sarkar and P. Sewell and Zappa Nardelli, F. and S. Owens and T. Ridge and T. Braibant and M. Myreen and J. Alglave},
author = {Susmit Sarkar and Peter Sewell and Zappa Nardelli, Francesco and Scott Owens and Tom Ridge and Thomas Braibant and Magnus Myreen and Jade Alglave},
title = {The Semantics of {x86-CC} Multiprocessor Machine Code},
year = {2009},
optpages = {},
optcrossref = {},
optkey = {},
conf = {POPL 2009},
booktitle = {Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages},
optbooktitle = {Proc.~POPL 2009},
pages = {379--391},
numpages = {13},
opturl = {http://doi.acm.org/10.1145/1594834.1480929},
doi = {10.1145/1594834.1480929},
optpages = {},
optyear = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = jan,
optorganization = {},
optpublisher = {},
optnote = {To appear},
optannote = {},
opturl = {},
pdf = {https://www.cl.cam.ac.uk/~pes20/weakmemory/popl09.pdf},
abstract = {Multiprocessors are now dominant, but real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have subtle relaxed (or weak) memory models, usually described only in ambiguous prose, leading to widespread confusion.
We develop a rigorous and accurate semantics for x86 multiprocessor programs, from instruction decoding to relaxed memory model, mechanised in HOL. We test the semantics against actual processors and the vendor litmus-test examples, and give an equivalent abstract-machine characterisation of our axiomatic memory model. For programs that are (in some precise sense) data-race free, we prove in HOL that their behaviour is sequentially consistent. We also contrast the x86 model with some aspects of Power and ARM behaviour.
This provides a solid intuition for low-level programming, and a sound foundation for future work on verification, static analysis, and compilation of low-level concurrent code.},
topic = {x86}
}
@inproceedings{mtv09,
author = {Peter Sewell},
title = {Multiprocessor Architectures Don't Really Exist (But They Should)},
optcrossref = {},
optkey = {},
conf = {MTV 2010},
booktitle = {Proceedings of the 10th International Workshop on Microprocessor Test and Verification (MTV), Austin, Texas},
pages = {2},
year = {2009},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
optmonth = {},
optorganization = {},
optpublisher = {},
note = {Invited session on Verification issues for multi-core systems},
pdf = {https://www.cl.cam.ac.uk/~pes20/weakmemory/mtv_2009.pdf},
optannote = {},
abstract = {Multiprocessors and high-level concurrent languages generally provide only relaxed (non-sequentially-consistent) memory models, to permit performance optimisations.
One has to understand these models to program reliable concurrent systems but, despite work in this area over many years, the
specifications of real-world multiprocessors and languages are
typically ambiguous and incomplete informal-prose documents,
cannot be used for testing hardware or software, sometimes give
guarantees that are too weak to be useful, and are sometimes
simply unsound. Such informal prose is a very poor medium for
loose specifications.
This talk will review various problems with some current
specifications, for x86 (Intel 64/IA32 and AMD64), and Power
and ARM processors, and for the Java and C++ languages, and
describe ongoing work to produce rigorously defined specifications for some of these.
},
topic = {relaxed}
}
@techreport{UCAM-CL-TR-742,
author = {Ridge, Thomas and Norrish, Michael and Sewell, Peter},
title = {{TCP, UDP, and Sockets: Volume 3: The Service-level
Specification}},
year = 2009,
month = feb,
pdf = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-742.pdf},
institution = {University of Cambridge, Computer Laboratory},
number = {UCAM-CL-TR-742},
note = {305pp},
topic = {netsem},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}
@techreport{UCAM-CL-TR-745,
author = {Owens, Scott and Sarkar, Susmit and Sewell, Peter},
title = {{A better x86 memory model: x86-TSO (extended version)}},
year = 2009,
month = mar,
pdf = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-745.pdf},
institution = {University of Cambridge, Computer Laboratory},
number = {UCAM-CL-TR-745},
note = {52pp},
pdf = {http://www.cl.cam.ac.uk/~pes20/weakmemory/x86tso-paper.pdf},
abstract = {Real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have relaxed memory models, typically described in ambiguous prose, which lead to widespread confusion. These are prime targets for mechanized formalization. In previous work we produced a rigorous x86-CC model, formalizing the Intel and AMD architecture specifications of the time, but those turned out to be unsound with respect to actual hardware, as well as arguably too weak to program above. We discuss these issues and present a new x86-TSO model that suffers from neither problem, formalized in HOL4. We believe it is sound with respect to real processors, reflects better the vendor's intentions, and is also better suited for programming. We give two equivalent definitions of x86-TSO: an intuitive operational model based on local write buffers, and an axiomatic total store ordering model, similar to that of the SPARCv8. Both are adapted to handle x86-specific features. We have implemented the axiomatic model in our memevents tool, which calculates the set of all valid executions of test programs, and, for greater confidence, verify the witnesses of such executions directly, with code extracted from a third, more algorithmic, equivalent version of the definition.
},
topic = {x86}
}
@inproceedings{ec2,
author = {Zappa Nardelli, Francesco and Peter Sewell and Jaroslav \v{S}ev\v{c}\'{\i}k and Susmit
Sarkar and Scott Owens and Luc Maranget and Mark Batty and Jade Alglave},
title = {Relaxed memory models must be rigorous},
optcrossref = {},
optkey = {},
conf = {EC2},
booktitle = {Proceedings of EC2: Exploiting Concurrency Efficiently and Correctly (CAV 2009 Workshop) (Grenoble, France)},
pages = {4pp},
year = {2009},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = jun,
optorganization = {},
optpublisher = {},
optnote = {\url{http://www.cs.utah.edu/ec2/}},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/weakmemory/ec2.pdf},
abstract = {Multiprocessors and high-level languages generally provide
only relaxed (non-sequentially-consistent) memory models,
to permit performance optimisations. One has to understand
these models to program reliable concurrent systems -- but
they are typically ambiguous and incomplete informal-prose
documents, sometimes give guarantees that are too weak
to be useful, and are sometimes simply unsound. Based on
our previous work, we review various problems with some
current specifications, for x86 (Intel 64/IA32 and AMD64),
and Power and ARM processors, and for the Java and
C++ languages. We argue that such specifications should
be rigorously defined and tested.
},
topic = {relaxed}
}
@article{npict-toplas,
author = {Peter Sewell and Pawe{\l} Wojciechowski and Asis Unyapoth},
title = {Nomadic {Pict}: Programming Languages, Communication Infrastructure Overlays, and Semantics for Mobile Computation},
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
year = {2010},
optkey = {},
volume = {32},
number = {4},
pages = {1--63 (and electronic appendix, 33pp)},
optmonth = {},
optnote = {(Accepted for publication, 3 Sep.~2009)},
optannote = {},
doi = {10.1145/1734206.1734209},
pdf = {http://www.cl.cam.ac.uk/~pes20/npict.pdf},
abstract = {
Mobile computation, in which executing computations can move from one physical computing device to another, is a recurring theme: from OS process migration, to language-level mobility, to virtual machine migration. This article reports on the design, implementation, and verification of overlay networks to support reliable communication between migrating computations, in the Nomadic Pict project. We define two levels of abstraction as calculi with precise semantics: a low-level Nomadic $\pi$ calculus with migration and location-dependent communication, and a high-level calculus that adds location-independent communication. Implementations of location-independent communication, as overlay networks that track migrations and forward messages, can be expressed as translations of the high-level calculus into the low. We discuss the design space of such overlay network algorithms and define three precisely, as such translations. Based on the calculi, we design and implement the Nomadic Pict distributed programming language, to let such algorithms (and simple applications above them) to be quickly prototyped. We go on to develop the semantic theory of the Nomadic $\pi$ calculi, proving correctness of one example overlay network. This requires novel equivalences and congruence results that take migration into account, and reasoning principles for agents that are temporarily immobile (e.g., waiting on a lock elsewhere in the system). The whole stands as a demonstration of the use of principled semantics to address challenging system design problems.
},
topic = {nomadic_pict},
project = {http://www.cl.cam.ac.uk/~pes20/nomadicpict.html}
}
@article{ott-jfp,
author = {Peter Sewell and Zappa Nardelli, Francesco and Scott Owens and Gilles Peskine and Thomas Ridge and Susmit Sarkar and Rok Strni\v sa},
title = {{Ott}: Effective Tool Support for the Working Semanticist},
optcrossref = {},
optkey = {},
optjournal = {J. Functional Programming},
journal = {Journal of Functional Programming},
year = {2010},
optkey = {},
volume = {20},
number = {1},
pages = {70--122},
month = jan,
note = {Invited submission from ICFP 2007},
optannote = {},
project = {http://www.cl.cam.ac.uk/~pes20/ott/},
doi = {https://doi.org/10.1017/S0956796809990293},
pdf = {http://www.cl.cam.ac.uk/~pes20/ott/ott-jfp.pdf},
abstract = {
Semantic definitions of full-scale programming languages are rarely given, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics – usually either LaTeX for informal mathematics or the formal mathematics of a proof assistant – make it much harder than necessary to work with large definitions. We present a metalanguage specifically designed for this problem, and a tool, Ott, that sanity-checks such definitions and compiles them into proof assistant code for Coq, HOL, and Isabelle/HOL, together with LaTeX code for production-quality typesetting, and OCaml boilerplate. The main innovations are (1) metalanguage design to make definitions concise, and easy to read and edit; (2) an expressive but intuitive metalanguage for specifying binding structures; and (3) compilation to proof assistant code. This has been tested in substantial case studies, including modular specifications of calculi from the TAPL text, a Lightweight Java with Java JSR 277/294 module system proposals, and a large fragment of OCaml (OCamllight, 310 rules), with mechanised proofs of various soundness results. Our aim with this work is to enable a phase change: making it feasible to work routinely, without heroic effort, with rigorous semantic definitions of realistic languages.},
topic = {ott}
}
@inproceedings{cav2010,
author = {Jade Alglave and
Luc Maranget and
Susmit Sarkar and
Peter Sewell},
title = {Fences in Weak Memory Models},
conf = {CAV 2010},
booktitle = {Proceedings of the 22nd International Conference on Computer Aided Verification, LNCS 6174},
year = {2010},
pages = {258-272},
doi = {http://dx.doi.org/10.1007/978-3-642-14295-6_25},
optcrossref = {DBLP:conf/cav/2010},
bibsource = {DBLP, http://dblp.uni-trier.de},
pdf = {http://www.cl.cam.ac.uk/~pes20/weakmemory/cav2010.pdf},
abstract = {We present a class of relaxed memory models, defined in Coq, parameterised by the chosen permitted local reorderings of reads and writes, and the visibility of inter- and intra-processor communications through memory (e.g. store atomicity relaxation). We prove results on the required behaviour and placement of memory fences to restore a given model (such as Sequential Consistency) from a weaker one. Based on this class of models we develop a tool, diy, that systematically and automatically generates and runs litmus tests to determine properties of processor implementations. We detail the results of our experiments on Power and the model we base on them. This work identified a rare implementation error in Power 5 memory barriers (for which IBM is providing a workaround); our results also suggest that Power 6 does not suffer from this problem.},
topic = {Power_and_ARM}
}
@inproceedings{Sewell:2010:MEA:1806651.1806660,
author = {Sewell, Peter},
title = {Memory, an elusive abstraction},
conf = {ISMM 2010},
booktitle = {Proceedings of the International Symposium on Memory Management},
optseries = {ISMM '10},
year = {2010},
isbn = {978-1-4503-0054-4},
location = {Toronto, Ontario, Canada},
pages = {51--52},
numpages = {2},
opturl = {http://doi.acm.org/10.1145/1806651.1806660},
doi = {http://doi.acm.org/10.1145/1806651.1806660},
acmid = {1806660},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {relaxed memory models, semantics},
note = {Invited talk abstract},
pdf = {https://www.cl.cam.ac.uk/~pes20/weakmemory/ismm1kn2-sewell.pdf},
topic = {relaxed}
}
@article{cacm,
author = {Peter Sewell and Susmit Sarkar and Scott Owens and Zappa Nardelli, Francesco and Magnus O. Myreen},
title = {{x86-TSO}: A Rigorous and Usable Programmer's Model for x86 Multiprocessors},
journal = {Communications of the ACM},
year = {2010},
optkey = {},
volume = {53},
number = {7},
pages = {89--97},
month = jul,
url = {http://doi.acm.org/10.1145/1785414.1785443},
doi = {10.1145/1785414.1785443},
note = {(Research Highlights)},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/weakmemory/cacm.pdf},
abstract = {Exploiting the multiprocessors that have recently become
ubiquitous requires high-performance and reliable concurrent systems code, for concurrent data structures, operating system kernels, synchronisation libraries, compilers, and
so on. However, concurrent programming, which is always
challenging, is made much more so by two problems. First,
real multiprocessors typically do not provide the sequentially
consistent memory that is assumed by most work on semantics and verification. Instead, they have relaxed memory
models, varying in subtle ways between processor families,
in which different hardware threads may have only loosely
consistent views of a shared memory. Second, the public
vendor architectures, supposedly specifying what programmers can rely on, are often in ambiguous informal prose (a
particularly poor medium for loose specifications), leading
to widespread confusion.
In this paper we focus on x86 processors. We review several recent Intel and AMD specifications, showing that all
contain serious ambiguities, some are arguably too weak to
program above, and some are simply unsound with respect
to actual hardware. We present a new x86-TSO programmer's model that, to the best of our knowledge, suffers from
none of these problems. It is mathematically precise (rigorously defined in HOL4) but can be presented as an intuitive abstract machine which should be widely accessible to
working programmers. We illustrate how this can be used to
reason about the correctness of a Linux spinlock implementation and describe a general theory of data-race-freedom for
x86-TSO. This should put x86 multiprocessor system building on a more solid foundation; it should also provide a basis
for future work on verification of such systems.
},
topic = {x86}
}
@misc{N3132,
optkey = {},
author = {M. Batty and S. Owens and S. Sarkar and P. Sewell and T. Weber},
title = {N3132: {Mathematizing C++ Concurrency: The Post-Rapperswil Model}},
howpublished = {ISO JTC1/SC22/WG21 - The C++ Standards Committee. Working Paper},
month = aug,
year = 2010,
optnote = {},
optannote = {},
topic = {c11}
}
@misc{N3125,
optkey = {},
author = {P. McKenney and M. Batty and C. Nelson and H. Boehm and A. Williams and S. Owens and S. Sarkar and P. Sewell and T. Weber and M.Wong and L. Crowl},
title = {N3125: Omnibus Memory Model and Atomics Paper},
howpublished = {ISO JTC1/SC22/WG21 - The C++ Standards Committee. Working Paper},
month = aug,
year = 2010,
optnote = {},
optannote = {},
topic = {c11}
}
@inproceedings{WMM10,
author = {Stephanie Weirich and Scott Owens and Peter Sewell and Zappa Nardelli, Francesco},
title = {{Ott} or {Nott}},
month = sep,
year = 2010,
note = {2pp},
conf = {WMM 2010},
booktitle = {Proceedings of the 5th ACM SIGPLAN Workshop on Mechanizing Metatheory},
project = {http://www.cl.cam.ac.uk/~pes20/ott/},
pdf = {https://www.cl.cam.ac.uk/~pes20/ott/wmm2010.pdf},
abstract = {
Ott: This talk discusses the experience of using Ott for programming
language design. Or Nott?
We reflect on the limitations of Ott, and on what other (New Ott?)
tool support a working semanticist might want in an ideal world.
},
topic = {ott}
}
@misc{N3196,
optkey = {},
author = {P. McKenney and M. Batty and C. Nelson and H. Boehm and A. Williams and S. Owens and S. Sarkar and P. Sewell and T. Weber and M.Wong and L. Crowl and B. Kosnik},
title = {N3196: Omnibus Memory Model and Atomics Paper},
howpublished = {ISO JTC1/SC22/WG21 -- The C++ Standards Committee. Working Paper},
month = nov,
year = 2010,
optnote = {},
optannote = {},
topic = {c11}
}
@inproceedings{DBLP:conf/itp/OwensBNS11,
author = {Scott Owens and
Peter B{\"o}hm and
Francesco Zappa Nardelli and
Peter Sewell},
title = {Lem: A Lightweight Tool for Heavyweight Semantics},
conf = {ITP 2011},
booktitle = {Proceedings of Interactive Theorem Proving -- Second International Conference (previously {TPHOLs}) (Berg en Dal), LNCS 6898},
year = {2011},
pages = {363-369},
ee = {http://dx.doi.org/10.1007/978-3-642-22863-6_27},
optcrossref = {DBLP:conf/itp/2011},
bibsource = {DBLP, http://dblp.uni-trier.de},
url = {https://doi.org/10.1007/978-3-642-22863-6_27},
doi = {10.1007/978-3-642-22863-6_27},
note = {(Rough Diamond) 7pp},
project = {http://www.cl.cam.ac.uk/~pes20/lem/},
topic = {lem}
}
@inproceedings{pldi105,
author = {Susmit Sarkar and Peter Sewell and Jade Alglave and Luc Maranget and Derek Williams},
title = {Understanding {POWER} Multiprocessors},
optcrossref = {},
optkey = {},
conf = {PLDI 2011},
booktitle = {Proceedings of the 32nd ACM SIGPLAN conference on Programming Language Design and Implementation},
optbooktitle = {Proc.~PLDI},
optpages = {},
year = {2011},
pages = {175--186},
numpages = {12},
opturl = {http://doi.acm.org/10.1145/1993498.1993520},
doi = {10.1145/1993498.1993520},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
optmonth = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/pldi105-sarkar.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/index.html},
abstract = {Exploiting today's multiprocessors requires high-performance and correct concurrent systems code (optimising compilers, language runtimes, OS kernels, etc.), which in turn requires a good understanding of the observable processor behaviour that can be relied on. Unfortunately this critical hardware/software interface is not at all clear for several current multiprocessors.
In this paper we characterise the behaviour of IBM POWER multiprocessors, which have a subtle and highly relaxed memory model (ARM multiprocessors have a very similar architecture in this respect). We have conducted extensive experiments on several generations of processors: POWER G5, 5, 6, and 7. Based on these, on published details of the microarchitectures, and on discussions with IBM staff, we give an abstract-machine semantics that abstracts from most of the implementation detail but explains the behaviour of a range of subtle examples. Our semantics is explained in prose but defined in rigorous machine-processed mathematics; we also confirm that it captures the observable processor behaviour, or the architectural intent, for our examples with an executable checker. While not officially sanctioned by the vendor, we believe that this model gives a reasonable basis for reasoning about current POWER multiprocessors.
Our work should bring new clarity to concurrent systems programming for these architectures, and is a necessary precondition for any analysis or verification. It should also inform the design of languages such as C and C++, where the language memory model is constrained by what can be efficiently compiled to such multiprocessors.},
topic = {Power_and_ARM}
}
@inproceedings{Alglave:2011:LRT:1987389.1987395,
author = {Alglave, Jade and Maranget, Luc and Sarkar, Susmit and Sewell, Peter},
title = {Litmus: running tests against hardware},
conf = {TACAS 2011},
booktitle = {Proceedings of the 17th international conference on Tools and Algorithms for the Construction and Analysis of Systems},
optseries = {TACAS'11/ETAPS'11},
year = {2011},
isbn = {978-3-642-19834-2},
location = {Saarbr\&\#252;cken, Germany},
pages = {41--44},
numpages = {4},
url = {https://doi.org/10.1007/978-3-642-19835-9_5},
doi = {10.1007/978-3-642-19835-9_5},
acmid = {1987395},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
pdf = {https://www.cl.cam.ac.uk/~pes20/weakmemory/tacas11.pdf},
abstract = {Shared memory multiprocessors typically expose subtle, poorly understood and poorly specified relaxed-memory semantics to programmers. To understand them, and to develop formal models to use in program verification, we find it essential to take an empirical approach, testing what results parallel programs can actually produce when executed on the hardware. We describe a key ingredient of our approach, our litmus tool, which takes small 'litmus test' programs and runs them for many iterations to find interesting behaviour. It embodies various techniques for making such interesting behaviour appear more frequently.},
topic = {Power_and_ARM}
}
@inproceedings{compcertTSO-popl,
author = {Jaroslav \v{S}ev\v{c}\'{\i}k and Viktor Vafeiadis and Zappa Nardelli, Francesco and Suresh Jagannathan and Peter Sewell},
title = {Relaxed-Memory Concurrency and Verified Compilation},
optcrossref = {},
optkey = {},
conf = {POPL 2011},
booktitle = {Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
optbooktitle = {Proc.~POPL},
pages = {43--54},
numpages = {12},
opturl = {http://doi.acm.org/10.1145/1926385.1926393},
doi = {10.1145/1926385.1926393},
optpages = {},
year = {2011},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
optmonth = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/paper.pdf},
project = {https://www.cl.cam.ac.uk/~pes20/CompCertTSO},
abstract = {In this paper, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation above x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behaviour of the hardware, the effects of compiler optimisation on concurrent code, the need to support high-performance concurrent algorithms, and the desire for a reasonably simple programming model. In turn, this complexity makes verified (or verifying) compilation both essential and challenging.
We define a concurrent relaxed-memory semantics for ClightTSO, an extension of CompCert's Clight in which the processor's memory model is exposed for high-performance code. We discuss a strategy for verifying compilation from ClightTSO to x86, which we validate with correctness proofs (building on CompCert) for the most interesting compiler phases.},
topic = {CompCertTSO}
}
@inproceedings{cpp-popl,
optauthor = {M. Batty and S. Owens and S. Sarkar and P. Sewell and T. Weber},
author = {Mark Batty and Scott Owens and Susmit Sarkar and Peter Sewell and Tjark Weber},
title = {Mathematizing {C++} Concurrency},
optcrossref = {},
optkey = {},
conf = {POPL 2011},
booktitle = {Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
optbooktitle = {Proc.~POPL},
pages = {55--66},
numpages = {12},
doi = {10.1145/1926385.1926394},
optpages = {},
year = {2011},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
optmonth = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/cpp/popl085ap-sewell.pdf},
abstract = {Shared-memory concurrency in C and C++ is pervasive in systems programming, but has long been poorly defined. This motivated an ongoing shared effort by the standards committees to specify concurrent behaviour in the next versions of both languages. They aim to provide strong guarantees for race-free programs, together with new (but subtle) relaxed-memory atomic primitives for high-performance concurrent code. However, the current draft standards, while the result of careful deliberation, are not yet clear and rigorous definitions, and harbour substantial problems in their details.
In this paper we establish a mathematical (yet readable) semantics for C++ concurrency. We aim to capture the intent of the current (`Final Committee') Draft as closely as possible, but discuss changes that fix many of its problems. We prove that a proposed x86 implementation of the concurrency primitives is correct with respect to the x86-TSO model, and describe our Cppmem tool for exploring the semantics of examples, using code generated from our Isabelle/HOL definitions.
Having already motivated changes to the draft standard, this work will aid discussion of any further changes, provide a correctness condition for compilers, and give a much-needed basis for analysis and verification of concurrent C and C++ programs.},
topic = {c11}
}
@article{DBLP:journals/dagstuhl-reports/BoehmGHS11,
author = {Hans-Juergen Boehm and
Ursula Goltz and
Holger Hermanns and
Peter Sewell},
title = {Multi-Core Memory Models and Concurrency Theory ({Dagstuhl}
Seminar 11011)},
journal = {Dagstuhl Reports},
volume = {1},
number = {1},
year = {2011},
pages = {1-26},
doi = {http://dx.doi.org/10.4230/DagRep.1.1.1},
bibsource = {DBLP, http://dblp.uni-trier.de},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2011/3105/pdf/dagrep_v001_i001_p001_s11011.pdf},
abstract = {This report documents the programme and the outcomes of Dagstuhl Seminar 11011 "Multi-Core Memory Models and Concurrency Theory".},
topic = {relaxed}
}
@inproceedings{Gordon:2011:RMV:1926385.1926439,
author = {Gordon, Andrew D. and Harper, Robert and Harrison, John and Jeffrey, Alan and Sewell, Peter},
title = {{Robin Milner} 1934--2010: verification, languages, and concurrency},
conf = {POPL 2011},
booktitle = {Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages},
optseries = {POPL '11},
year = {2011},
isbn = {978-1-4503-0490-0},
optlocation = {Austin, Texas, USA},
pages = {473--474},
numpages = {2},
opturl = {http://doi.acm.org/10.1145/1926385.1926439},
doi = {http://doi.acm.org/10.1145/1926385.1926439},
optacmid = {1926439},
optpublisher = {ACM},
optaddress = {New York, NY, USA},
optkeywords = {Robin Milner},
topic = {misc}
}
@inproceedings{DBLP:conf/cav/Mador-HaimMSMAOAMSW12,
author = {Sela Mador-Haim and
Luc Maranget and
Susmit Sarkar and
Kayvan Memarian and
Jade Alglave and
Scott Owens and
Rajeev Alur and
Milo M. K. Martin and
Peter Sewell and
Derek Williams},
title = {An Axiomatic Memory Model for {POWER} Multiprocessors},
booktitle = {Proceedings of the 24th International Conference on Computer Aided Verification},
conf = {CAV 2012},
year = {2012},
pages = {495-512},
opturl = {http://dx.doi.org/10.1007/978-3-642-31424-7_36},
doi = {10.1007/978-3-642-31424-7_36},
ee = {http://dx.doi.org/10.1007/978-3-642-31424-7_36},
optcrossref = {DBLP:conf/cav/2012},
bibsource = {DBLP, http://dblp.uni-trier.de},
pdf = {https://www.cl.cam.ac.uk/~pes20/weakmemory/CAV2012paper-final.pdf},
abstract = {The growing complexity of hardware optimizations employed by multiprocessors leads to subtle distinctions among allowed and disallowed behaviors, posing challenges in specifying their memory models formally and accurately, and in understanding and analyzing the behavior of concurrent software. This complexity is particularly evident in the IBM Power Architecture, for which a faithful specification was published only in 2011 using an operational style. In this paper we present an equivalent axiomatic specification, which is more abstract and concise. Although not officially sanctioned by the vendor, our results indicate that this axiomatic specification provides a reasonable basis for reasoning about current IBM POWER multiprocessors. We establish the equivalence of the axiomatic and operational specifications using both manual proof and extensive testing. To demonstrate that the constraint-based style of axiomatic specification is more amenable to computer-aided verification, we develop a SAT-based tool for evaluating possible outcomes of multi-threaded test programs, and we show that this tool is significantly more efficient than a tool based on an operational specification.},
topic = {Power_and_ARM}
}
@inproceedings{pldi2012,
author = {Susmit Sarkar and Kayvan Memarian and Scott Owens and Mark Batty and Peter Sewell and Luc Maranget and Jade Alglave and Derek Williams},
title = {Synchronising {C/C++} and {POWER}},
optcrossref = {},
optkey = {},
conf = {PLDI 2012},
booktitle = {Proceedings of the 33rd {ACM SIGPLAN conference on Programming Language Design and Implementation (Beijing)}},
pages = {311--322},
numpages = {12},
opturl = {http://doi.acm.org/10.1145/2254064.2254102},
doi = {10.1145/2254064.2254102},
year = {2012},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
optmonth = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/cppppc-supplemental/pldi010-sarkar.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/cppppc-supplemental/},
abstract = {Shared memory concurrency relies on synchronisation primitives: compare-and-swap, load-reserve/store-conditional (aka LL/SC), language-level mutexes, and so on. In a sequentially consistent setting, or even in the TSO setting of x86 and Sparc, these have well-understood semantics. But in the very relaxed settings of IBM, POWER, ARM, or C/C++, it remains surprisingly unclear exactly what the programmer can depend on.
This paper studies relaxed-memory synchronisation. On the hardware side, we give a clear semantic characterisation of the load-reserve/store-conditional primitives as provided by POWER multiprocessors, for the first time since they were introduced 20 years ago; we cover their interaction with relaxed loads, stores, barriers, and dependencies. Our model, while not officially sanctioned by the vendor, is validated by extensive testing, comparing actual implementation behaviour against an oracle generated from the model, and by detailed discussion with IBM staff. We believe the ARM semantics to be similar.
On the software side, we prove sound a proposed compilation scheme of the C/C++ synchronisation constructs to POWER, including C/C++ spinlock mutexes, fences, and read-modify-write operations, together with the simpler atomic operations for which soundness is already known from our previous work; this is a first step in verifying concurrent algorithms that use load-reserve/store-conditional with respect to a realistic semantics. We also build confidence in the C/C++ model in its own terms, fixing some omissions and contributing to the C standards committee adoption of the C++11 concurrency model.},
topic = {Power_and_ARM},
errata = {http://www.cl.cam.ac.uk/~pes20/cppppc/errata.html}
}
@inproceedings{popl2012,
author = {Mark Batty and Kayvan Memarian and Scott Owens and Susmit Sarkar and Peter Sewell},
title = {{Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER}},
optcrossref = {},
optkey = {},
conf = {POPL 2012},
booktitle = {Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Philadelphia)},
pages = {509--520},
numpages = {12},
opturl = {http://doi.acm.org/10.1145/2103656.2103717},
doi = {10.1145/2103656.2103717},
year = {2012},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
optmonth = {},
optorganization = {},
optpublisher = {},
optnote = {12 pp},
optannote = {},
project = {http://www.cl.cam.ac.uk/~pes20/cppppc},
pdf = {http://www.cl.cam.ac.uk/~pes20/cppppc/popl079-batty.pdf},
abstract = {The upcoming C and C++ revised standards add concurrency to the languages, for the first time, in the form of a subtle *relaxed memory model* (the *C++11 model*). This aims to permit compiler optimisation and to accommodate the differing relaxed-memory behaviours of mainstream multiprocessors, combining simple semantics for most code with high-performance *low-level atomics* for concurrency libraries. In this paper, we first establish two simpler but provably equivalent models for C++11, one for the full language and another for the subset without consume operations. Subsetting further to the fragment without low-level atomics, we identify a subtlety arising from atomic initialisation and prove that, under an additional condition, the model is equivalent to sequential consistency for race-free programs.
We then prove our main result, the correctness of two proposed compilation schemes for the C++11 load and store concurrency primitives to Power assembly, having noted that an earlier proposal was flawed. (The main ideas apply also to ARM, which has a similar relaxed memory architecture.)
This should inform the ongoing development of production compilers for C++11 and C1x, clarifies what properties of the machine architecture are required, and builds confidence in the C++11 and Power semantics.},
topic = {Power_and_ARM},
errata = {http://www.cl.cam.ac.uk/~pes20/cppppc/errata.html}
}
@inproceedings{Sewell:2012:FCS:2403555.2403560,
author = {Sewell, Peter},
title = {False Concurrency and Strange-but-true Machines},
conf = {CONCUR 2012},
booktitle = {Proceedings of the 23rd International Conference on Concurrency Theory},
optseries = {CONCUR'12},
year = {2012},
isbn = {978-3-642-32939-5},
location = {Newcastle upon Tyne, UK},
pages = {37--38},
numpages = {2},
opturl = {http://dx.doi.org/10.1007/978-3-642-32940-1_4},
doi = {10.1007/978-3-642-32940-1_4},
acmid = {2403560},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
note = {Invited talk abstract},
pdf = {},
abstract = {Concurrency theory and real-world multiprocessors have developed in parallel for the last 50 years, from their beginnings in the mid 1960s. Both have been very productive: concurrency theory has given us a host of models, calculi, and proof techniques, while engineered multiprocessors are now ubiquitous, from 2-8 core smartphones and laptops through to servers with 1024 or more hardware threads. But the fields have scarcely communicated, and the shared-memory interaction primitives offered by those mainstream multiprocessors are very different from the theoretical models that have been heavily studied.},
topic = {relaxed}
}
@inproceedings{Sewell:2012:TJ:2364527.2364566,
author = {Sewell, Peter},
title = {Tales from the Jungle},
conf = {ICFP 2012},
booktitle = {Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming},
optseries = {ICFP '12},
year = {2012},
isbn = {978-1-4503-1054-3},
location = {Copenhagen, Denmark},
pages = {271--272},
numpages = {2},
opturl = {http://doi.acm.org/10.1145/2364527.2364566},
doi = {10.1145/2364527.2364566},
acmid = {2364566},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {mainstream systems},
note = {Invited talk abstract},
abstract = {We rely on a computational infrastructure that is a densely interwined mass of software and hardware: programming languages, network protocols, operating systems, and processors. It has accumulated great complexity, from a combination of engineering design decisions, contingent historical choices, and sheer scale, yet it is defined at best by prose specifications, or, all too often, just by the common implementations. Can we do better? More specifically, can we apply rigorous methods to this mainstream infrastructure, taking the accumulated complexity seriously, and if we do, does it help? My colleagues and I have looked at these questions in several contexts: the TCP/IP network protocols with their Sockets API; programming language design, including the Java module system and the C11/C++11 concurrency model; the hardware concurrency behaviour of x86, IBM POWER, and ARM multiprocessors; and compilation of concurrent code.
In this talk I will draw some lessons from what did and did not succeed, looking especially at the empirical nature of some of the work, at the social process of engagement with the various different communities, and at the mathematical and software tools we used. Domain-specific modelling languages (based on functional programming ideas) and proof assistants were invaluable for working with the large and loose specifications involved: idioms within HOL4 for TCP, our Ott tool for programming language specification, and Owens's Lem tool for portable semantic definitions, with HOL4, Isabelle, and Coq, for the relaxed-memory concurrency semantics work. Our experience with these suggests something of what is needed to make full-scale rigorous semantics a commonplace reality.},
topic = {relaxed}
}
@article{Alglave:2012:FWM:2205506.2205523,
author = {Alglave, Jade and Maranget, Luc and Sarkar, Susmit and Sewell, Peter},
title = {Fences in Weak Memory Models (Extended Version)},
journal = {Formal Methods in System Design},
optissue_date = {April 2012},
volume = {40},
number = {2},
month = apr,
year = {2012},
issn = {0925-9856},
pages = {170--205},
numpages = {36},
opturl = {http://dx.doi.org/10.1007/s10703-011-0135-z},
doi = {10.1007/s10703-011-0135-z},
acmid = {2205523},
publisher = {Kluwer Academic Publishers},
address = {Hingham, MA, USA},
keywords = {Fences, Formal proofs, Generic framework, PowerPC, Testing tool, Weak memory models},
pdf = {https://www.cl.cam.ac.uk/~pes20/weakmemory/fmsd12-40-2.pdf},
abstract = {We present a class of relaxed memory models, defined in Coq, parameterised by the chosen permitted local reorderings of reads and writes, and by the visibility of inter- and intra-processor communications through memory (e.g. store atomicity relaxation). We prove results on the required behaviour and placement of memory fences to restore a given model (such as Sequential Consistency) from a weaker one. Based on this class of models we develop a tool, diy, that systematically and automatically generates and runs litmus tests. These tests can be used to explore the behaviour of processor implementations and the behaviour of models, and hence to compare the two against each other. We detail the results of experiments on Power and a model we base on them.},
topic = {Power_and_ARM}
}
@article{Sevcik:2013:CVC:2487241.2487248,
author = {\v{S}ev\v{c}\'{\i}k, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
title = {{CompCertTSO}: A Verified Compiler for Relaxed-Memory Concurrency},
optjournal = {Journal of the ACM},
journal = {J. ACM},
issue_date = {June 2013},
volume = {60},
number = {3},
month = jun,
year = {2013},
issn = {0004-5411},
pages = {22:1--22:50},
articleno = {22},
numpages = {50},
opturl = {http://doi.acm.org/10.1145/2487241.2487248},
doi = {10.1145/2487241.2487248},
acmid = {2487248},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Relaxed memory models, semantics, verified compilation},
project = {https://www.cl.cam.ac.uk/~pes20/CompCertTSO},
pdf = {https://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/paper-long.pdf},
abstract = {In this article, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation on x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behavior of the hardware, the effects of compiler optimization on concurrent code, the need to support high-performance concurrent algorithms, and the desire for a reasonably simple programming model. In turn, this complexity makes verified compilation both essential and challenging.
We describe ClightTSO, a concurrent extension of CompCert’s Clight in which the TSO-based memory model of x86 multiprocessors is exposed for high-performance code, and CompCertTSO, a formally verified compiler from ClightTSO to x86 assembly language, building on CompCert. CompCertTSO is verified in Coq: for any well-behaved and successfully compiled ClightTSO source program, any permitted observable behavior of the generated assembly code (if it does not run out of memory) is also possible in the source semantics. We also describe some verified fence-elimination optimizations, integrated into CompCertTSO.
},
topic = {CompCertTSO}
}
@article{Dreyer:2013:PP:2502508.2502517,
author = {Dreyer, Derek and Field, John and Giacobazzi, Roberto and Hicks, Michael and Jagannathan, Suresh and Sagiv, Mooly and Sewell, Peter and Wadler, Phil},
title = {Principles of {POPL}},
journal = {SIGPLAN Notices},
issue_date = {April 2013},
volume = {48},
number = {4S},
month = jul,
year = {2013},
issn = {0362-1340},
pages = {12--16},
numpages = {5},
opturl = {http://doi.acm.org/10.1145/2502508.2502517},
doi = {10.1145/2502508.2502517},
acmid = {2502517},
publisher = {ACM},
address = {New York, NY, USA},
topic = {misc}
}
@article{Sewell:2014:PPC:2641638.2641647,
author = {Sewell, Peter},
title = {{POPL} 2014 Program Chair's Report},
journal = {SIGPLAN Notices},
issue_date = {April 2014},
volume = {49},
number = {4},
month = jul,
year = {2014},
issn = {0362-1340},
pages = {10--26},
numpages = {17},
opturl = {http://doi.acm.org/10.1145/2641638.2641647},
doi = {10.1145/2641638.2641647},
acmid = {2641647},
publisher = {ACM},
address = {New York, NY, USA},
pdf = {http://www.cl.cam.ac.uk/~pes20/popl2014-pc-chair-report.pdf},
abstract = {This note describes the POPL 2014 paper selection process and its
rationale.
},
topic = {misc}
}
@inproceedings{Mulligan:2014:LRE:2628136.2628143,
author = {Mulligan, Dominic P. and Owens, Scott and Gray, Kathryn E. and Ridge, Tom and Sewell, Peter},
title = {Lem: Reusable Engineering of Real-world Semantics},
conf = {ICFP 2014},
booktitle = {Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming},
series = {ICFP '14},
year = {2014},
month = sep,
isbn = {978-1-4503-2873-9},
location = {Gothenburg, Sweden},
pages = {175--188},
numpages = {14},
opturl = {http://doi.acm.org/10.1145/2628136.2628143},
project = {http://www.cl.cam.ac.uk/~pes20/lem/},
pdf = {http://www.cl.cam.ac.uk/~pes20/lem/built-doc/lem-icfp-2014.pdf},
doi = {10.1145/2628136.2628143},
acmid = {2628143},
publisher = {ACM},
address = {New York, NY, USA},
optkeywords = {lem, proof assistants, real-world semantics, specification languages},
abstract = {
Recent years have seen remarkable successes in rigorous engineering: using mathematically rigorous semantic models (not just idealised calculi) of real-world processors, programming languages, protocols, and security mechanisms, for testing, proof, analysis, and design. Building these models is challenging, requiring experimentation, dialogue with vendors or standards bodies, and validation; their scale adds engineering issues akin to those of programming to the task of writing clear and usable mathematics. But language and tool support for specification is lacking. Proof assistants can be used but bring their own difficulties, and a model produced in one, perhaps requiring many person-years effort and maintained over an extended period, cannot be used by those familiar with another.
We introduce Lem, a language for engineering reusable large-scale semantic models. The Lem design takes inspiration both from functional programming languages and from proof assistants, and Lem definitions are translatable into OCaml for testing, Coq, HOL4, and Isabelle/HOL for proof, and LaTeX and HTML for presentation. This requires a delicate balance of expressiveness, careful library design, and implementation of transformations - akin to compilation, but subject to the constraint of producing usable and human-readable code for each target. Lem's effectiveness is demonstrated by its use in practice.
},
topic = {lem}
}
@inproceedings{BMNPS2015,
author = {Mark Batty and
Kayvan Memarian and
Kyndylan Nienhuis and
Jean Pichon{-}Pharabod and
Peter Sewell},
title = {The Problem of Programming Language Concurrency Semantics},
abstract = {Despite decades of research, we do not have a satisfactory concurrency semantics for any general-purpose programming language that aims to support concurrent systems code. The Java Memory Model has been shown to be unsound with respect to standard compiler optimisations, while the C/C++11 model is too weak, admitting undesirable thin-air executions. Our goal in this paper is to articulate this major open problem as clearly as is currently possible, showing how it arises from the combination of multiprocessor relaxed-memory behaviour and the desire to accommodate current compiler optimisations. We make several novel contributions that each shed some light on the problem, constraining the possible solutions and identifying new difficulties.},
conf = {ESOP 2015},
booktitle = {Programming Languages and Systems - 24th European Symposium on Programming,
Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2015, London, UK, April 11-18, 2015.
},
pages = {283--307},
year = {2015},
month = apr,
optcrossref = {DBLP:conf/esop/2015},
opturl = {http://dx.doi.org/10.1007/978-3-662-46669-8_12},
pdf = {http://www.cl.cam.ac.uk/~pes20/cpp/c_concurrency_challenges.pdf},
doi = {10.1007/978-3-662-46669-8_12},
timestamp = {Tue, 07 Apr 2015 15:19:02 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/esop/BattyMNPS15},
bibsource = {dblp computer science bibliography, http://dblp.org},
topic = {c11}
}
@inproceedings{nqsbTLS-sub,
author = {David Kaloper{-}Mersinjak and
Hannes Mehnert and
Anil Madhavapeddy and
Peter Sewell},
title = {Not-Quite-So-Broken {TLS:} Lessons in Re-Engineering a Security Protocol
Specification and Implementation},
abstract = {Transport Layer Security (TLS) implementations have a history of security flaws. The immediate causes of these are often programming errors, e.g.~in memory management, but the root causes are more fundamental: the challenges of interpreting the ambiguous prose specification, the complexities inherent in large APIs and code bases, inherently unsafe programming choices, and the impossibility of directly testing conformance between implementations and the specification.
We present \emph{nqsb-TLS}, the result of our re-engineered approach to security protocol specification and implementation that addresses these root causes. The same code serves dual roles: it is both a specification of TLS, executable as a test oracle to check conformance of traces from arbitrary implementations, and a usable implementation of TLS; a modular and declarative programming style provides clean separation between its components. Many security flaws are thus excluded by construction.
nqsb-TLS can be used in standalone applications, which we demonstrate with a messaging client, and can also be compiled into a Xen unikernel (a specialised virtual machine image) with a TCB that is 4\% of a standalone system running a standard Linux/OpenSSL stack, with all network traffic being handled in a memory-safe language; this supports applications including HTTPS, IMAP, Git, and Websocket clients and servers.
},
conf = {USENIX Security 2015},
booktitle = {24th {USENIX} Security Symposium, Washington,
D.C., USA},
pages = {223--238},
year = {2015},
month = aug,
optcrossref = {DBLP:conf/uss/2015},
url = {https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/kaloper-mersinjak},
project = {http://nqsb.io/},
pdf = {http://www.cl.cam.ac.uk/~pes20/nqsbtls-usenix-security15.pdf},
timestamp = {Thu, 20 Aug 2015 14:07:40 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/uss/Kaloper-Mersinjak15},
bibsource = {dblp computer science bibliography, http://dblp.org},
topic = {TLS}
}
@inproceedings{SibylFS-sub,
author = {Tom Ridge and
David Sheets and
Thomas Tuerk and
Andrea Giugliano and
Anil Madhavapeddy and
Peter Sewell},
title = {{SibylFS}: formal specification and oracle-based testing for {POSIX}
and real-world file systems},
abstract = {Systems depend critically on the behaviour of file systems, but that behaviour differs in many details, both between implementations and between each implementation and the POSIX (and other) prose specifications. Building robust and portable software requires understanding these details and differences, but there is currently no good way to systematically describe, investigate, or test file system behaviour across this complex multi-platform interface.
In this paper we show how to characterise the envelope of allowed
behaviour of file systems in a form that enables practical and highly
discriminating testing. We give a mathematically rigorous model of
file system behaviour, SibylFS, that specifies the range of allowed
behaviours of a file system for any sequence of the system calls
within our scope, and that can be used as a \emph{test oracle} to
decide whether an observed trace is allowed by the model, both for
validating the model and for testing file systems against it. SibylFS
is modular enough to not only describe POSIX, but also specific
Linux, OSX and FreeBSD behaviours. We complement the model
with an extensive test suite of over 21000 tests; this can be run on
a target file system and checked in less than 5 minutes, making it
usable in practice. Finally, we report experimental results for
around 40 configurations of many file systems, identifying many
differences and some serious flaws.
},
conf = {SOSP 2015},
booktitle = {Proceedings of the 25th Symposium on Operating Systems Principles,
Monterey, CA, USA},
pages = {38--53},
year = {2015},
month = oct,
optcrossref = {DBLP:conf/sosp/2015},
project = {http://sibylfs.io},
opturl = {http://doi.acm.org/10.1145/2815400.2815411},
pdf = {http://www.cl.cam.ac.uk/~pes20/SOSP15-paper102-submitted.pdf},
doi = {10.1145/2815400.2815411},
timestamp = {Fri, 02 Oct 2015 08:59:57 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/sosp/RidgeSTGMS15},
bibsource = {dblp computer science bibliography, http://dblp.org},
topic = {SibylFS}
}
@inproceedings{DBLP:conf/micro/GrayKMPSS15,
author = {Kathryn E. Gray and
Gabriel Kerneis and
Dominic P. Mulligan and
Christopher Pulte and
Susmit Sarkar and
Peter Sewell},
title = {An integrated concurrency and core-{ISA} architectural envelope definition,
and test oracle, for {IBM} {POWER} multiprocessors},
abstract = {Weakly consistent multiprocessors such as ARM and IBM POWER have been with us for decades, but their subtle programmer-visible concurrency behaviour remains challenging, both to implement and to use; the traditional architecture documentation, with its mix of prose and pseudocode, leaves much unclear.
In this paper we show how a precise architectural envelope model for such architectures can be defined, taking IBM POWER as our example. Our model specifies, for an arbitrary test program, the set of all its allowable executions, not just those of some particular implementation. The model integrates an operational concurrency model with an ISA model for the fixed-point non-vector user-mode instruction set (largely automatically derived from the vendor pseudocode, and expressed in a new ISA description language). The key question is the interface between these two: allowing all the required concurrency behaviour, without overcommitting to some particular microarchitectural implementation, requires a novel abstract structure.
Our model is expressed in a mathematically rigorous language that can be automatically translated to an executable test-oracle tool; this lets one either interactively explore or exhaustively compute the set of all allowed behaviours of intricate test cases, to provide a reference for hardware and software development.
},
conf = {MICRO 2015},
booktitle = {Proceedings of the 48th International Symposium on Microarchitecture,
, Waikiki, HI, USA},
pages = {635--646},
year = {2015},
month = dec,
optcrossref = {DBLP:conf/micro/2015},
opturl = {http://doi.acm.org/10.1145/2830772.2830775},
pdf = {http://www.cl.cam.ac.uk/~pes20/micro-48-2015.pdf},
doi = {10.1145/2830772.2830775},
timestamp = {Sun, 10 Jan 2016 12:42:56 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/micro/GrayKMPSS15},
bibsource = {dblp computer science bibliography, http://dblp.org},
topic = {Power_and_ARM},
topictwo = {ISA_semantics}
}
@inproceedings{PPS16,
author = {Jean Pichon{-}Pharabod and
Peter Sewell},
title = {A concurrency semantics for relaxed atomics that permits optimisation
and avoids thin-air executions},
abstract = {Despite much research on concurrent programming languages, especially for Java and C/C++, we still do not have a satisfactory definition of their semantics, one that admits all common optimisations without also admitting undesired behaviour. Especially problematic are the ``thin-air'' examples involving high-performance concurrent accesses, such as C/C++11 relaxed atomics. The C/C++11 model is in a per-candidate-execution style, and previous work has identified a tension between that and the fact that compiler optimisations do not operate over single candidate executions in isolation; rather, they operate over syntactic representations that represent all executions.
In this paper we propose a novel approach that circumvents this difficulty. We define a concurrency semantics for a core calculus, including relaxed-atomic and non-atomic accesses, and locks, that admits a wide range of optimisation while still forbidding the classic thin-air examples. It also addresses other problems relating to undefined behaviour.
The basic idea is to use an event-structure representation of the current state of each thread, capturing all of its potential executions, and to permit interleaving of execution and transformation steps over that to reflect optimisation (possibly dynamic) of the code. These are combined with a non-multi-copy-atomic storage subsystem, to reflect common hardware behaviour.
The semantics is defined in a mechanised and executable form, and designed to be implementable above current relaxed hardware and strong enough to support the programming idioms that C/C++11 does for this fragment. It offers a potential way forward for concurrent programming language semantics, beyond the current C/C++11 and Java models.
},
conf = {POPL 2016},
booktitle = {Proceedings of the 43rd Annual {ACM} {SIGPLAN-SIGACT} Symposium on
Principles of Programming Languages, St. Petersburg,
FL, USA, January 20 - 22, 2016},
pages = {622--633},
year = {2016},
month = jan,
optcrossref = {DBLP:conf/popl/2016},
opturl = {http://doi.acm.org/10.1145/2837614.2837616},
project = {http://www.cl.cam.ac.uk/~pes20/popl16-thinair},
pdf = {http://www.cl.cam.ac.uk/~jp622/popl16-thinair/a_concurrency_semantics.pdf},
doi = {10.1145/2837614.2837616},
timestamp = {Fri, 08 Jan 2016 18:18:25 +0100},
optbiburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/Pichon-Pharabod16},
optbibsource = {dblp computer science bibliography, http://dblp.org},
topic = {c11}
}
@inproceedings{DBLP:conf/popl/FlurGPSSMDS16,
author = {Shaked Flur and
Kathryn E. Gray and
Christopher Pulte and
Susmit Sarkar and
Ali Sezgin and
Luc Maranget and
Will Deacon and
Peter Sewell},
title = {Modelling the {ARMv8} architecture, operationally: concurrency and {ISA}},
abstract = {In this paper we develop semantics for key aspects of the ARMv8 multiprocessor architecture: the concurrency model and much of the 64-bit application-level instruction set (ISA). Our goal is to clarify what the range of architecturally allowable behaviour is, and thereby to support future work on formal verification, analysis, and testing of concurrent ARM software and hardware.
Establishing such models with high confidence is intrinsically difficult: it involves capturing the vendor's architectural intent, aspects of which (especially for concurrency) have not previously been precisely defined. We therefore first develop a concurrency model with a microarchitectural flavour, abstracting from many hardware implementation concerns but still close to hardware-designer intuition. This means it can be discussed in detail with ARM architects. We then develop a more abstract model, better suited for use as an architectural specification, which we prove sound w.r.t.~the first.
The instruction semantics involves further difficulties, handling the mass of detail and the subtle intensional information required to interface to the concurrency model. We have a novel ISA description language, with a lightweight dependent type system, letting us do both with a rather direct representation of the ARM reference manual instruction descriptions.
We build a tool from the combined semantics that lets one explore, either interactively or exhaustively, the full range of architecturally allowed behaviour, for litmus tests and (small) ELF executables. We prove correctness of some optimisations needed for tool performance.
We validate the models by discussion with ARM staff, and by comparison against ARM hardware behaviour, for ISA single- instruction tests and concurrent litmus tests.},
conf = {POPL 2016},
booktitle = {Proceedings of the 43rd Annual {ACM} {SIGPLAN-SIGACT} Symposium on
Principles of Programming Languages, St. Petersburg,
FL, USA },
pages = {608--621},
year = {2016},
month = jan,
optcrossref = {DBLP:conf/popl/2016},
opturl = {http://doi.acm.org/10.1145/2837614.2837615},
pdf = {http://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf},
project = {http://www.cl.cam.ac.uk/~sf502/popl16/index.html},
optproject = {http://www.cl.cam.ac.uk/~pes20/popl16-armv8/},
doi = {10.1145/2837614.2837615},
timestamp = {Fri, 08 Jan 2016 18:18:25 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/FlurGPSSMDS16},
bibsource = {dblp computer science bibliography, http://dblp.org},
topic = {Power_and_ARM},
topictwo = {ISA_semantics}
}
@misc{N2012,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {N2012: Clarifying the {C} memory object model},
howpublished = {ISO SC22 WG14 N2012, \url{http://www.cl.cam.ac.uk/~pes20/cerberus/notes64-wg14.html}},
html = {http://www.cl.cam.ac.uk/~pes20/cerberus/notes64-wg14.html},
month = mar,
year = 2016,
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2013,
optkey = {},
author = {David Chisnall and Justus Matthiesen and Kayvan Memarian and Kyndylan Nienhuis and Peter Sewell and Robert N. M. Watson},
title = {N2013: C memory object and value semantics: the space of de facto and {ISO} standards},
howpublished = {ISO SC22 WG14 N2013, \url{http://www.cl.cam.ac.uk/~pes20/cerberus/notes30.pdf}},
month = mar,
year = 2016,
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
pdf = {http://www.cl.cam.ac.uk/~pes20/cerberus/notes30.pdf},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2014,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {N2014: What is {C} in practice? ({Cerberus} survey v2): Analysis of Responses},
howpublished = {ISO SC22 WG14 N2014, \url{http://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html}},
month = mar,
year = 2016,
html = {http://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2015,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {N2015: What is {C} in practice? ({Cerberus} survey v2): Analysis of Responses -- with Comments},
howpublished = {ISO SC22 WG14 N2015, \url{http://www.cl.cam.ac.uk/~pes20/cerberus/analysis-2016-02-05-anon.txt}},
month = mar,
year = 2016,
txt = {http://www.cl.cam.ac.uk/~pes20/cerberus/analysis-2016-02-05-anon.txt},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@inproceedings{Cerberus-PLDI16,
author = {
Kayvan Memarian and
Justus Matthiesen and
James Lingard and
Kyndylan Nienhuis and
David Chisnall and
Robert N.M. Watson and
Peter Sewell
},
title = {Into the depths of {C}: elaborating the de facto standards},
abstract = {
C remains central to our computing infrastructure. It is notionally defined by ISO standards, but in reality the properties of C assumed by systems code and those implemented by compilers have diverged, both from the ISO standards and from each other, and none of these are clearly understood.
We make two contributions to help improve this error-prone situation. First, we describe an in-depth analysis of the design space for the semantics of pointers and memory in C as it is used in practice. We articulate many specific questions, build a suite of semantic test cases, gather experimental data from multiple implementations, and survey what C experts believe about the de facto standards. We identify questions where there is a consensus (either following ISO or differing) and where there are conflicts. We apply all this to an experimental C implemented above capability hardware. Second, we describe a formal model, Cerberus, for large parts of C. Cerberus is parameterised on its memory model; it is linkable either with a candidate de facto memory object model, under construction, or with an operational C11 concurrency model; it is defined by elaboration to a much simpler Core language for accessibility, and it is executable as a test oracle on small examples.
This should provide a solid basis for discussion of what mainstream C is now: what programmers and analysis tools can assume and what compilers aim to implement. Ultimately we hope it will be a step towards clear, consistent, and accepted semantics for the various use-cases of C.
},
optcrossref = {},
optkey = {},
conf = {PLDI 2016},
booktitle = {Proceedings of the 37th annual ACM SIGPLAN conference on Programming Language Design and Implementation},
optpages = {},
year = {2016},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = jun,
optorganization = {},
optpublisher = {},
note = {PLDI 2016 Distinguished Paper award},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
url = {http://doi.acm.org/10.1145/2908080.2908081},
doi = {10.1145/2908080.2908081},
pdf = {http://www.cl.cam.ac.uk/users/pes20/cerberus/pldi16.pdf},
optannote = {},
topic = {Cerberus},
topictwo = {cheri},
topicthree = {WG14},
recent = {true}
}
@misc{N2089,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {N2089: Clarifying Unspecified Values},
subtitle = {(Draft Defect Report or Proposal for C2x)},
howpublished = {ISO SC22 WG14 N2089, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2089.htm}},
month = sep,
year = 2016,
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2089.htm},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2090,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {N2090: Clarifying Pointer Provenance},
subtitle = {(Draft Defect Report or Proposal for C2x)},
howpublished = {ISO SC22 WG14 N2090, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2090.htm}},
month = sep,
year = 2016,
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2090.htm},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2091,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {N2091: Clarifying Trap Representations},
subtitle = {(Draft Defect Report or Proposal for C2x)},
howpublished = {ISO SC22 WG14 N2091, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2091.htm}},
month = sep,
year = 2016,
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2091.htm},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@inproceedings{kell_missing_2016,
author = {Stephen Kell and Dominic P. Mulligan and Peter Sewell},
title = {The missing link: explaining {ELF} static linking, semantically},
conf = {OOPSLA 2016},
booktitle = {Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications},
series = {OOPSLA 2016},
year = {2016},
month = nov,
location = {Amsterdam, The Netherlands},
numpages = {17},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Linking, formal specification, Executable and Linkable Format (ELF), theorem-proving},
abstract = {Beneath the surface, software usually depends on complex \emph{linker
behaviour} to work as intended. Even linking
\texttt{hello\_world.c} is surprisingly involved, and systems software
such as \texttt{libc} and operating system kernels rely on a host of
linker features. But linking is poorly understood by working
programmers and has largely been neglected by language researchers.
In this paper we survey the many use-cases that linkers support and
the poorly specified \emph{linker speak} by which they are controlled:
metadata in object files, command-line options, and linker-script
language. We provide the first validated formalisation of a realistic
executable and linkable format (ELF), and capture aspects of the
Application Binary Interfaces for four mainstream platforms (AArch64,
AMD64, Power64, and IA32). Using these, we develop an executable
specification of static linking, covering (among other things) enough to link
small C programs (we use the example of \textsf{bzip2}) into a correctly
running executable. We
provide our specification in Lem and Isabelle/HOL forms. This is the
first formal specification of mainstream linking. We have used the
Isabelle/HOL version to prove a sample
correctness property for one case of AMD64 ABI relocation,
demonstrating that the specification supports formal proof, and as a
first step towards the much more ambitious goal of verified linking.
Our work should enable several novel strands of research, including
linker-aware verified compilation and program analysis, and better
languages for controlling linking.
},
url = {http://doi.acm.org/10.1145/2983990.2983996},
doi = {10.1145/2983990.2983996},
pdf = {http://www.cl.cam.ac.uk/~pes20/rems/papers/oopsla-elf-linking-2016.pdf},
project = {https://github.com/rems-project/linksem},
topic = {linksem},
recent = {true}
}
@inproceedings{operational-semantics-c11-2016,
author = {Kyndylan Nienhuis and Kayvan Memarian and Peter Sewell},
title = {An operational semantics for {C/C++11} concurrency},
conf = {OOPSLA 2016},
booktitle = {Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications},
location = {Amsterdam, The Netherlands},
numpages = {18},
publisher = {ACM},
address = {New York, NY, USA},
month = nov,
year = {2016},
abstract = {The C/C++11 concurrency model balances two goals: it is relaxed enough to be efficiently implementable and (leaving aside the ``thin-air'' problem) it is strong enough to give useful guarantees to programmers. It is mathematically precise and has been used in verification research and compiler testing. However, the model is expressed in an axiomatic style, as predicates on complete candidate executions. This suffices for computing the set of allowed executions of a small litmus test, but it does not directly support the incremental construction of executions of larger programs. It is also at odds with conventional operational semantics, as used implicitly in the rest of the C/C++ standards.
Our main contribution is the development of an operational model for C/C++11 concurrency. This covers all the features of the previous formalised axiomatic model, and we have a mechanised proof that the two are equivalent, in Isabelle/HOL. We also integrate this semantics with an operational semantics for sequential C (described elsewhere); the combined semantics can incrementally execute programs in a small fragment of C.
Doing this uncovered several new aspects of the C/C++11 model: we show that one cannot build an equivalent operational model that simply follows program order, sequential consistent order, or the synchronises-with order. The first negative result is forced by hardware-observable behaviour, but the latter two are not, and so might be ameliorated by changing C/C++11. More generally, we hope that this work, with its focus on incremental construction of executions, will inform the future design of new concurrency models.},
url = {http://doi.acm.org/10.1145/2983990.2983997},
doi = {10.1145/2983990.2983997},
pdf = {http://www.cl.cam.ac.uk/~pes20/rems/papers/nienhuis-oopsla-2016.pdf},
topic = {c11},
recent = {true}
}
@inproceedings{mixed17,
author = {Shaked Flur and Susmit Sarkar and Christopher Pulte and Kyndylan Nienhuis and Luc Maranget and Kathryn E. Gray and Ali Sezgin and Mark Batty and Peter Sewell},
title = {Mixed-size Concurrency: {ARM}, {POWER}, {C/C++11}, and {SC}},
conf = {POPL 2017},
booktitle = {The 44st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
Programming Languages, Paris, France},
year = {2017},
month = jan,
pages = {429--442},
numpages = {14},
opturl = {http://doi.acm.org/10.1145/3009837.3009839},
doi = {10.1145/3009837.3009839},
project = {http://www.cl.cam.ac.uk/users/pes20/popl17/},
abstract = {Previous work on the semantics of relaxed shared-memory concurrency has only considered the case in which each load reads the data of exactly one store. In practice, however, multiprocessors support mixed-size accesses, and these are used by systems software and (to some degree) exposed at the C/C++ language level. A semantic foundation for software, therefore, has to address them.
We investigate the mixed-size behaviour of ARMv8 and IBM POWER architectures and implementations: by experiment, by developing semantic models, by testing the correspondence between these, and by discussion with ARM and IBM staff. This turns out to be surprisingly subtle, and on the way we have to revisit the fundamental concepts of coherence and sequential consistency, which change in this setting. In particular, we show that adding a memory barrier between each instruction does not restore sequential consistency. We go on to extend the C/C++11 model to support non-atomic mixed-size memory accesses.
This is a necessary step towards semantics for real-world shared-memory concurrent code, beyond litmus tests.
},
pdf = {http://www.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf},
topic = {Power_and_ARM},
topictwo = {ISA_semantics},
recent = {true}
}
@misc{relaxedtutorial2012,
optkey = {},
author = {Luc Maranget and Susmit Sarkar and Peter Sewell.},
title = {A Tutorial Introduction to the ARM and POWER Relaxed Memory Models},
opthowpublished = {},
month = oct,
year = {2012},
note = {Draft},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test7.pdf},
abstract = {ARM and IBM POWER multiprocessors have highly
\emph{relaxed} memory models: they make use of a range of hardware
optimisations that do not affect the observable behaviour of
sequential code but which are exposed to concurrent programmers, and
concurrent code may not execute in the way one intends unless
sufficient synchronisation, in the form of barriers, dependencies, and
load-reserve/store-conditional pairs, is present. In this tutorial we
explain some of the main issues that programmers should be aware of,
by example. The material is based on extensive experimental testing,
discussion with some of the designers, and formal models that aim to
capture the architectural intent (though we do not speak for the vendors). To keep this tutorial as accessible
as possible, we refer to our previous work for those details.},
topic = {Power_and_ARM}
}
@inproceedings{armv8-mca,
author = {Christopher Pulte and Shaked Flur and Will Deacon and Jon French and Susmit Sarkar and Peter Sewell},
title = {{Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8}},
optcrossref = {},
optkey = {},
conf = {POPL 2018},
booktitle = {Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages},
optpages = {},
year = {2018},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
doi = {10.1145/3158107},
month = jan,
optorganization = {},
optpublisher = {},
optnote = {Draft},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/armv8-mca/armv8-mca-draft.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/armv8-mca/},
abstract = {ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8. Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified by the potential benefits. In particular, the model was originally \emph{non-multicopy-atomic}: writes could become visible to some other threads before becoming visible to all --- but this has not been exploited in production implementations, the corresponding potential hardware optimisations are thought to have insufficient benefits in the ARM context, and it gives rise to subtle complications when combined with other ARMv8 features. The ARMv8 architecture has therefore been revised: it now has a multicopy-atomic model. It has also been simplified in other respects, including more straightforward notions of dependency, and the architecture now includes a formal concurrency model.
In this paper we detail these changes and discuss their motivation. We define two formal concurrency models: an operational one, simplifying the Flowing model of Flur et al., and the axiomatic model of the revised ARMv8 specification. The models were developed by an academic group and by ARM staff, respectively, and this extended collaboration partly motivated the above changes. We prove the equivalence of the two models. The operational model is integrated into an executable exploration tool with new web interface, demonstrated by exhaustively checking the possible behaviours of a loop-unrolled version of a Linux kernel lock implementation, a previously known bug due to unprevented speculation, and a fixed version.},
topic = {Power_and_ARM},
topictwo = {ISA_semantics},
recent = {true}
}
@inproceedings{cerberus-popl2019,
author = {Kayvan Memarian and Victor B. F. Gomes and Brooks Davis and Stephen Kell and Alexander Richardson and Robert N. M. Watson and Peter Sewell},
title = {Exploring {C} Semantics and Pointer Provenance},
optcrossref = {},
optkey = {},
conf = {POPL 2019},
booktitle = {Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages},
optbooktitle = {},
year = {2019},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {Proc. ACM Program. Lang. 3, POPL, Article 67. Also available as ISO/IEC JTC1/SC22/WG14 N2311 },
optannote = {},
doi = {10.1145/3290380},
pdf = {http://www.cl.cam.ac.uk/users/pes20/cerberus/cerberus-popl2019.pdf},
supplementarymaterial = {http://www.cl.cam.ac.uk/users/pes20/cerberus/supplementary-material-popl2019},
topic = {Cerberus},
topictwo = {cheri},
topicthree = {WG14},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
abstract = {The semantics of pointers and memory objects in C has been a vexed question for many years. C values cannot be treated as either purely abstract or purely concrete entities: the language exposes their representations, but compiler optimisations rely on analyses that reason about provenance and initialisation status, not just runtime representations. The ISO WG14 standard leaves much of this unclear, and in some respects differs with de facto standard usage --- which itself is difficult to investigate.
In this paper we explore the possible source-language semantics for memory objects and pointers, in ISO C and in C as it is used and implemented in practice, focussing especially on pointer provenance. We aim to, as far as possible, reconcile the ISO C standard, mainstream compiler behaviour, and the semantics relied on by the corpus of existing C code. We present two coherent proposals, tracking provenance via integers and not; both address many design questions. We highlight some pros and cons and open questions, and illustrate the discussion with a library of test cases. We make our semantics executable as a test oracle, integrating it with the Cerberus semantics for much of the rest of C, which we have made substantially more complete and robust, and equipped with a web-interface GUI. This allows us to experimentally assess our proposals on those test cases. To assess their viability with respect to larger bodies of C code, we analyse the changes required and the resulting behaviour for a port of FreeBSD to CHERI, a research architecture supporting hardware capabilities, which (roughly speaking) traps on the memory safety violations which our proposals deem undefined behaviour. We also develop a new runtime instrumentation tool to detect possible provenance violations in normal C code, and apply it to some of the SPEC benchmarks. We compare our proposal with a source-language variant of the twin-allocation LLVM semantics proposal of Lee et al. Finally, we describe ongoing interactions with WG14, exploring how our proposals could be incorporated into the ISO standard.
},
recent = {true}
}
@inproceedings{sail-popl2019,
author = {Alasdair Armstrong and Thomas Bauereiss and Brian Campbell and Alastair Reid and Kathryn E. Gray and Robert M. Norton and Prashanth Mundkur and Mark Wassell and Jon French and Christopher Pulte and Shaked Flur and Ian Stark and Neel Krishnaswami and Peter Sewell},
title = {{ISA} Semantics for {ARMv8-A, RISC-V, and CHERI-MIPS}},
optcrossref = {},
optkey = {},
conf = {POPL 2019},
booktitle = {Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages},
optbooktitle = {},
year = {2019},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {Proc. ACM Program. Lang. 3, POPL, Article 71},
optnote = {},
optannote = {},
doi = {10.1145/3290384},
abstract = {Architecture specifications notionally define the fundamental interface between hardware and software: the envelope of allowed behaviour for processor implementations, and the basic assumptions for software development and verification. But in practice, they are typically prose and pseudocode documents, not rigorous or executable artifacts, leaving software and verification on shaky ground.
In this paper, we present rigorous semantic models for the sequential behaviour of large parts of the mainstream ARMv8-A, RISC-V, and MIPS architectures, and the research CHERI-MIPS architecture, that are complete enough to boot operating systems, variously Linux, FreeBSD, or seL4. Our ARMv8-A models are automatically translated from authoritative ARM-internal definitions, and (in one variant) tested against the ARM Architecture Validation Suite.
We do this using a custom language for ISA semantics, Sail, with a lightweight dependent type system, that supports automatic generation of emulator code in C and OCaml, and automatic generation of proof-assistant definitions for Isabelle, HOL4, and (currently only for MIPS) Coq. We use the former for validation, and to assess specification coverage. To demonstrate the usability of the latter, we prove (in Isabelle) correctness of a purely functional characterisation of ARMv8-A address translation. We moreover integrate the RISC-V model into the RMEM tool for (user-mode) relaxed-memory concurrency exploration. We prove (on paper) the soundness of the core Sail type system.
We thereby take a big step towards making the architectural abstraction actually well-defined, establishing foundations for verification and reasoning.
},
pdf = {http://www.cl.cam.ac.uk/users/pes20/sail/sail-popl2019.pdf},
supplementarymaterial = {http://www.cl.cam.ac.uk/users/pes20/sail/popl2019.html},
topic = {ISA_semantics},
topictwo = {cheri},
project = {http://www.cl.cam.ac.uk/~pes20/sail/},
recent = {true}
}
@misc{N2219,
optkey = {},
author = {Kayvan Memarian and Victor Gomes and Peter Sewell},
title = {N2219: Clarifying Pointer Provenance (Q1-Q20) v3},
howpublished = {ISO SC22 WG14 N2219, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2219.htm}},
month = mar,
year = 2018,
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2219.htm},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2220,
optkey = {},
author = {Kayvan Memarian and Victor Gomes and Peter Sewell},
title = {N2220: Clarifying Trap Representations (Q47) v3},
howpublished = {ISO SC22 WG14 N2220, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2220.htm}},
month = mar,
year = 2018,
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2220.htm},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2221,
optkey = {},
author = {Kayvan Memarian and Victor Gomes and Peter Sewell},
title = {N2221: Clarifying Unspecified Values (Q48-Q59) v3},
howpublished = {ISO SC22 WG14 N2221, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2221.htm}},
month = mar,
year = 2018,
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2221.htm},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2222,
optkey = {},
author = {Kayvan Memarian and Victor Gomes and Peter Sewell},
title = {N2222: Further Pointer Issues (Q21-Q46)},
howpublished = {ISO SC22 WG14 N2222, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2222.htm}},
month = mar,
year = 2018,
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2222.htm},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2223,
optkey = {},
author = {Kayvan Memarian and Victor Gomes and Peter Sewell},
title = {N2223: Clarifying the C Memory Object Model: Introduction to N2219 -- N2222},
howpublished = {ISO SC22 WG14 N2223, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2223.htm}},
month = mar,
year = 2018,
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2223.htm},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2263,
optkey = {},
author = {Kayvan Memarian and Victor Gomes and Peter Sewell},
title = {N2263: Clarifying Pointer Provenance (Q1-Q20) v4},
howpublished = {ISO SC22 WG14 N2263, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2263.htm}},
month = mar,
year = 2018,
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2263.htm},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{Sew99pi,
optkey = {},
author = {Peter Sewell},
title = {A Brief Introduction to Applied $\pi$},
opthowpublished = {},
year = {1999},
month = jan,
note = {Lecture notes for the Mathfit Instructional Meeting on Recent Advances in
Semantics and Types for Concurrency: Theory and Practice, July 1998.},
optannote = {},
url = {http://www.cl.cam.ac.uk/~pes20/mathfit.html},
topic = {pi_tutorial}
}
@misc{udp-model,
optkey = {SWN01},
author = {Michael Norrish and Andrei Serjantov and Peter Sewell and Keith Wansbrough},
title = {Timing {UDP}: The {HOL} Model},
opthowpublished = {},
month = jul,
year = {2001},
note = {\url{http://www.cl.cam.ac.uk/users/pes20/Netsem/index.html}},
url = {http://www.cl.cam.ac.uk/users/pes20/Netsem/index.html},
optannote = {},
topic = {netsem},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}
@misc{SW04,
optkey = {},
author = {Peter Sewell and Keith Wansbrough},
title = {Applied Semantics: Specifying and Developing Abstractions for Distributed Computation (Grand Challenge Discussion Paper -- {GC2}, {GC4}, and {GC6})},
howpublished = {Position paper for Grand Challenge meeting (Newcastle). 5pp},
optmonth = {},
year = {2004},
optnote = {},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/users/pes20/grandchallenge2004.pdf},
topic = {misc}
}
@misc{netsem04a,
optkey = {},
author = {Steven Bishop and Matthew Fairbairn and Michael Norrish and Peter Sewell and Keith
Wansbrough},
title = {The {TCP} Specification: A Quick Introduction},
opthowpublished = {},
optmonth = {},
year = {2004},
optnote = {},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/quickstart.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/Netsem/quickstart.ps},
topic = {netsem},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}
@misc{acute-release-0-50-1,
optnote = {acute-release},
author = {Peter Sewell and
James J. Leifer and
Keith Wansbrough and
Mair Allen-Williams and
Zappa Nardelli, Francesco and
Pierre Habouzit and
Viktor Vafeiadis},
title = {Source release of the {Acute} system},
optinstitution = {University of Cambridge Computer Laboratory},
year = {2005},
optkey = {},
opttype = {},
optnumber = {},
optaddress = {},
month = jan,
note = {Available from \url{http://www.cl.cam.ac.uk/users/pes20/acute/distro/acute-0.50-1-src.tar.gz}},
optannote = {},
url = {http://www.cl.cam.ac.uk/users/pes20/acute/distro/acute-0.50-1-src.tar.gz},
topic = {distributed_types},
project = {http://www.cl.cam.ac.uk/~pes20/acute/}
}
@misc{TCP:poster,
optkey = {},
author = {Steven Bishop and Matthew Fairbairn and Michael Norrish and
Peter Sewell and Michael Smith and Keith Wansbrough},
title = {An approximation to the real TCP state diagram},
opthowpublished = {},
month = mar,
year = {2005},
note = {This is a poster with a version of the "TCP state diagram" extracted from the specification. It is rather more complete than the usual diagram, but is still a very abstract and simplified view of the state space of our specification. It is intended to be printed at A1 size or bigger.},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/poster.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/Netsem/poster.ps},
topic = {netsem},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}
@misc{hashcaml-release,
optkey = {},
author = {John Billings and Peter Sewell and Mark Shinwell and Rok Strni\v sa},
title = {{HashCaml} release, version 3.09.1-alpha-795},
opthowpublished = {},
month = apr,
year = {2006},
note = {\url{http://www.cl.cam.ac.uk/~pes20/hashcaml/index.html}},
url = {http://www.cl.cam.ac.uk/~pes20/hashcaml/index.html},
optannote = {},
topic = {distributed_types},
project = {http://www.cl.cam.ac.uk/~pes20/hashcaml/}
}
@misc{ott-release,
optkey = {},
author = {Peter Sewell and Zappa Nardelli, Francesco},
title = {Ott release, version 0.10.9},
opthowpublished = {},
month = aug,
year = {2007},
note = {\url{http://www.cl.cam.ac.uk/~pes20/ott/}},
url = {http://www.cl.cam.ac.uk/~pes20/ott/},
project = {http://www.cl.cam.ac.uk/~pes20/ott/},
optannote = {},
topic = {ott}
}
@misc{ppcmem-release,
optkey = {},
author = {Jade Alglave and Luc Maranget and Pankaj Pawan and Susmit Sarkar and Peter Sewell and Derek Williams and Zappa Nardelli, Francesco},
title = {ppcmem},
opthowpublished = {},
optmonth = aug,
year = {2011},
note = {\url{http://www.cl.cam.ac.uk/~pes20/ppcmem/}},
url = {http://www.cl.cam.ac.uk/~pes20/ppcmem/},
optannote = {},
opttopic = {Power_and_ARM}
}
@misc{epsrcfoc1,
optkey = {},
author = {Peter Sewell},
title = {{Fundamentals of Computing} Research: a perspective from the ground},
opthowpublished = {},
month = feb,
year = 2011,
note = {Briefing note for EPSRC ICT team, with input from Anuj Dawar, Chris Hankin, Tom Melham, Faron Moller, Peter O'Hearn, and Phil Wadler. 6pp},
optannote = {}
}
@misc{epsrcfoc2,
optkey = {},
author = {Peter O'Hearn},
title = {Responses to {FoC} Questions},
opthowpublished = {},
month = feb,
year = {2011},
note = {Briefing note for EPSRC ICT team, with contributions and input from
Anuj Dawar, Philippa Gardner, Chris Hankin, Tom Melham, Faron Moller,
Andrew Pitts, Uday Reddy, Peter Sewell, and Philip Wadler. 11pp},
optannote = {}
}
@misc{compcertTSO-release,
author = {Jaroslav \v{S}ev\v{c}\'{\i}k and Viktor Vafeiadis and Zappa Nardelli, Francesco and Suresh Jagannathan and Peter Sewell},
optkey = {},
optauthor = {},
title = {{CompCert-TSO} release, Version 1.12},
opthowpublished = {},
month = aug,
year = {2011},
note = {\url{http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/index.html}},
url = {http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/index.html},
optannote = {},
project = {https://www.cl.cam.ac.uk/~pes20/CompCertTSO},
topic = {CompCertTSO}
}
@misc{ott-release-20-3,
optkey = {},
author = {Peter Sewell and Zappa Nardelli, Francesco },
title = {Ott release, version 0.20.3},
opthowpublished = {},
month = aug,
year = {2011},
note = {\url{http://www.cl.cam.ac.uk/~pes20/ott/}},
url = {http://www.cl.cam.ac.uk/~pes20/ott/},
optannote = {},
project = {http://www.cl.cam.ac.uk/~pes20/ott/}
}
@misc{lem-sw,
author = { Dominic Mulligan and Thomas Tuerk and Scott Owens and Kathryn E. Gray and Peter Sewell},
title = {Lem},
year = 2014,
note = {\url{http://www.cl.cam.ac.uk/~pes20/lem/}},
url = {http://www.cl.cam.ac.uk/~pes20/lem/},
project = {http://www.cl.cam.ac.uk/~pes20/lem/},
opttopic = {lem}
}
@misc{HCSS2015-Flur,
optkey = {},
author = {S. Flur and K. Gray and G. Kerneis and D. Mulligan and C. Pulte and S. Sarkar and P. Sewell},
title = {Rigorous Architectural Modelling for Production Multiprocessors},
opthowpublished = {},
month = may,
year = 2015,
note = {Presentation at HCSS 2015: the Fifteenth Annual
High Confidence Software and Systems Conference},
optannote = {},
abstract = {
Processor architectures are critical interfaces in computing, but they
are typically defined only by prose and pseudocode documentation.
This is especially problematic for the subtle concurrency behaviour of
weakly consistent multiprocessors such as ARM and IBM POWER: the
traditional documentation does not define precisely what
programmer-observable behaviour is (and is not) allowed for concurrent
code; it is not executable as a test oracle for pre-Silicon or
post-Silicon hardware testing; it is not executable as an emulator for
software testing; and it is not mathematically rigorous enough to
serve as a foundation for software verification.
We present a rigorous architectural envelope model for IBM POWER
multiprocessors, and similar work in progress for ARM, that aims to
support all of these for small-but-intricate test cases, integrating
an operational concurrency model with an ISA model for the sequential
behaviour of a substantial fragment of the user-mode instruction set
(largely automatically derived from the vendor pseudocode, and
expressed in a new ISA description language). The key question is the
interface between these two: we have to allow all the required
relaxed-memory behaviour, without overcommitting to some particular
microarchitectural model. Our models can be automatically translated
into executable code, which, combined with front-ends for concurrency
litmus tests and ELF executables, can interactively or exhaustively
explore all the allowed behaviours of small test cases.
},
opttopic = {Power_and_ARM}
}
@misc{HCSS2015-Memarian,
optkey = {},
author = {Kayvan Memarian and Kyndylan Nienhuis and Justus Matthiesen and James Lingard and Peter Sewell},
title = {Cerberus: towards an Executable Semantics for Sequential and Concurrent {C11}},
opthowpublished = {},
month = may,
year = 2015,
note = {Presentation at HCSS 2015: the Fifteenth Annual
High Confidence Software and Systems Conference},
optmonth = {},
optyear = {},
optannote = {},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
abstract = {C remains central to our computing infrastructure but still lacks a
clear and complete semantics. Programmers lack tools to explore the
range of behaviours they should expect; compiler development lacks
test oracles; and formal verification and analysis must make
(explicitly or implicitly) many choices about the specific C they
target.
We describe Cerberus, a semantics for a substantial fragment of C11.
Its thread-local semantics is factored via an elaboration into a
simpler Core language, to make it conceptually and mathematically
tractable. This is integrated with an operational model for C11
concurrency, with a mechanised proof of equivalence to the axiomatic
C11 model of Batty et al. The front-end includes a parser that
closely follows the C11 standard grammar and a typechecker. Cerberus
is executable, to explore all behaviours or single paths of test
programs, and it supports proof, as shown by a preliminary experiment
in translation validation for the front-end of Clang, for very simple
programs. This is a step towards a clear, consistent, and unambiguous
semantics for C.
}
}
@misc{HCSS-Kaloper,
optkey = {},
author = {David Kaloper Mer{\v{s}}injak and Hannes Mehnert and Anil Madhavapeddy and Peter Sewell},
title = {Not-quite-so-broken {TLS}: lessons in re-engineering a security protocol
specification and implementation},
opthowpublished = {},
month = may,
year = 2015,
note = {Presentation at HCSS 2015: the Fifteenth Annual
High Confidence Software and Systems Conference},
optmonth = {},
optyear = {},
optnote = {},
optannote = {},
project = {http://nqsb.io/},
abstract = {Transport Layer Security (TLS) implementations have a history of
security flaws. The immediate causes of these range from simple
programming errors, such as memory management, to subtle violations of
the protocol logic. Deeper causes can be seen in the challenges of
interpreting the ambiguous prose specification, the complexities
inherent in large APIs and code bases, unsafe performance-oriented
programming choices, and the impossibility of directly testing
conformance between implementations and the specification.
We present nqsb-TLS, the result of our re-engineering approach
to improve the quality of security protocol implementations. The same
code serves dual roles: it is both a specification of TLS, executable
as a test oracle to check conformance of traces from arbitrary
implementations, and a secure and usable executable implementation of
TLS. nqsb-TLS employs a modular and declarative programming
style that also allows it to be compiled into a Xen unikernel (a
specialised virtual machine image) with a TCB that is 2.5\% of a
standalone system running a standard Linux/OpenSSL stack, with all
network traffic being handled in a memory-safe language.
nqsb-TLS focuses on protocol-level interoperability, and makes
no effort to be compatible with existing (and often poorly designed)
library APIs such as OpenSSL. The higher-level API in nqsb-TLS
makes it harder to misuse the library, and is demonstrated via several
unikernel applications ranging over HTTPS, IMAP, Git, Websocket clients
and servers.
}
}
@misc{sail-sw,
author = {Kathryn E. Gray and Peter Sewell and Christopher Pulte and Shaked Flur and Robert Norton-Wright},
title = {The {Sail} instruction-set semantics specification language},
year = 2016,
note = {\url{http://www.cl.cam.ac.uk/~pes20/sail/}},
url = {http://www.cl.cam.ac.uk/~pes20/sail/},
topic = {Power_and_ARM},
optrecent = {true}
}
@article{tcp3draft,
optkey = {},
author = {Steve Bishop and Matthew Fairbairn and Hannes Mehnert and Michael Norrish and Tom Ridge and Peter Sewell and Michael Smith and Keith Wansbrough},
title = {Engineering with Logic: Rigorous Test-Oracle Specification and Validation for {TCP/IP} and the {Sockets API}},
journal = {J. ACM},
opthowpublished = {},
optmonth = {},
issue_date = {December 2018},
volume = {66},
number = {1},
month = dec,
year = {2018},
issn = {0004-5411},
pages = {1:1--1:77},
articleno = {1},
numpages = {77},
url = {http://doi.acm.org/10.1145/3243650},
doi = {10.1145/3243650},
acmid = {3243650},
publisher = {ACM},
optaddress = {New York, NY, USA},
optnote = {Accepted for publication 2018-08},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/Netsem/index.html},
recent = {true},
topic = {netsem},
abstract = {
Conventional computer engineering relies on test-and-debug development
processes, with the behaviour of common interfaces described (at best)
with prose specification documents. But prose specifications cannot be used in
test-and-debug development in any automated way, and prose is a poor
medium for expressing complex (and loose) specifications.
The TCP/IP protocols and Sockets API are a good example of this:
they play a vital role in modern communication and computation, and
interoperability between implementations is essential. But what
exactly they are is surprisingly obscure: their original development
focussed on ``rough consensus and running code'', augmented by prose
RFC specifications that do not precisely define what it means for an
implementation to be correct. Ultimately, the actual standard is the
de facto one of the common implementations, including, for example,
the 15\,000--20\,000 lines of the BSD implementation --- optimised and
multithreaded C code, time-dependent, with asynchronous event
handlers, intertwined with the operating system, and
security-critical.
This paper reports on work done in the \emph{Netsem} project to
develop lightweight mathematically rigorous techniques that can be
applied to such systems: to specify their behaviour precisely (but
loosely enough to permit the required implementation variation) and to
test whether these specifications and the implementations correspond,
with specifications that are \emph{executable as test oracles}.
We developed post-hoc specifications of TCP, UDP, and the Sockets API, both of
the service that they provide to applications (in terms of TCP
bidirectional stream connections), and of the internal operation of
the protocol (in terms of TCP segments and UDP datagrams), together
with a testable abstraction function relating the two. These specifications
are rigorous, detailed, readable, with broad coverage, and are rather
accurate. Working within a general-purpose proof assistant (HOL4), we
developed \emph{language idioms} (within higher-order logic) in which
to write the specifications: operational semantics with
nondeterminism, time, system calls, monadic relational programming,
etc. We followed an \emph{experimental semantics} approach,
validating the specifications against several thousand traces captured
from three implementations (FreeBSD, Linux, and WinXP). Many
differences between these were identified, and a number of bugs.
Validation was done using a special-purpose \emph{symbolic model
checker} programmed above HOL4.
Having demonstrated that our logic-based engineering techniques
suffice for handling real-world protocols, we argue that similar
techniques could be applied to future critical software infrastructure
at design time, leading to cleaner designs and (via
specification-based testing) more robust and predictable
implementations. In cases where specification looseness can be
controlled, this should be possible with lightweight techniques,
without the need for a general-purpose proof assistant, at relatively
little cost.
}
}
@inproceedings{sail-arw18,
author = { Alasdair Armstrong and
Thomas Bauereiss and
Brian Campbell and
Shaked Flur and
Kathryn E. Gray and
Prashanth Mundkur and
Robert M.~Norton and
Christopher Pulte and
Alastair Reid and
Peter Sewell and
Ian Stark and
Mark Wassell},
title = {Detailed Models of Instruction Set Architectures: From
Pseudocode to Formal Semantics},
optcrossref = {},
optkey = {},
conf = {Automated Reasoning Workshop (ARW) 2018},
booktitle = {Proc. Automated Reasoning Workshop},
year = {2018},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
pages = {23--24},
month = apr,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {Two-page abstract. Proceedings available at \url{https://www.cl.cam.ac.uk/events/arw2018/arw2018-proc.pdf}},
optannote = {},
topic = {ISA_semantics},
topic2 = {cheri},
project = {http://www.cl.cam.ac.uk/~pes20/sail/},
pdf = {http://www.cl.cam.ac.uk/~pes20/sail/2018-04-12-arw-paper.pdf},
abstract = {Processor instruction set architectures (ISAs) are typically specified using a mixture of prose and
pseudocode. We present ongoing work on expressing such specifications rigorously and automatically trans-
lating them to interactive theorem prover definitions, making them amenable to mechanised proof. Our ISA
descriptions are written in Sail—a custom ISA specification language designed to support idioms from var-
ious processor vendor’s pseudocode, with lightweight dependent typing for bitvectors, targeting a variety of
use cases including sequential and concurrent ISA semantics. From Sail we aim to portably generate usable
theorem prover definitions for multiple provers, including Isabelle, HOL4, and Coq. We are focusing on the
full ARMv8.3-A specification, CHERI-MIPS, and RISC-V, together with fragments of IBM POWER and x86.}
}
@inproceedings{sail-arw18-minisail,
author = {Alasdair Armstrong and Neel Krishnaswami and Peter Sewell and Mark Wassell},
title = {Formalisation of {MiniSail} in the {Isabelle} Theorem Prover},
optcrossref = {},
optkey = {},
conf = {Automated Reasoning Workshop (ARW) 2018},
booktitle = {Proc. Automated Reasoning Workshop},
year = {2018},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
pages = {27--28},
month = apr,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {Two-page abstract. Proceedings available at \url{https://www.cl.cam.ac.uk/events/arw2018/arw2018-proc.pdf}},
optannote = {},
topic = {ISA_semantics},
project = {http://www.cl.cam.ac.uk/~pes20/sail/},
pdf = {http://www.cl.cam.ac.uk/~pes20/sail/arw18_mpew2.pdf},
abstract = {Sail is a language used to model instruction set architectures. It has an imperative syntax and a
dependent type system. We formalise a core calculus of the language in the Isabelle theorem prover describing
the language syntax, substitution, the type system and operational semantics. A number of classic theorems
such as preservation and progress are then proved. The purpose of this formalisation is to ensure that the full
language is built on sound foundations and to provide a platform for the generation of the implementation of
a type checker and evaluator for the language.}
}
@inproceedings{cheri-arw18,
author = {Kyndylan Nienhuis and Alexandre Joannou and Peter Sewell},
title = {Proving security properties of {CHERI-MIPS}},
optcrossref = {},
optkey = {},
conf = {Automated Reasoning Workshop (ARW) 2018},
booktitle = {Proc. Automated Reasoning Workshop},
year = {2018},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
pages = {18},
month = apr,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {Two-page abstract. Proceedings available at \url{https://www.cl.cam.ac.uk/events/arw2018/arw2018-proc.pdf}},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/cheri/cheri-arw18.pdf},
topic = {cheri},
abstract = { CHERI-MIPS is an instruction set architecture that
provides hardware support for secure encapsulation
and fine-grained memory protection. The guarantees
it intends to offer are described in high-level
prose, which makes it difficult to understand what
they precisely are, whether they are true, and
whether they indeed provide memory protection. We
describe ongoing work on proposing formal
definitions of these guarantees and proving that
they are true.}
}
@book{riscv-20181221-Public-Review-draft,
optkey = {},
editor = {Andrew Waterman and Krste Asanovi{\'{c}}},
optauthor = {},
title = {The {RISC-V} Instruction Set Manual {Volume I: Unprivileged ISA}},
howpublished = {\url{https://github.com/riscv/riscv-isa-manual/releases/tag/draft-20181227-c6741cb}},
month = dec,
year = 2018,
note = {Document Version {20181221-Public-Review-draft. Contributors: Arvind, Krste Asanovi\'{c}, Rimas Avi\v{z}ienis, Jacob Bachmeyer, Christopher
F. Batten, Allen J. Baum, Alex Bradbury, Scott Beamer, Preston Briggs,
Christopher Celio, Chuanhua Chang, David Chisnall, Paul Clayton, Palmer
Dabbelt, Roger Espasa, Shaked Flur, Stefan Freudenberger, Jan Gray, Michael
Hamburg, John Hauser, David Horner, Bruce Hoult, Alexandre Joannou,
Olof Johansson, Ben Keller, Yunsup Lee,
Paul Loewenstein, Daniel Lustig, Yatin Manerkar, Luc Maranget, Margaret
Martonosi, Joseph Myers, Vijayanand Nagarajan, Rishiyur Nikhil, Jonas
Oberhauser, Stefan O'Rear, Albert Ou, John Ousterhout, David Patterson,
Christopher Pulte, Jose Renau, Colin Schmidt, Peter Sewell, Susmit Sarkar,
Michael Taylor, Wesley Terpstra, Matt Thomas, Tommy Thorn, Caroline Trippel,
Ray VanDeWalker, Muralidaran Vijayaraghavan, Megan Wachs, Andrew Waterman,
Robert Watson, Derek Williams, Andrew Wright, Reinoud Zandijk, and Sizhuo Zhang}},
optannote = {},
topic = {Power_and_ARM},
recent = {true},
pdf = {\url{https://github.com/riscv/riscv-isa-manual/releases/download/draft-20181227-c6741cb/riscv-spec.pdf}}
}
@misc{rems-summary,
optkey = {},
author = {Peter Sewell},
title = {{REMS: Rigorous Engineering for Mainstream Systems. Summary 2013-03 -- 2019-01}},
opthowpublished = {},
month = feb,
year = {2019},
optnote = {},
pdf = {http://www.cl.cam.ac.uk/users/pes20/rems/report-2019-web.pdf},
optannote = {},
abstract = {REMS, \emph{Rigorous Engineering for Mainstream Systems}, is an
EPSRC-funded Programme Grant (2013--2020, \pounds 5.6M, Cambridge,
Imperial, and Edinburgh) to explore how
we can use rigorous mathematics to improve engineering practice for
mainstream computer systems, to make them more robust and secure:
broadly, to \emph{``create the intellectual and software tools to apply
semantics and verification at the heart of mainstream system
engineering''}.
%
REMS brings together an unusual combination of researchers to achieve this: in
architecture, operating systems, security, and networks, and in
semantics, programming languages, and mechanised reasoning.
%
Our work is in close collaboration with a range of industrial
partners, including ARM, IBM, and the standards committees for C,
JavaScript, WebAssembly, and TLS.
We are building accurate full-scale mathematical models of some of the
key computational abstractions (processor architectures, programming
languages, concurrent OS interfaces, and network protocols), studying
how this can best be done, and investigating how such models can be used
for new verification research and in new systems and programming
language research. For many of these abstractions, our work has
exposed and clarified fundamental questions about what the
abstractions are, and provided tools to let them be explored. Supporting all this, we are also developing new
specification tools. Most of our models and tools are publicly
available under permissive open-source licences.
This note summarises REMS progress to date. Highlights include
models and tools for the production ARMv8-A architecture (including
user-mode concurrency and the full ISA), the RISC-V and research
CHERI-MIPS architectures, the C, JavaScript, and WebAssembly
programming languages, ELF linking, POSIX filesystems, the TLS and TCP
protocols, and extensive work on concurrency verification.
},
recent = {true}
}
@inproceedings{cheriABIsub,
optkey = {},
author = {Brooks Davis and
Robert N. M. Watson and
Alexander Richardson and
Peter G. Neumann and
Simon W. Moore and
John Baldwin and
David Chisnall and
James Clarke and
Nathaniel Wesley Filardo and
Khilan Gudka and
Alexandre Joannou and
Ben Laurie and
A. Theodore Markettos and
J. Edward Maste and
Alfredo Mazzinghi and
Edward Tomasz Napierala and
Robert M. Norton and
Michael Roe and
Peter Sewell and
Stacey Son and
Jonathan Woodruff},
title = {{CheriABI}: Enforcing Valid Pointer Provenance and Minimizing
Pointer Privilege in the {POSIX C} Run-time Environment},
opthowpublished = {Submitted for publication},
conf = {ASPLOS 2019},
booktitle = {\textbf{ASPLOS 2019}: the 24th ACM International Conference on Architectural Support for Programming Languages and Operating Systems},
month = apr,
year = {2019},
note = {Best paper award},
url = {http://doi.acm.org/10.1145/3297858.3304042},
doi = {10.1145/3297858.3304042},
acmid = {3304042},
publisher = {ACM},
optannote = {},
abstract = {The CHERI architecture allows pointers to be implemented as
capabilities (rather than integer virtual addresses) in a manner that
is compatible with, and strengthens, the
semantics of the C language.
In addition to the spatial protections offered by conventional fat pointers,
CHERI capabilities offer strong integrity, enforced provenance validity, and
access monotonicity.
The stronger guarantees of these architectural capabilities must be reconciled with the real-world behavior of operating systems, run-time environments, and applications.
When the process model, user-kernel interactions, dynamic linking, and memory
management are all considered, we observe that simple derivation of architectural capabilities is insufficient to describe appropriate access to memory.
We bridge this conceptual gap with a notional \emph{abstract capability} that
describes the accesses that should be allowed at a given point in execution,
whether in the kernel or userspace.
To investigate this notion at scale, we describe the first adaptation of a
full C-language operating system (FreeBSD) with an enterprise database
(PostgreSQL) for complete spatial and referential memory safety.
We show that awareness of abstract capabilities, coupled with CHERI
architectural capabilities, can provide more complete protection, strong
compatibility, and acceptable performance overhead compared with the pre-CHERI
baseline and software-only approaches.
Our observations also have potentially significant implications for other
mitigation techniques.},
pdf = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201904-asplos-cheriabi.pdf},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
recent = {true}
}
@misc{N2362,
optkey = {},
author = {Jens Gustedt and Peter Sewell and Kayvan Memarian and Victor B. F. Gomes and Martin Uecker},
title = {N2362: Moving to a provenance-aware memory object model for {C}},
howpublished = {ISO/IEC JTC1/SC22/WG14 N2362 v1, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2362.pdf}},
month = mar,
year = 2019,
pdf = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2362.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2363,
optkey = {},
author = {Peter Sewell and Kayvan Memarian and Victor B. F. Gomes and Jens Gustedt and Martin Uecker},
title = {N2363: {C} provenance semantics: examples},
howpublished = {ISO/IEC JTC1/SC22/WG14 N2363, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2363.pdf}},
month = apr,
year = 2019,
pdf = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2363.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2364,
optkey = {},
author = {Peter Sewell and Kayvan Memarian and Victor B. F. Gomes},
title = {N2364: {C provenance semantics: detailed semantics (for PNVI-plain, PNVI address-exposed, PNVI address-exposed user-disambiguation, and PVI models)}},
howpublished = {ISO/IEC JTC1/SC22/WG14 N2364, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2364.pdf}},
month = apr,
year = 2019,
pdf = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2364.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2369,
optkey = {},
author = {Paul E. McKenney and Maged Michael and Peter Sewell},
title = {{N2369: Pointer lifetime-end zap}},
howpublished = {ISO/IEC JTC1/SC22/WG14 N2369, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2369.pdf}},
month = apr,
year = 2019,
pdf = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2369.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@misc{N2378,
optkey = {},
author = {Peter Sewell and Kayvan Memarian and Victor B. F. Gomes and Jens Gustedt and Martin Uecker},
title = {N2378: {C} provenance semantics: slides (extracts from N2363)},
howpublished = {ISO/IEC JTC1/SC22/WG14 N2378 v1, \url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2378.pdf}},
month = apr,
year = 2019,
pdf = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2378.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {WG14}
}
@inproceedings{cerberusBMC,
author = {Stella Lau and Victor B. F. Gomes and Kayvan Memarian and Jean Pichon-Pharabod and Peter Sewell},
title = {{Cerberus-BMC}: a Principled Reference Semantics and Exploration
Tool for Concurrent and Sequential {C}},
optcrossref = {},
optkey = {},
conf = {CAV 2019},
booktitle = {Proc. 31st International Conference on Computer-Aided Verification},
optpages = {},
year = {2019},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = jul,
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/users/pes20/cerberus/bmc-cerberus.pdf},
topic = {Cerberus},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
abstract = {C remains central to our infrastructure, making verification of C code
an essential and much-researched topic, but the semantics of C is
remarkably complex, and important aspects of it are still unsettled,
leaving programmers and verification tool builders on shaky
ground.
This paper describes a tool, Cerberus-BMC, that for the first time
provides a principled reference semantics that simultaneously supports
(1) a choice of concurrency memory model (including substantial
fragments of the C11, RC11, and Linux kernel memory models), (2) a modern memory object model,
and (3) a well-validated thread-local semantics for a large fragment
of the language.
The tool should be useful for C programmers, compiler writers,
verification tool builders, and members of the C/C++ standards committees.
},
recent = {true}
}
@techreport{UCAM-CL-TR-927,
author = {Watson, Robert N. M. and Neumann, Peter G. and Woodruff,
Jonathan and Roe, Michael and Almatary, Hesham and
Anderson, Jonathan and Baldwin, John and Chisnall, David
and Davis, Brooks and Filardo, Nathaniel Wesley and
Joannou, Alexandre and Laurie, Ben and Markettos, A.
Theodore and Moore, Simon W. and Murdoch, Steven J. and
Nienhuis, Kyndylan and Norton, Robert and Richardson, Alex
and Rugg, Peter and Sewell, Peter and Son, Stacey and Xia,
Hongyan},
title = {{Capability Hardware Enhanced RISC Instructions: CHERI
Instruction-Set Architecture (Version 7)}},
year = 2019,
month = jun,
pdf = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-927.pdf},
institution = {University of Cambridge, Computer Laboratory},
number = {UCAM-CL-TR-927},
topic = {CHERI},
abstract = {This technical report describes CHERI ISAv7, the seventh version of the
Capability Hardware Enhanced RISC Instructions (CHERI) Instruction-Set
Architecture (ISA)
being developed by SRI International and the University of Cambridge.
This design captures nine years of research, development, experimentation,
refinement, formal analysis, and validation through hardware and software
implementation.
CHERI ISAv7 is a substantial enhancement to prior ISA versions.
We differentiate an architecture-neutral protection model vs.
architecture-specific instantiations in 64-bit MIPS, 64-bit RISC-V, and
x86-64.
We have defined a new CHERI Concentrate compression model.
CHERI-RISC-V is more substantially elaborated.
A new compartment-ID register assists in resisting microarchitectural
side-channel attacks.
Experimental features include linear capabilities, capability coloring,
temporal memory safety, and 64-bit capabilities for 32-bit architectures.
CHERI is a {\em hybrid capability-system architecture} that adds new
capability-system primitives to commodity 64-bit RISC ISAs, enabling software
to efficiently implement {\em fine-grained memory protection} and {\em
scalable software compartmentalization}.
Design goals include incremental adoptability within current ISAs and
software stacks, low performance overhead for memory protection, significant
performance improvements for software compartmentalization, formal grounding,
and programmer-friendly underpinnings.
We have focused on providing strong, non-probabilistic, efficient
architectural foundations for the principles of \textit{least privilege} and
\textit{intentional use} in the execution of software at multiple levels of
abstraction, preventing and mitigating vulnerabilities.
The CHERI system architecture purposefully addresses known performance and
robustness gaps in commodity ISAs that hinder the adoption of more secure
programming models centered around the principle of least privilege.
To this end, CHERI blends traditional paged virtual memory with an
in-address-space capability model that includes capability registers,
capability instructions, and tagged memory.
CHERI builds on the C-language fat-pointer literature: its capabilities can
describe fine-grained regions of memory, and can be substituted for data or
code pointers in generated code, protecting data and also improving
control-flow robustness.
Strong capability integrity and monotonicity properties allow the CHERI model
to express a variety of protection properties, from enforcing valid C-language
pointer provenance and bounds checking to implementing the isolation and
controlled communication structures required for software
compartmentalization.
CHERI's hybrid capability-system approach, inspired by the Capsicum security
model, allows incremental adoption of capability-oriented design: software
implementations that are more robust and resilient can be deployed where they
are most needed, while leaving less critical software largely unmodified, but
nevertheless suitably constrained to be incapable of having adverse effects.
Potential deployment scenarios include low-level software Trusted Computing
Bases (TCBs) such as separation kernels, hypervisors, and operating-system
kernels, as well as userspace TCBs such as language runtimes and web browsers.
We also see potential early-use scenarios around particularly high-risk
software libraries (such as data compression, protocol parsing, and image
processing), which are concentrations of both complex and historically
vulnerability-prone code exposed to untrustworthy data sources, while leaving
containing applications unchanged.
},
recent = {true}
}
This file was generated by bibtex2html 1.98.