@misc{rems-summary,
optkey = {},
author = {Peter Sewell},
title = {{REMS: Rigorous Engineering for Mainstream Systems. Summary 2013-03 -- 2019-01}},
opthowpublished = {},
month = jan,
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.
}
}
@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},
booktitle = {\textbf{ICFP 2014}: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming},
conf = {ICFP 2014},
year = {2014},
month = sep,
isbn = {978-1-4503-2873-9},
location = {Gothenburg, Sweden},
pages = {175--188},
numpages = {14},
url = {http://doi.acm.org/10.1145/2628136.2628143},
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.
}
}
@inproceedings{ITP-sub,
author = {Anthony C. J. Fox},
title = {Improved Tool Support for Machine-Code Decompilation in {HOL4}},
abstract = {The HOL4 interactive theorem prover provides a sound logical environment for reasoning about machine-code programs. The rigour of HOL's LCF-style kernel naturally guarantees very high levels of assurance, but it does present challenges when it comes implementing efficient proof tools. This paper presents improvements that have been made to our methodology for soundly \emph{decompiling} machine-code programs to functions expressed in HOL logic. These advancements have been facilitated by the development of a domain specific language, called L3, for the specification of Instruction Set Architectures (ISAs). As a result of these improvements, decompilation is faster (on average by one to two orders of magnitude), the instruction set specifications are easier to write, and the proof tools are easier to maintain.
},
booktitle = {{\textbf{ITP 2015}}:Interactive Theorem Proving - 6th International Conference, Nanjing, China},
conf = {ITP 2015},
pages = {187--202},
year = {2015},
month = aug,
optcrossref = {DBLP:conf/itp/2015},
url = {http://dx.doi.org/10.1007/978-3-319-22102-1_12},
pdf = {http://www.cl.cam.ac.uk/~acjf3/papers/itp15.pdf},
doi = {10.1007/978-3-319-22102-1_12},
timestamp = {Mon, 24 Aug 2015 16:29:06 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/itp/Fox15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@misc{BasileMPRI,
optkey = {},
author = {Basile Clement},
title = {Running programming language specifications},
opthowpublished = {},
month = aug,
year = 2014,
note = {MPRI report},
conf = {MPRI report},
optannote = {}
}
@inproceedings{PittsAM:deptta,
author = {A. M. Pitts and J. Matthiesen and J. Derikx},
title = {A Dependent Type Theory with Abstractable Names},
booktitle = {\textbf{LSFA 2014}: Proceedings of the 9th Workshop on Logical and
Semantic Frameworks, with Applications},
conf = {LSFA 2014},
year = 2015,
month = apr,
editor = {I. Mackie and M. Ayala-Rincon},
volume = 312,
series = {Electronic Notes in Theoretical Computer Science},
pages = {19--50},
doi = {http://dx.doi.org/10.1016/j.entcs.2015.04.003},
pdf = {https://www.repository.cam.ac.uk/bitstream/handle/1810/247863/Pitts_et_al-2015-Electronic_Notes_in_Theoretical_Computer_Science.pdf?sequence=1},
abstract = {This paper describes a version of Martin-Löf's dependent type theory extended with names and constructs for freshness and name-abstraction derived from the theory of nominal sets. We aim for a type theory for computing and proving (via a Curry-Howard correspondence) with syntactic structures which captures familiar, but informal, "nameful" practices when dealing with binders.},
publisher = {Elsevier}
}
@inproceedings{skeletons2018,
title = {Skeletal Semantics and their Interpretations},
author = {Bodin, Martin and Gardner, Philippa and Jensen, Thomas and Schmitt, Alan},
conf = {POPL 2019},
booktitle = {\textbf{POPL 2019}: Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages},
year = {2019},
month = jan,
optnote = {Submitted for publication},
abstract = {Many meta-languages have been proposed for writing rule-based operational semantics, in order to provide general interpreters and analysis tools. We take a different approach. We develop a meta-language for a skeletal semantics of a language, where each skeleton describes the complete semantic behaviour of a language construct. We define a general notion of interpretation, which provides a systematic and language-independent way of deriving semantic judgements from the skeletal semantics. We provide four generic interpretations of our skeletal semantics to yield: a simple well-formedness interpretation; a concrete interpretation; an abstract interpretation; and a constraint generator for flow-sensitive analysis. We prove general consistency results, establishing that the concrete and abstract interpretations are consistent and that any solution to the constraints generated by the constraint generator must be a correct abstract semantics.},
pdf = {http://skeletons.inria.fr/popl2019/skeletons.pdf}
}
@inproceedings{rems-fmics14,
title = {Randomised Testing of a Microprocessor Model Using {SMT}-Solver State Generation},
author = {Brian Campbell and Ian Stark},
booktitle = {\textbf{FMICS 2014}: Formal Methods for Industrial Critical Systems},
conf = {FMICS 2014},
year = 2014,
month = sep,
editor = {Fr{\'{e}}d{\'{e}}ric Lang and Francesco Flammini},
volume = 8718,
series = {Lecture Notes in Computer Science},
pages = {185--199},
publisher = {Springer},
doi = {10.1007/978-3-319-10702-8_13},
slides = {rems/fmics-m0-talk.pdf},
preprint = {rems/fmics2014.pdf},
pdf = {http://homepages.inf.ed.ac.uk/bcampbe2/rems/fmics2014.pdf},
preprintnote = {The final publication is available at link.springer.com},
abstract = {We validate a HOL4 model of the ARM Cortex-M0 microcontroller core by testing the model's behaviour on randomly chosen
instructions against a real chip.
The model and our intended application involve precise timing information about instruction execution, but the implementations are pipelined,
so checking the behaviour of single instructions would not give us sufficient confidence in the model. Thus we test the model using sequences
of randomly chosen instructions.
The main challenge is to meet the constraints on the initial and intermediate execution states: we must ensure that memory accesses are in
range and that we respect restrictions on the instructions. By careful
transformation of these constraints an off-the-shelf SMT solver can be
used to find suitable states for executing test sequences.
}
}
@article{rems-scico15,
author = {Brian Campbell and Ian Stark},
title = {Randomised Testing of a Microprocessor Model Using {SMT}-Solver State Generation},
journal = {\textbf{Sci. Comput. Program.}},
volume = 118,
pages = {60--76},
year = 2016,
month = mar,
issn = {0167-6423},
doi = {10.1016/j.scico.2015.10.012},
pdf = {http://homepages.inf.ed.ac.uk/bcampbe2/rems/scico2015.pdf},
abstract = {We validate a HOL4 model of the ARM Cortex-M0 microcontroller core by testing the model’s behaviour on randomly chosen instructions against real chips from several manufacturers.
The model and our intended application involve precise timing information about instruction execution, but the implementations are pipelined, so checking the behaviour of single instructions would not give us sufficient confidence in the model. Thus we test the model using sequences of randomly chosen instructions.
The main challenge is to meet the constraints on the initial and intermediate execution states: we must ensure that memory accesses are in range and that we respect restrictions on the instructions. By careful transformation of these constraints an off-the-shelf SMT solver can be used to find suitable states for executing test sequences. We also use additional constraints to test our hypotheses about the timing anomalies encountered.}
}
@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.
}
}
@inproceedings{DBLP:conf/asplos/AlglaveBDGKPSW15,
author = {Jade Alglave and
Mark Batty and
Alastair F. Donaldson and
Ganesh Gopalakrishnan and
Jeroen Ketema and
Daniel Poetzl and
Tyler Sorensen and
John Wickerson},
title = {{GPU} Concurrency: Weak Behaviours and Programming Assumptions},
booktitle = {\textbf{ASPLOS 2015}: Proceedings of the Twentieth International Conference on Architectural
Support for Programming Languages and Operating Systems, Istanbul, Turkey},
conf = {ASPLOS 2015},
pages = {577--591},
year = {2015},
month = mar,
optcrossref = {DBLP:conf/asplos/2015},
url = {http://doi.acm.org/10.1145/2694344.2694391},
doi = {10.1145/2694344.2694391},
timestamp = {Thu, 26 Feb 2015 17:21:18 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/asplos/AlglaveBDGKPSW15},
bibsource = {dblp computer science bibliography, http://dblp.org},
abstract = {
Concurrency is pervasive and perplexing, particularly on graphics processing units (GPUs). Current specifications of languages and hardware are inconclusive; thus programmers often rely on folklore assumptions when writing software.
To remedy this state of affairs, we conducted a large empirical study of the concurrent behaviour of deployed GPUs. Armed with litmus tests (i.e. short concurrent programs), we questioned the assumptions in programming guides and vendor documentation about the guarantees provided by hardware. We developed a tool to generate thousands of litmus tests and run them under stressful workloads. We observed a litany of previously elusive weak behaviours, and exposed folklore beliefs about GPU programming---often supported by official tutorials---as false.
As a way forward, we propose a model of Nvidia GPU hardware, which correctly models every behaviour witnessed in our experiments. The model is a variant of SPARC Relaxed Memory Order (RMO), structured following the GPU concurrency hierarchy.
}
}
@inproceedings{CHERI-Oakland,
author = {Robert N. M. Watson and Jonathan Woodruff and Peter G. Neumann and Simon W. Moore and Jonathan Anderson and David Chisnall and Nirav Dave and Brooks Davis and Khilan Gudka and Ben Laurie and Steven J. Murdoch and Robert Norton and Michael Roe and Stacey Son and Munraj Vadera},
title = {{CHERI}: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization},
optcrossref = {},
optkey = {},
booktitle = {\textbf{Security and Privacy 2015}: {Proceedings of the 36th IEEE Symposium on Security and Privacy (``Oakland'')}},
conf = {Security and Privacy 2015},
optpages = {},
year = {2015},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = may,
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
doi = {http://dx.doi.org/10.1109/SP.2015.9},
pdf = {http://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201505-oakland2015-cheri-compartmentalization.pdf},
abstract = {CHERI extends a conventional RISC Instruction-Set Architecture, compiler, and operating system to support
fine-grained, capability-based memory protection to mitigate
memory-related vulnerabilities in C-language TCBs. We describe
how CHERI capabilities can also underpin a hardware-software
object-capability model for application compartmentalization
that can mitigate broader classes of attack. Prototyped as an
extension to the open-source 64-bit BERI RISC FPGA softcore processor, FreeBSD operating system, and LLVM compiler,
we demonstrate multiple orders-of-magnitude improvement in
scalability, simplified programmability, and resulting tangible
security benefits as compared to compartmentalization based on
pure Memory-Management Unit (MMU) designs. We evaluate
incrementally deployable CHERI-based compartmentalization
using several real-world UNIX libraries and applications.
}
}
@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.
},
booktitle = {\textbf{MICRO 2015}: Proceedings of the 48th International Symposium on Microarchitecture,
, Waikiki, HI, USA},
conf = {MICRO 2015},
pages = {635--646},
year = {2015},
month = dec,
optcrossref = {DBLP:conf/micro/2015},
url = {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}
}
@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.},
booktitle = {\textbf{POPL 2016}: Proceedings of the 43rd Annual {ACM} {SIGPLAN-SIGACT} Symposium on
Principles of Programming Languages, St. Petersburg,
FL, USA },
conf = {POPL 2016},
pages = {608--621},
year = {2016},
month = jan,
optcrossref = {DBLP:conf/popl/2016},
url = {http://doi.acm.org/10.1145/2837614.2837615},
pdf = {http://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf},
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}
}
@inproceedings{DBLP:conf/memocode/NaylorM15,
author = {Matthew Naylor and
Simon W. Moore},
title = {A generic synthesisable test bench},
booktitle = {\textbf{MEMOCODE 2015}: {ACM/IEEE} International Conference on Formal
Methods and Models
for Codesign, Austin, TX, USA},
conf = {MEMOCODE 2015},
pages = {128--137},
year = {2015},
month = sep,
url = {http://dx.doi.org/10.1109/MEMCOD.2015.7340479},
doi = {10.1109/MEMCOD.2015.7340479},
timestamp = {Tue, 08 Dec 2015 17:08:30 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/memocode/NaylorM15},
bibsource = {dblp computer science bibliography, http://dblp.org},
pdf = {http://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201509-memocode2015-bluecheck.pdf},
abstract = {
Writing test benches is one of the most frequently-performed tasks in
the hardware development process. The ability to reuse common
test bench features is therefore key to productivity. In this paper,
we present a generic test bench, parameterised by a
specification of correctness, which can be used to test any
design. Our test bench provides several important features, including
automatic test-sequence generation and shrinking of counter-examples,
and is fully synthesisable, allowing rigorous testing on FPGA as well
as in simulation. The approach is easy to use, cheap to implement,
and encourages the formal specification of hardware components through
the reward of automatic testing and simple failure cases.
}
}
@techreport{UCAM-CL-TR-876,
author = {Watson, Robert N. M. and Neumann, Peter G. and Woodruff,
Jonathan and Roe, Michael and Anderson, Jonathan and
Chisnall, David and Davis, Brooks and Joannou, Alexandre
and Laurie, Ben and Moore, Simon W. and Murdoch, Steven J.
and Norton, Robert and Son, Stacey},
title = {{Capability Hardware Enhanced RISC Instructions: CHERI
Instruction-Set Architecture}},
year = 2015,
month = sep,
pdf = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-876.pdf},
institution = {University of Cambridge, Computer Laboratory},
number = {UCAM-CL-TR-876},
abstract = {This technical report describes CHERI ISAv4, the fourth version of the Capability Hardware Enhanced RISC Instructions (CHERI) Instruction-Set Architecture (ISA). CHERI is being developed by SRI International and the University of Cambridge. This design captures four years of research, development, refinement, formal analysis, and testing, and is a substantial enhancement to the ISA version described in UCAM-CL-TR-850. Key improvements lie in tighter C-language integration, and more mature support for software object-capability models; these changes result from experience gained in adapting substantial software stacks to run on prototype hardware.
The CHERI instruction set is based on a hybrid capability-system architecture that adds new capability-system primitives to a commodity 64-bit RISC ISA enabling software to efficiently implement fine-grained memory protection and a hardware-software object-capability security model. These extensions support incrementally adoptable, high-performance, formally based, programmer-friendly underpinnings for fine-grained software decomposition and compartmentalization, motivated by and capable of enforcing the principle of least privilege.
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 a per-address-space capability model that includes capability registers, capability instructions, and tagged memory that have been added to the 64-bit MIPS ISA via a new capability coprocessor. CHERI also learns from the C-language fat-pointer literature: CHERI capabilities can describe not only regions of memory, but can also capture C pointer semantics allowing capabilities to be substituted for pointers in generated code.
CHERI’s hybrid system approach, inspired by the Capsicum security model, allows incremental adoption of capability-oriented software 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. For example, we are focusing conversion efforts on low-level TCB components of the system: separation kernels, hypervisors, operating system kernels, language runtimes, and userspace TCBs such as web browsers. Likewise, we see early-use scenarios (such as data compression, protocol parsing, image processing, and video processing) that relate to particularly high-risk software libraries, which are concentrations of both complex and historically vulnerability-prone code combined with untrustworthy data sources, while leaving containing applications unchanged.
This report describes the CHERI Instruction-Set Architecture (ISA) and design, and provides reference documentation and potential memory models, along with their requirements. It also briefly addresses the CHERI system hardware-software architecture, documenting our current thinking on integrating programming languages and operating systems with the CHERI hardware.}
}
@techreport{UCAM-CL-TR-877,
author = {Watson, Robert N. M. and Chisnall, David and Davis, Brooks
and Koszek, Wojciech and Moore, Simon W. and Murdoch,
Steven J. and Neumann, Peter G. and Woodruff, Jonathan},
title = {{Capability Hardware Enhanced RISC Instructions: CHERI
Programmer's Guide}},
year = 2015,
month = sep,
pdf = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-877.pdf},
institution = {University of Cambridge, Computer Laboratory},
number = {UCAM-CL-TR-877},
abstract = {The CHERI Programmer's Guide documents the software environment for the Capability Hardware Enhanced RISC Instructions (CHERI) prototype developed by SRI International and the
University of Cambridge. The Guide is targeted at hardware and software developers working
with capability-enhanced software. It describes how to use the CHERI Clang/LLVM compiler
suite and CheriBSD operating system -- versions of the off-the-shelf LLVM suite and FreeBSD
operating system adapted to use CHERI’s protection features -- as well as implementation details of both.}
}
@inproceedings{NaylorFMCAD2016,
author = {M. Naylor and S. W. Moore and A. Mujumdar},
booktitle = {\textbf{FMCAD 2016}: Formal Methods in Computer-Aided Design},
conf = {FMCAD 2016},
title = {A Consistency Checker for Memory Subsystem Traces},
year = {2016},
month = sep,
abstract = {Verifying the memory subsystem in a modern
shared-memory multiprocessor is a big challenge. Optimized
implementations are highly sophisticated, yet must provide subtle
consistency and liveness guarantees for the correct execution of
concurrent programs. We present a tool that supports efficient
specification-based testing of the memory subsystem against a
range of formally specified consistency models. Our tool operates
directly on the memory subsystem interface, promoting a compositional
approach to system-on-chip verification, and can be
used to search for simple failure cases – assisting rapid debug. It
has recently been incorporated into the development flows of two
open-source implementations -- Berkeley’s Rocket Chip (RISCV)
and Cambridge’s BERI (MIPS) -- where it has uncovered a
number of serious bugs.},
pdf = {http://www.cl.cam.ac.uk/~pes20/rems/papers/fmcad2016-camera-ready.pdf},
doi = {http://dx.doi.org/10.17863/CAM.4451}
}
@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}},
booktitle = {\textbf{POPL 2017}: The 44st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
Programming Languages, Paris, France},
conf = {POPL 2017},
year = {2017},
month = jan,
pages = {429--442},
numpages = {14},
url = {http://doi.acm.org/10.1145/3009837.3009839},
doi = {10.1145/3009837.3009839},
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}
}
@article{Watson2015,
author = {Robert N.M. Watson and Robert M. Norton and Jonathan Woodruff
and Simon W. Moore and Peter G. Neumann and Jonathan Anderson and
David Chisnall and Brooks Davis and Ben Laurie and Michael Roe and
Nirav H. Dave and Khilan Gudka and Alexandre Joannou and
A. Theodore Markettos and Ed Maste and Steven J. Murdoch and Colin Rothwell
and Stacey D. Son and Munraj Vadera},
title = {Fast Protection-Domain Crossing in the {CHERI} Capability-System
Architecture},
journal = {IEEE Micro},
volume = {36},
number = {5},
pages = {38--49},
month = sep,
year = 2016,
doi = {10.1109/MM.2016.84},
pdf = {http://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=7723791},
abstract = {Capability Hardware Enhanced RISC Instructions (CHERI) supplement
the conventional memory management unit (MMU) with instruction-set architecture
(ISA) extensions that implement a capability system model in the address space.
CHERI can also underpin a hardware-software object-capability model for
scalable application compartmentalization that can mitigate broader classes of
attack. This article describes ISA additions to CHERI that support fast
protection-domain switching, not only in terms of low cycle count, but also
efficient memory sharing with mutual distrust. The authors propose ISA support
for sealed capabilities, hardware-assisted checking during protection-domain
switching, a lightweight capability flow-control model, and fast register
clearing, while retaining the flexibility of a software-defined
protection-domain transition model. They validate this approach through a
full-system experimental design, including ISA extensions, a field-programmable
gate array prototype (implemented in Bluespec SystemVerilog), and a software
stack including an OS (based on FreeBSD), compiler (based on LLVM), software
compartmentalization model, and open-source applications.}
}
@inproceedings{rems-fmcad16,
title = {Extracting Behaviour from an Executable Instruction Set Model},
author = {Brian Campbell and Ian Stark},
booktitle = {\textbf{FMCAD 2016}: Formal Methods in Computer-Aided Design},
conf = {FMCAD 2016},
year = 2016,
month = oct,
editor = {Ruzica Piskac and Muralidhar Talupur},
pages = {33--40},
isbn = {978-0-9835678-6-8},
pdf = {http://homepages.inf.ed.ac.uk/bcampbe2/rems/fmcad16.pdf},
note = {Full proceedings \url{http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/proceedings/fmcad-2016-proceedings.pdf}},
abstract = {Presenting large formal instruction set models as executable functions makes them accessible to engineers and useful for less formal purposes such as simulation. However, it is more difficult to extract information about the behaviour of individual instructions for reasoning. We present a method which combines symbolic evaluation and symbolic execution techniques to provide a rule-based view of instruction behaviour, with particular application to automatic test generation for large MIPS-like models.}
}
@techreport{UCAM-CL-TR-907,
author = {Watson, Robert N. M. and Neumann, Peter G. and Woodruff,
Jonathan and Roe, Michael and Anderson, Jonathan and
Baldwin, John and Chisnall, David and Davis, Brooks and
Joannou, Alexandre and Laurie, Ben and Moore, Simon W. and
Murdoch, Steven J. and Norton, Robert and Son, Stacey and
Xia, Hongyan},
title = {{Capability Hardware Enhanced RISC Instructions: CHERI
Instruction-Set Architecture (Version 6)}},
year = 2017,
month = apr,
pdf = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-907.pdf},
institution = {University of Cambridge, Computer Laboratory},
number = {UCAM-CL-TR-907},
abstract = {This technical report describes CHERI ISAv6, the sixth 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 seven years of research, development, experimentation, refinement, formal analysis, and validation through hardware and software implementation. CHERI ISAv6 is a substantial enhancement to prior ISA versions: it introduces support for kernel-mode compartmentalization, jump-based rather than exception-based domain transition, architecture-abstracted and efficient tag restoration, and more efficient generated code. A new chapter addresses potential applications of the CHERI model to the RISC-V and x86-64 ISAs, previously described relative only to the 64-bit MIPS ISA. CHERI ISAv6 better explains our design rationale and research methodology.
CHERI is a hybrid capability-system architecture that adds new capability-system primitives to a commodity 64-bit RISC ISA enabling software to efficiently implement fine-grained memory protection and scalable software compartmentalization. Design goals have included 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. Throughout, we have focused on providing strong and efficient architectural foundations for the principles of least privilege and 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 C-language fat-pointer literature: its capabilities 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. Likewise, we see early-use scenarios (such as data compression, protocol parsing, and image processing) that relate to particularly high-risk software libraries, which are concentrations of both complex and historically vulnerability-prone code exposed to untrustworthy data sources, while leaving containing applications unchanged.}
}
@inproceedings{Joannou2017Tags,
author = {Alexandre Joannou and Jonathan Woodruff and Robert Kovacsics and Simon W. Moore and Alex Bradbury and Hongyan Xia and Robert N. M. Watson and David Chisnall and Michael Roe and Brooks Davis and Edward Napierala and John Baldwin and Khilan Gudka and Peter G. Neumann and Alfredo Mazzinghi and Alex Richardson and Stacey Son and A. Theodore Markettos},
title = {Efficient Tagged Memory},
booktitle = {\textbf{ICCD 2017}: IEEE 35th International Conference on Computer Design},
conf = {ICCD 2017},
year = {2017},
month = nov,
url = {},
doi = {},
pdf = {http://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201711-iccd2017-efficient-tags.pdf},
abstract = {We characterize the cache behavior of an in-memory tag table and demonstrate that an optimized implementation can typically achieve a near-zero memory traffic overhead. Both industry and academia have repeatedly demonstrated tagged memory as a key mechanism to enable enforcement of power- ful security invariants, including capabilities, pointer integrity, watchpoints, and information-flow tracking. A single-bit tag shadowspace is the most commonly proposed requirement, as one bit is the minimum metadata needed to distinguish between an untyped data word and any number of new hardware- enforced types. We survey various tag shadowspace approaches and identify their common requirements and positive features of their implementations. To avoid non-standard memory widths, we identify the most practical implementation for tag storage to be an in-memory table managed next to the DRAM controller. We characterize the caching performance of such a tag table and demonstrate a DRAM traffic overhead below 5\% for the vast majority of applications. We identify spatial locality on a page scale as the primary factor that enables surprisingly high table cache-ability. We then demonstrate tag-table compression for a set of common applications. A hierarchical structure with elegantly simple optimizations reduces DRAM traffic overhead to below 1% for most applications. These insights and optimizations pave the way for commercial applications making use of single-bit tags stored in commodity memory.}
}
@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}},
booktitle = {\textbf{POPL 2018}},
conf = {POPL 2018},
optcrossref = {},
optkey = {},
optbooktitle = {},
optpages = {},
year = {2018},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = jan,
issn = {2475-1421},
pages = {19:1--19:29},
articleno = {19},
numpages = {29},
url = {http://doi.acm.org/10.1145/3158107},
doi = {10.1145/3158107},
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},
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 = {\textbf{POPL 2019}: 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},
topic = {ISA_semantics},
project = {http://www.cl.cam.ac.uk/~pes20/sail/},
recent = {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/download/draft-20181227-c6741cb/riscv-spec.pdf}},
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}},
pdf = {https://github.com/riscv/riscv-isa-manual/releases/download/draft-20181227-c6741cb/riscv-spec.pdf},
optannote = {}
}
@inproceedings{promisingARM,
author = {Christopher Pulte and
Jean Pichon-Pharabod and
Jeehoon Kang and
Sung-Hwan Lee and
Chung-Kil Hur},
abstract = {For ARMv8 and RISC-V, there are concurrency models in two styles,
extensionally equivalent: axiomatic models, expressing the concurrency
semantics in terms of global properties of complete executions; and
operational models, that compute incrementally. The latter are in an
abstract microarchitectural style: they execute each instruction in
multiple steps, out-of-order and with explicit branch speculation.
This similarity to hardware implementations has been important in
developing the models and in establishing confidence, but involves
complexity that, for programming and model-checking, one would prefer
to avoid.
We present new more abstract operational models for ARMv8 and RISC-V,
and an exploration tool based on them. The models compute the allowed
concurrency behaviours incrementally based on thread-local conditions
and are significantly simpler than the existing operational models:
executing instructions in a single step and (with the exception of
early writes) in program order, and without branch speculation. We
prove the models equivalent to the existing ARMv8 and RISC-V axiomatic
models in Coq. The exploration tool is the first such tool for ARMv8
and RISC-V fast enough for exhaustively checking the concurrency
behaviour of a number of interesting examples. We demonstrate using
the tool for checking several standard concurrent datastructure and
lock implementations, and for interactively stepping through
model-allowed executions for debugging.},
url = {https://www.cl.cam.ac.uk/~cp526/promising_camera_ready.pdf},
title = {Promising-{ARM/RISC-V}: A Simpler and Faster Operational Concurrency Model},
conf = {PLDI 2019},
booktitle = {\textbf{PLDI 2019:} Proceedings of the 40th ACM SIGPLAN Conference on
Programming Language Design and Implementation},
year = {2019},
month = jun,
doi = {10.1145/3314221.3314624}
}
@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,
url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-927.pdf},
institution = {University of Cambridge, Computer Laboratory},
number = {UCAM-CL-TR-927},
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.}
}
@techreport{cheri-formal-tr,
optkey = {},
author = {
Kyndylan Nienhuis
and Alexandre Joannou
and Anthony Fox
and Michael Roe
and Thomas Bauereiss
and Brian Campbell
and Matthew Naylor
and Robert M. Norton
and Simon W. Moore
and Peter G. Neumann
and Ian Stark
and Robert N. M. Watson
and Peter Sewell
},
title = {Rigorous engineering for hardware security: Formal modelling and proof in the {CHERI} design and implementation process},
institution = {University of Cambridge, Computer Laboratory},
number = {UCAM-CL-TR-940},
opthowpublished = {Draft},
month = sep,
year = {2019},
optnote = {},
optannote = {},
abstract = {The root causes of many security vulnerabilities include a pernicious combination of two problems, often regarded as inescapable aspects of computing. First, the protection mechanisms provided by the mainstream processor architecture and C/C++ language abstractions, dating back to the 1970s and before, provide only coarse-grain virtual-memory-based protection. Second, mainstream system engineering relies almost exclusively on test-and-debug methods, with (at best) prose specifications. These methods have historically sufficed commercially for much of the computer industry, but they fail to prevent large numbers of exploitable bugs, and the security problems that this causes are becoming ever more acute.
In this paper we show how more rigorous engineering methods can be applied to the development of a new security-enhanced processor architecture, with its accompanying hardware implementation and software stack. We use formal models of the complete instruction-set architecture (ISA) at the heart of the design and engineering process, both in lightweight ways that support and improve normal engineering practice -- as documentation, in emulators used as a test oracle for hardware and for running software, and for test generation -- and for formal verification. We formalise key intended security properties of the design, and establish that these hold with mechanised proof. This is for the same complete ISA models (complete enough to boot operating systems), without idealisation.
We do this for CHERI, an architecture with \emph{hardware capabilities} that supports fine-grained memory protection and scalable secure compartmentalisation, while offering a smooth adoption path for existing software. CHERI is a maturing research architecture, developed since 2010, with work now underway to explore its possible adoption in mass-market commercial processors. The rigorous engineering work described here has been an integral part of its development to date, enabling more rapid and confident experimentation, and boosting confidence in the design.
},
optproject = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
opttopic = {cheri},
cheriformal = {true},
recent = {true},
pdf = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-940.pdf}
}
@techreport{UCAM-CL-TR-932,
author = {Davis, Brooks and Watson, Robert N. M. and Richardson,
Alexander and Neumann, Peter G. and Moore, Simon W. and
Baldwin, John and Chisnall, David and Clarke, James and
Filardo, Nathaniel Wesley and Gudka, Khilan and Joannou,
Alexandre and Laurie, Ben and Markettos, A. Theodore and
Maste, J. Edward and Mazzinghi, Alfredo and Napierala,
Edward Tomasz and Norton, Robert M. and Roe, Michael and
Sewell, Peter and Son, Stacey and Woodruff, Jonathan},
title = {{CheriABI: Enforcing valid pointer provenance and
minimizing pointer privilege in the POSIX C run-time
environment}},
year = 2019,
month = jan,
pdf = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-932.pdf},
institution = {University of Cambridge, Computer Laboratory},
number = {UCAM-CL-TR-932},
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 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.},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
cheriformal = {true},
recent = {false}
}
@techreport{UCAM-CL-TR-941,
author = {Watson, Robert N. M. and Moore, Simon W. and
Sewell, Peter and Neumann, Peter},
title = {An Introduction to {CHERI}},
year = 2019,
month = sep,
pdf = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-941.pdf},
institution = {University of Cambridge, Computer Laboratory},
number = {UCAM-CL-TR-941},
abstract = {},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
cheriformal = {true},
recent = {false}
}
@article{8703061,
author = {J. {Woodruff} and A. {Joannou} and H. {Xia} and A. {Fox} and R. M. {Norton} and D. {Chisnall} and B. {Davis} and K. {Gudka} and N. W. {Filardo} and A. T. {Markettos} and M. {Roe} and P. G. {Neumann} and R. N. M. {Watson} and S. W. {Moore}},
journal = {IEEE Transactions on Computers},
title = {CHERI Concentrate: Practical Compressed Capabilities},
year = {2019},
month = oct,
volume = {68},
number = {10},
pages = {1455-1469},
abstract = {We present CHERI Concentrate, a new fat-pointer compression scheme applied to CHERI, the most developed capability-pointer system at present. Capability fat pointers are a primary candidate to enforce fine-grained and non-bypassable security properties in future computer systems, although increased pointer size can severely affect performance. Thus, several proposals for capability compression have been suggested elsewhere that do not support legacy instruction sets, ignore features critical to the existing software base, and also introduce design inefficiencies to RISC-style processor pipelines. CHERI Concentrate improves on the state-of-the-art region-encoding efficiency, solves important pipeline problems, and eases semantic restrictions of compressed encoding, allowing it to protect a full legacy software stack. We present the first quantitative analysis of compiled capability code, which we use to guide the design of the encoding format. We analyze and extend logic from the open-source CHERI prototype processor design on FPGA to demonstrate encoding efficiency, minimize delay of pointer arithmetic, and eliminate additional load-to-use delay. To verify correctness of our proposed high-performance logic, we present a HOL4 machine-checked proof of the decode and pointer-modify operations. Finally, we measure a 50 to 75 percent reduction in L2 misses for many compiled C-language benchmarks running under a commodity operating system using compressed 128-bit and 64-bit formats, demonstrating both compatibility with and increased performance over the uncompressed, 256-bit format.},
keywords = {data compression;decoding;encoding;field programmable gate arrays;microprocessor chips;pipeline processing;program compilers;reduced instruction set computing;storage management;theorem proving;tree data structures;practical compressed capabilities;fat-pointer compression scheme;developed capability-pointer system;capability fat pointers;nonbypassable security properties;future computer systems;increased pointer size;capability compression;legacy instruction sets;existing software base;design inefficiencies;RISC-style processor pipelines;state-of-the-art region-encoding efficiency;compressed encoding;legacy software stack;compiled capability code;encoding format;open-source CHERI prototype processor design;pointer arithmetic;decode;pointer-modify operations;commodity operating system;CHERI concentrate;pipeline problems;efficiency 75.0 percent;Encoding;Pipelines;Delays;Safety;Software;Semantics;Registers;Capabilities;fat pointers;compression;memory safety;computer architecture},
doi = {10.1109/TC.2019.2914037},
pdf = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/2019tc-cheri-concentrate.pdf},
issn = {},
month = {Oct}
}
@inproceedings{cheri-formal-SP2020,
author = {Kyndylan Nienhuis and Alexandre Joannou and Thomas Bauereiss and Anthony Fox and Michael Roe and Brian Campbell and Matthew Naylor and Robert M. Norton and Moore, Simon W. and Neumann, Peter G. and Ian Stark and Watson, Robert N. M. and Peter Sewell},
title = {Rigorous engineering for hardware security: Formal modelling and proof in the {CHERI} design and implementation process},
optcrossref = {},
optkey = {},
conf = {Security and Privacy 2020},
booktitle = {\textbf{Security and Privacy 2020}: Proceedings of the 41st IEEE Symposium on Security and Privacy (SP)},
year = {2020},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = may,
optaddress = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
abstract = {The root causes of many security vulnerabilities include a pernicious combination of two problems, often regarded as inescapable aspects of computing. First, the protection mechanisms provided by the mainstream processor architecture and C/C++ language abstractions, dating back to the 1970s and before, provide only coarse-grain virtual-memory-based protection. Second, mainstream system engineering relies almost exclusively on test-and-debug methods, with (at best) prose specifications. These methods have historically sufficed commercially for much of the computer industry, but they fail to prevent large numbers of exploitable bugs, and the security problems that this causes are becoming ever more acute.
In this paper we show how more rigorous engineering methods can be applied to the development of a new security-enhanced processor architecture, with its accompanying hardware implementation and software stack. We use formal models of the complete instruction-set architecture (ISA) at the heart of the design and engineering process, both in lightweight ways that support and improve normal engineering practice -- as documentation, in emulators used as a test oracle for hardware and for running software, and for test generation -- and for formal verification. We formalise key intended security properties of the design, and establish that these hold with mechanised proof. This is for the same complete ISA models (complete enough to boot operating systems), without idealisation.
We do this for CHERI, an architecture with \emph{hardware capabilities} that supports fine-grained memory protection and scalable secure compartmentalisation, while offering a smooth adoption path for existing software. CHERI is a maturing research architecture, developed since 2010, with work now underway on an Arm industrial prototype to explore its possible adoption in mass-market commercial processors. The rigorous engineering work described here has been an integral part of its development to date, enabling more rapid and confident experimentation, and boosting confidence in the design.
},
pdf = {https://www.cl.cam.ac.uk/users/pes20/cheri-formal.pdf},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
cheriformal = {true},
recent = {true}
}
@inproceedings{iflat-esop2020-extended,
author = {Ben Simner and Shaked Flur and Christopher Pulte and Alasdair Armstrong and Jean Pichon-Pharabod and Luc Maranget and Peter Sewell},
title = {{ARMv8-A} system semantics: instruction fetch in relaxed architectures (extended version)},
optcrossref = {},
optkey = {},
conf = {ESOP 2020},
booktitle = {\textbf{ESOP 2020:} Proceedings of the 29th European Symposium on Programming},
year = {2020},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = apr,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {This is an extended version of the ESOP 2020 paper, with appendices giving additional details},
optannote = {},
abstract = {Computing relies on \emph{architecture specifications} to decouple hardware and software development. Historically these have been prose documents, with all the problems that entails, but research over the last ten years has developed rigorous and executable-as-test-oracle specifications of mainstream architecture instruction sets and ``user-mode'' concurrency, clarifying architectures and bringing them into the scope of programming-language semantics and verification. However, the \emph{system semantics}, of instruction-fetch and cache maintenance, exceptions and interrupts, and address translation, remains obscure, leaving us without a solid foundation for verification of security-critical systems software.
In this paper we establish a robust model for one aspect of system semantics: instruction fetch and cache maintenance for ARMv8-A. Systems code relies on executing instructions that were written by data writes, e.g.~in program loading, dynamic linking, JIT compilation, debugging, and OS configuration, but hardware implementations are often highly optimised, e.g.~with instruction caches, linefill buffers, out-of-order fetching, branch prediction, and instruction prefetching, which can affect programmer-observable behaviour. It is essential, both for programming and verification, to abstract from such microarchitectural details as much as possible, but no more. We explore the key architecture design questions with a series of examples, discussed in detail with senior Arm staff; capture the architectural intent in operational and axiomatic semantic models, extending previous work on ``user-mode'' concurrency; make these models executable as test oracles for small examples; and experimentally validate them against hardware behaviour (finding a bug in one hardware device). We thereby bring these subtle issues into the mathematical domain, clarifying the architecture and enabling future work on system software verification.
},
topic = {Power_and_ARM},
recent = {true},
project = {http://www.cl.cam.ac.uk/~pes20/iflat},
pdf = {http://www.cl.cam.ac.uk/~pes20/iflat/top-extended.pdf}
}
@inproceedings{ChisnallCPDP11,
author = {Chisnall, David and Rothwell, Colin and Davis, Brooks and Watson, Robert N.M. and Woodruff, Jonathan and Vadera, Munraj and Moore, Simon W. and Neumann, Peter G. and Roe, Michael},
title = {Beyond the {PDP-11}: Processor support for a memory-safe {C} abstract machine},
booktitle = {\textbf{ASPLOS 2015}: Proceedings of the Fifteenth Edition of ASPLOS on Architectural Support for Programming Languages and Operating Systems},
conf = {ASPLOS 2015},
series = {ASPLOS XX},
year = {2015},
month = mar,
location = {Istanbul, Turkey},
numpages = {15},
publisher = {ACM},
address = {New York, NY, USA},
optkeywords = {C, memory safety, memory models, code generation},
doi = {10.1145/2694344.2694367},
optpdf = {papers/asplos15-memory-safe-c.pdf},
abstract = {We propose a new memory-safe interpretation of the C abstract machine that provides stronger protection to benefit
security and debugging. Despite ambiguities in the specification intended to provide implementation flexibility, contemporary implementations of C have converged on a memory model similar to the PDP-11, the original target for C.
This model lacks support for \emph{memory safety} despite well-documented impacts on security and reliability.
Attempts to change this model are often hampered by assumptions embedded in a large body of existing C code, dating back to the memory model exposed by the original C
compiler for the PDP-11. Our experience with attempting to
implement a memory-safe variant of C on the CHERI experimental microprocessor led us to identify a number of
problematic idioms. We describe these as well as their interaction with existing memory safety schemes and the assumptions that they make beyond the requirements of the C
specification. Finally, we refine the CHERI ISA and abstract
model for C, by combining elements of the CHERI capability model and fat pointers, and present a softcore CPU that
implements a C abstract machine that can run legacy C code
with strong memory protection guarantees.
}
}
@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.},
booktitle = {\textbf{ESOP 2015}: 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.
},
conf = {ESOP 2015},
pages = {283--307},
year = {2015},
month = apr,
optcrossref = {DBLP:conf/esop/2015},
url = {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}
}
@misc{EBC2014,
optkey = {},
author = {Reinoud Elhorst and Mark Batty and David Chisnall},
title = {Efficient code generation for weakly ordered architectures},
howpublished = {Presentation at the 4th European LLVM conference (EuroLLVM)},
month = apr,
year = 2014,
note = {Slides and report available at \url{http://llvm.org/devmtg/2014-04/}},
optannote = {},
abstract = {This report explores the way LLVM generates the
memory barriers needed to support the C11/C++11 atomics
for ARM. I measure the influence of memory barriers on
performance, and I show that in some cases LLVM generates
too many barriers. By leaving these barriers out, performance
increases significantly. I introduce two LLVM passes, which will
remove these extra barriers, improving performance in my test
by 40\%. I believe one of these passes is ready to be upstreamed
to LLVM, while the other will need more testing.
}
}
@misc{Elhorst2014,
optkey = {},
author = {Reinoud Elhorst},
title = {Lowering {C11} Atomics for {ARM} in {LLVM}},
opthowpublished = {},
optmonth = {},
year = {2014},
month = mar,
optnote = {},
optannote = {},
pdf = {http://llvm.org/devmtg/2014-04/PDFs/Talks/Reinoud-report.pdf},
abstract = {This report explores the way LLVM generates the
memory barriers needed to support the C11/C++11 atomics
for ARM. I measure the influence of memory barriers on
performance, and I show that in some cases LLVM generates
too many barriers. By leaving these barriers out, performance
increases significantly. I introduce two LLVM passes, which will
remove these extra barriers, improving performance in my test
by 40\%. I believe one of these passes is ready to be upstreamed
to LLVM, while the other will need more testing.
}
}
@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 = {},
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.
}
}
@inproceedings{Kell:2014:ST:2661136.2661154,
author = {Kell, Stephen},
title = {In Search of Types},
booktitle = {\textbf{Onward! 2014}: Proceedings of the 2014 ACM International Symposium on New
Ideas, New Paradigms, and Reflections on Programming \& Software},
conf = {Onward! 2014},
series = {Onward! 2014},
year = {2014},
month = oct,
isbn = {978-1-4503-3210-1},
location = {Portland, Oregon, USA},
pages = {227--241},
numpages = {15},
url = {http://doi.acm.org/10.1145/2661136.2661154},
doi = {10.1145/2661136.2661154},
acmid = {2661154},
publisher = {ACM},
address = {New York, NY, USA},
optkeywords = {abstraction, data types, information hiding, type
discipline, type system},
abstract = {The concept of "type" has been used without a consistent,
precise definition in discussions about programming languages for 60 years.
In this essay I explore various concepts lurking behind distinct uses of this word,
highlighting two traditions in which the word came into use largely independently:
engineering traditions on the one hand, and those of symbolic logic on the other.
These traditions are founded on differing attitudes to the nature and purpose of abstraction,
but their distinct uses of "type" have never been explicitly unified.
One result is that discourse across these traditions often finds itself at cross purposes,
such as overapplying one sense of "type" where another is appropriate, and occasionally
proceeding to draw wrong conclusions. I illustrate this with examples from well-known
and justly well-regarded literature, and argue that ongoing developments in both the
theory and practice of programming make now a good time to resolve these problems. }
}
@inproceedings{DBLP:conf/pepm/KerneisSH14,
author = {Gabriel Kerneis and
Charlie Shepherd and
Stefan Hajnoczi},
title = {{QEMU/CPC:} static analysis and {CPS} conversion for safe, portable,
and efficient coroutines},
booktitle = {\textbf{PEPM 2014}: Proceedings of the {ACM} {SIGPLAN} 2014 workshop on Partial evaluation
and program manipulation, San Diego,
California, {USA}},
conf = {PEPM 2014},
pages = {83--94},
year = {2014},
month = jan,
optcrossref = {DBLP:conf/pepm/2014},
url = {http://doi.acm.org/10.1145/2543728.2543733},
doi = {10.1145/2543728.2543733},
timestamp = {Thu, 09 Jan 2014 10:44:12 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/pepm/KerneisSH14},
bibsource = {dblp computer science bibliography, http://dblp.org},
abstract = {
Coroutines and events are two common abstractions for writing concurrent programs. Because coroutines are often more convenient, but events more portable and efficient, it is natural to want to translate the former into the latter. CPC is such a source-to-source translator for C programs, based on a partial conversion into continuation-passing style (CPS conversion) of functions annotated as cooperative.
In this article, we study the application of the CPC translator to QEMU, an open-source machine emulator which also uses annotated coroutine functions for concurrency. We first propose a new type of annotations to identify functions which never cooperate, and we introduce CoroCheck, a tool for the static analysis and inference of cooperation annotations. Then, we improve the CPC translator, defining CPS conversion as a calling convention for the C language, with support for indirect calls to CPS-converted function through function pointers. Finally, we apply CoroCheck and CPC to QEMU (750 000 lines of C code), fixing hundreds of missing annotations and comparing performance of the translated code with existing implementations of coroutines in QEMU.
Our work shows the importance of static annotation checking to prevent actual concurrency bugs, and demonstrates that CPS conversion is a flexible, portable, and efficient compilation technique, even for very large programs written in an imperative language.
}
}
@inproceedings{DBLP:conf/popl/Pichon-Pharabod16,
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.
},
booktitle = {\textbf{POPL 2016}: Proceedings of the 43rd Annual {ACM} {SIGPLAN-SIGACT} Symposium on
Principles of Programming Languages, St. Petersburg,
FL, USA, January 20 - 22, 2016},
conf = {POPL 2016},
pages = {622--633},
year = {2016},
month = jan,
optcrossref = {DBLP:conf/popl/2016},
url = {http://doi.acm.org/10.1145/2837614.2837616},
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},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/Pichon-Pharabod16},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@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 = {},
booktitle = {\textbf{PLDI 2016}},
conf = {PLDI 2016},
optpages = {},
year = {2016},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = jun,
optorganization = {},
optpublisher = {},
note = {PLDI 2016 Distinguished Paper award},
pdf = {http://www.cl.cam.ac.uk/users/pes20/cerberus/pldi16.pdf},
optannote = {}
}
@inproceedings{gudka15:soaap,
author = {Khilan Gudka and Robert N. M. Watson and Jonathan Anderson and David Chisnall and Brooks Davis and Ben Laurie and Ilias Marinos and Peter G. Neumann and Alex Richardson},
title = {{Clean Application Compartmentalization with SOAAP}},
booktitle = {\textbf{CCS 2015}: {Proceedings of the 22nd ACM Conference on Computer and Communications Security}},
conf = {CCS 2015},
month = oct,
year = {2015},
pdf = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/2015ccs-soaap.pdf},
abstract = {Application compartmentalization, a vulnerability mitigation technique
employed in programs such as OpenSSH and the Chromium web browser,
decomposes software into isolated components to limit privileges leaked
or otherwise available to attackers.
However, compartmentalizing applications -- and maintaining that
compartmentalization -- is hindered by ad hoc
methodologies and significantly increased programming effort.
In practice, programmers stumble through (rather than overtly reason
about) compartmentalization spaces of possible decompositions,
unknowingly trading off correctness, security, complexity, and
performance.
We present a new conceptual framework embodied in an LLVM-based tool: the
Security-Oriented Analysis of Application Programs (SOAAP) that allows
programmers to reason about co mpartmentalization using source-code
annotations (compartmentalization hypotheses).
We demonstrate considerable benefit when creating new compartmentalizations
for complex applications, and analyze existing compartmentalized
applications to discover design faults and maintenance issues arising
from application evolution.}
}
@misc{N2012,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {Clarifying the {C} memory object model},
howpublished = {ISO SC22 WG14 N2012},
html = {http://www.cl.cam.ac.uk/~pes20/cerberus/notes64-wg14.html},
month = mar,
year = 2016,
optnote = {},
optannote = {}
}
@misc{N2013,
optkey = {},
author = {David Chisnall and Justus Matthiesen and Kayvan Memarian and Kyndylan Nienhuis and Peter Sewell and Robert N. M. Watson},
title = {C memory object and value semantics: the space of de facto and {ISO} standards},
howpublished = {ISO SC22 WG14 N2013},
pdf = {http://www.cl.cam.ac.uk/~pes20/cerberus/notes30.pdf},
month = mar,
year = 2016,
optnote = {},
optannote = {}
}
@misc{N2014,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {What is {C} in practice? ({Cerberus} survey v2): Analysis of Responses},
howpublished = {ISO SC22 WG14 N2014},
html = {http://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html},
month = mar,
year = 2016,
optnote = {},
optannote = {}
}
@misc{N2015,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {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,
optnote = {},
optannote = {}
}
@phdthesis{battyPhD,
author = {Mark John Batty},
title = {The C11 and C++11 Concurrency Model},
school = {University of Cambridge Computer Laboratory},
year = {2014},
month = nov,
optkey = {},
opttype = {},
optaddress = {},
optmonth = {},
note = {Winner of 2015 ACM SIGPLAN John C. Reynolds
Doctoral Dissertation Award and 2015 CPHC/BCS Distinguished
Dissertation competition},
optannote = {}
}
@inproceedings{kell_dynamically_2016,
author = {Kell, Stephen},
title = {Dynamically diagnosing type errors in unsafe code},
booktitle = {\textbf{OOPSLA 2016}: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications},
conf = {OOPSLA 2016},
series = {OOPSLA 2016},
year = {2016},
month = nov,
location = {Amsterdam, The Netherlands},
numpages = {20},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {C, unsafe code, pointers, type information},
abstract = {Existing approaches for detecting type errors in unsafe languages are limited.
Static analysis methods are imprecise,
and often require source-level changes, while
most dynamic methods check only memory properties
(bounds, liveness, etc.), owing to a lack of run-time type information.
This paper describes \textsf{libcrunch},
a system for binary-compatible \emph{run-time} type checking of unmodified
unsafe code, currently focusing on C.
Practical experience shows that our prototype implementation
is easily applicable to many real codebases without source-level modification,
correctly flags programmer errors with a very low rate of false positives,
offers a very low run-time overhead,
and covers classes of error caught by no previously existing tool.},
pdf = {http://www.cl.cam.ac.uk/~pes20/rems/papers/typebugs.pdf}
}
@inproceedings{kell_missing_2016,
author = {Stephen Kell and Dominic P. Mulligan and Peter Sewell},
title = {The missing link: explaining {ELF} static linking, semantically},
booktitle = {\textbf{OOPSLA 2016}: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications},
conf = {OOPSLA 2016},
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.
},
pdf = {http://www.cl.cam.ac.uk/~pes20/rems/papers/oopsla-elf-linking-2016.pdf}
}
@inproceedings{operational-semantics-c11-2016,
author = {Kyndylan Nienhuis and Kayvan Memarian and Peter Sewell},
title = {An operational semantics for {C/C++11} concurrency},
booktitle = {\textbf{OOPSLA 2016}: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications},
conf = {OOPSLA 2016},
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.},
pdf = {http://www.cl.cam.ac.uk/~pes20/rems/papers/nienhuis-oopsla-2016.pdf}
}
@misc{N2089,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {Clarifying Unspecified Values (Draft Defect Report or Proposal for C2x)},
howpublished = {ISO SC22 WG14 N2089},
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2089.htm},
month = sep,
year = 2016,
optnote = {},
optannote = {}
}
@misc{N2090,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {Clarifying Pointer Provenance (Draft Defect Report or Proposal for C2x)},
howpublished = {ISO SC22 WG14 N2090},
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2090.htm},
month = sep,
year = 2016,
optnote = {},
optannote = {}
}
@misc{N2091,
optkey = {},
author = {Kayvan Memarian and Peter Sewell},
title = {Clarifying Trap Representations (Draft Defect Report or Proposal for C2x)},
howpublished = {ISO SC22 WG14 N2091},
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2091.htm},
month = sep,
year = 2016,
optnote = {},
optannote = {}
}
@inproceedings{Chisnall2017,
author = {Chisnall, David and Davis, Brooks and Gudka, Khilan and Brazdil, David and Joannou, Alexandre and Woodruff, Jonathan and Markettos, A. Theodore and Maste, J. Edward and Norton, Robert and Son, Stacey and Roe, Michael and Moore, Simon W. and Neumann, Peter G. and Laurie, Ben and Watson, Robert N.M.},
title = {{CHERI JNI: Sinking the Java Security Model into the C}},
booktitle = {\textbf{ASPLOS 2017}: Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems},
series = {ASPLOS '17},
conf = {ASPLOS 2017},
year = {2017},
month = apr,
isbn = {978-1-4503-4465-4},
location = {Xi'an, China},
pages = {569--583},
numpages = {15},
url = {http://doi.acm.org/10.1145/3037697.3037725},
doi = {10.1145/3037697.3037725},
acmid = {3037725},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {architecture, capability systems, cheri, compartmentalization, compilers, hardware security, java, jni, language security, memory protection, sandboxing},
abstract = {Java provides security and robustness by building a high-level security model atop the foundation of memory protection. Unfortunately, any native code linked into a Java program -- including the million lines used to implement the standard library -- is able to bypass both the memory protection and the higher-level policies. We present a hardware-assisted implementation of the Java native code interface, which extends the guarantees required for Java's security model to native code.
Our design supports safe direct access to buffers owned by the JVM, including hardware-enforced read-only access where appropriate. We also present Java language syntax to declaratively describe isolated compartments for native code.
We show that it is possible to preserve the memory safety and isolation requirements of the Java security model in C code, allowing native code to run in the same process as Java code with the same impact on security as running equivalent Java code. Our approach has a negligible impact on performance, compared with the existing unsafe native code interface. We demonstrate a prototype implementation running on the CHERI microprocessor synthesized in FPGA.}
}
@inproceedings{DBLP:conf/popl/KumarMNO14,
author = {Ramana Kumar and
Magnus O. Myreen and
Michael Norrish and
Scott Owens},
title = {{CakeML}: a verified implementation of {ML}},
booktitle = {\textbf{POPL 2014}: The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
Programming Languages, San Diego, CA, USA},
conf = {POPL 2014},
pages = {179--192},
year = {2014},
month = jan,
optcrossref = {DBLP:conf/popl/2014},
url = {http://doi.acm.org/10.1145/2535838.2535841},
doi = {10.1145/2535838.2535841},
timestamp = {Thu, 09 Jan 2014 08:32:32 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/KumarMNO14},
bibsource = {dblp computer science bibliography, http://dblp.org},
abstract = {
We have developed and mechanically verified an ML system called CakeML, which supports a substantial subset of Standard ML. CakeML is implemented as an interactive read-eval-print loop (REPL) in x86-64 machine code. Our correctness theorem ensures that this REPL implementation prints only those results permitted by the semantics of CakeML. Our verification effort touches on a breadth of topics including lexing, parsing, type checking, incremental and dynamic compilation, garbage collection, arbitrary-precision arithmetic, and compiler bootstrapping.
Our contributions are twofold. The first is simply in building a system that is end-to-end verified, demonstrating that each piece of such a verification effort can in practice be composed with the others, and ensuring that none of the pieces rely on any over-simplifying assumptions. The second is developing novel approaches to some of the more challenging aspects of the verification. In particular, our formally verified compiler can bootstrap itself: we apply the verified compiler to itself to produce a verified machine-code implementation of the compiler. Additionally, our compiler proof handles diverging input programs with a lightweight approach based on logical timeout exceptions. The entire development was carried out in the HOL4 theorem prover.}
}
@article{DBLP:journals/jfp/MyreenO14,
author = {Magnus O. Myreen and
Scott Owens},
title = {Proof-producing translation of higher-order logic into pure and stateful
{ML}},
journal = {\textbf{J. Funct. Program.}},
volume = {24},
number = {2-3},
pages = {284--315},
year = {2014},
month = jan,
url = {http://dx.doi.org/10.1017/S0956796813000282},
doi = {10.1017/S0956796813000282},
timestamp = {Mon, 26 May 2014 10:31:52 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/jfp/MyreenO14},
bibsource = {dblp computer science bibliography, http://dblp.org},
abstract = {
The higher-order logic found in proof assistants such as Coq and various HOL systems provides a convenient setting for the development and verification of functional programs. However, to efficiently run these programs, they must be converted (or `extracted') to functional programs in a programming language such as ML or Haskell. With current techniques, this step, which must be trusted, relates similar looking objects that have very different semantic definitions, such as the set-theoretic model of a logic and the operational semantics of a programming language. In this paper, we show how to increase the trustworthiness of this step with an automated technique. Given a functional program expressed in higher-order logic, our technique provides the corresponding program for a functional language defined with an operational semantics, and it provides a mechanically checked theorem relating the two. This theorem can then be used to transfer verified properties of the logical function to the program. We have implemented our technique in the HOL4 theorem prover, translating functions to a subset of Standard ML, and have applied the implementation to examples including functional data structures, a parser generator, cryptographic algorithms, a garbage collector and the 500-line kernel of the HOL light theorem prover. This paper extends our previous conference publication with new material that shows how functions defined in terms of a state-and-exception monad can be translated, with proofs, into stateful ML code. The HOL light example is also new.}
}
@inproceedings{YongKiamMKFON16,
author = {Tan, Yong Kiam and Magnus O. Myreen and Ramana Kumar and
Anthony Fox and Scott Owens and Michael Norrish},
title = {A New Verified Compiler Backend for {CakeML}},
booktitle = {Proc. \textbf{ICFP 2016}: International Conference on Functional Programming},
conf = {ICFP 2016},
year = 2016,
month = sep,
doi = {10.1145/2951913.2951924},
pdf = {https://cakeml.org/icfp16.pdf},
publisher = {ACM Press},
abstract = {
We have developed and mechanically verified a new compiler backend
for CakeML. Our new compiler features a sequence of intermediate
languages that allows it to incrementally compile away high-level
features and enables verification at the right levels of semantic
detail. In this way, it resembles mainstream (unverified)
compilers for strict functional languages. The compiler supports
efficient curried multi-argument functions, configurable data
representations, exceptions that unwind the call stack, register
allocation, and more. The compiler targets several architectures:
x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V.
In this paper, we present the overall structure of the compiler,
including its 12 intermediate languages, and explain how
everything fits together. We focus particularly on the
interaction between the verification of the register allocator and
the garbage collector, and memory representations. The entire
development has been carried out within the HOL4 theorem prover.
}
}
@inproceedings{FoxMTK17,
author = {Anthony C. J. Fox and
Magnus O. Myreen and
Yong Kiam Tan and
Ramana Kumar},
title = {Verified compilation of {CakeML} to multiple
machine-code targets},
booktitle = {Proc. \textbf{CPP 2017}: Certified Programs and Proofs},
conf = {CPP 2017},
year = {2017},
month = jan,
doi = {10.1145/3018610.3018621},
editor = {Yves Bertot and Viktor Vafeiadis},
pdf = {https://cakeml.org/cpp17.pdf},
publisher = {{ACM}},
abstract = {
This paper describes how the latest CakeML compiler supports
verified compilation down to multiple realistically modelled
target architectures. In particular, we describe how the compiler
definition, the various language semantics, and the correctness
proofs were organised to minimize target-specific overhead. With
our setup we have incorporated compilation to four 64-bit
architectures, ARMv8, x86-64, MIPS-62, RISC-V, and one 32-bit
architecture, ARMv6. Our correctness theorem allows interference
from the environment: the top-level correctness statement takes
into account execution of foreign code and per-instruction
interference from external processes, such as interrupt handlers
in operating systems. The entire CakeML development is formalised
in the HOL4 theorem prover.
}
}
@inproceedings{kell_towards_20XX,
author = {Stephen Kell},
title = {Towards a dynamic object model within {Unix} processes},
booktitle = {\textbf{Onward! 2015}: 2015 {ACM} International Symposium on New Ideas, New Paradigms, and
Reflections on Programming and Software, Pittsburgh,
PA, USA},
conf = {Onward! 2015},
pages = {224--239},
year = {2015},
month = oct,
xcrossref = {DBLP:conf/oopsla/2015onward},
url = {http://doi.acm.org/10.1145/2814228.2814238},
doi = {10.1145/2814228.2814238},
timestamp = {Wed, 28 Oct 2015 16:51:55 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/oopsla/Kell15},
bibsource = {dblp computer science bibliography, http://dblp.org},
abstract = {Programmers face much complexity from the co-existence of
``native'' (Unix-like) and virtual machine (VM) ``managed'' run-time environments.
Rather than having VMs replace Unix processes, we investigate whether it makes
sense for the latter to ``become VMs'', by evolving Unix's
user-level services to subsume those of VMs.
We survey the (little-understood) VM-like features in modern Unix, noting
common shortcomings: a lack of semantic metadata (``type information'')
and the inability to bind from objects ``back'' to their metadata.
We describe the design and implementation of
a system, \textsf{liballocs}, which adds these capabilities in a highly compatible way,
and explore its consequences.},
pdf = {http://www.cl.cam.ac.uk/~srk31/research/papers/kell15towards-preprint.pdf}
}
@inproceedings{kell:some:2017,
author = {Kell, Stephen},
title = {Some were meant for {C}: the endurance of an unmanageable language},
booktitle = {\textbf{Onward! 2017}: Proceedings of the 2017 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming \& Software},
conf = {Onward! 2017},
series = {Onward! 2017},
year = {2017},
month = oct,
location = {Vancouver, British Columbia, Canada},
numpages = {18},
pdf = {http://www.cl.cam.ac.uk/~srk31/research/papers/kell17some-preprint.pdf},
doi = {10.1145/3133850.3133867},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {systems programming, virtual machine, managed languages, safety, undefined behavior},
abstract = {The C language leads a double life: as an application
programming language of yesteryear, perpetuated by
circumstance, and as a systems programming language
which remains a weapon of choice decades after its creation. This essay is a C programmer's reaction to the call
to abandon ship. It questions several properties commonly held to define the experience of using C; these
include unsafety, undefined behaviour, and the motivation of performance. It argues all these are in fact
inessential; rather, it traces C's ultimate strength to a
communicative design which does not fit easily within
the usual conception of ``a programming language'', but
can be seen as a counterpoint to so-called ``managed
languages''. This communicativity is what facilitates the
essential aspect of system-building: creating parts which
interact with other, remote parts---being ``alongside'' not
``within''. }
}
@article{YALLOP2017,
title = {A modular foreign function interface},
journal = {\textbf{Science of Computer Programming}},
year = {2017},
month = apr,
issn = {0167-6423},
doi = {https://doi.org/10.1016/j.scico.2017.04.002},
url = {http://www.sciencedirect.com/science/article/pii/S0167642317300709},
pdf = {https://www.cl.cam.ac.uk/~jdy22/papers/a-modular-foreign-function-interface.pdf},
author = {Jeremy Yallop and David Sheets and Anil Madhavapeddy},
keywords = {Foreign functions},
keywords = {Functional programming},
keywords = {Modularity},
abstract = {Abstract foreign function interfaces are typically organised monolithically, tying together the specification of each foreign function with the mechanism used to make the function available in the host language. This leads to inflexible systems, where switching from one binding mechanism to another (say from dynamic binding to static code generation) often requires changing tools and rewriting large portions of code. We show that ML-style module systems support exactly the kind of abstraction needed to separate these two aspects of a foreign function binding, leading to declarative foreign function bindings that support switching between a wide variety of binding mechanisms -- static and dynamic, synchronous and asynchronous, etc. -- with no changes to the function specifications. Note. This is a revised and expanded version of an earlier paper, Declarative Foreign Function Binding Through Generic Programming. This paper brings a greater focus on modularity, and adds new sections on error handling, and on the practicality of the approach we describe.}
}
@inproceedings{Watt:2018:MVW:3176245.3167082,
author = {Watt, Conrad},
title = {Mechanising and Verifying the {WebAssembly} Specification},
conf = {CPP 2018},
booktitle = {\textbf{CPP 2018}: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs},
series = {CPP 2018},
year = {2018},
isbn = {978-1-4503-5586-5},
location = {Los Angeles, CA, USA},
pages = {53--65},
numpages = {13},
url = {http://doi.acm.org/10.1145/3167082},
doi = {10.1145/3167082},
acmid = {3167082},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {bytecode, reduction, soundness, stack machine},
pdf = {http://www.cl.cam.ac.uk/users/pes20/mechanising-and-verifying-the-webassembly-specification.pdf},
abstract = {WebAssembly is a new low-level language currently being implemented in all major web browsers. It is designed to become the universal compilation target for the web, obsoleting existing solutions in this area, such as asm.js and Native Client. The WebAssembly working group has incorporated formal techniques into the development of the language, but their efforts so far have focussed on pen and paper formal specification.
We present a mechanised Isabelle specification for the WebAssembly language, together with a verified executable interpreter and type checker. Moreover, we present a fully mechanised proof of the soundness of the WebAssembly type system, and detail how our work on this proof has exposed several issues with the official WebAssembly specification, influencing its development. Finally, we give a brief account of our efforts in performing differential fuzzing of our interpreter against industry implementations.}
}
@inproceedings{Chargueraud2018JSExplain,
author = {Chargu{\'e}raud, Arthur and Schmitt, Alan and Wood, Thomas},
title = {{JSExplain}: a Double Debugger for {JavaScript}},
booktitle = {\textbf{WWW '18 Companion}: The 2018 Web Conference Companion, April 23--27, 2018, Lyon, France},
conf = {WWW},
year = {2018},
month = apr,
publisher = {ACM},
abstract = {We present JSExplain, a reference interpreter for JavaScript that closely
follows the specification and that produces execution traces.
These traces may be interactively investigated in a browser, with an
interface that displays not only the code and the state of the interpreter,
but also the code and the state of the interpreted program.
Conditional breakpoints may be expressed with respect to both the interpreter
and the interpreted program. In that respect, JSExplain is a double-debugger
for the specification of JavaScript.},
doi = {10.1145/3184558.3185969},
pdf = {https://psvg.doc.ic.ac.uk/publications/Chargueraud2018JSExplain.pdf}
}
@inproceedings{FragosoSantos2018JaVerT,
author = {{Fragoso Santos}, Jos{\'{e}} and Maksimovi\'{c}, Petar and Naud\v{z}i\={u}nien\.{e}, Daiva and Wood, Thomas and Gardner, Philippa},
title = {{JaVerT: JavaScript verification toolchain}},
booktitle = {\textbf{POPL 2018}},
conf = {POPL 2018},
optjournal = {{PACMPL}},
optvolume = {2},
optnumber = {\textbf{POPL}},
optconf = {{POPL}},
optpages = {50:1--50:33},
year = {2018},
month = jan,
abstract = {The dynamic nature of JavaScript and its complex semantics make it a difficult target for logic-based verification.
We introduce JaVerT, a semi-automatic JavaScript Verification Toolchain, based on separation logic and aimed at the specialist developer wanting rich,
mechanically verified specifications of critical JavaScript code. To specify JavaScript programs,
we design abstractions that capture its key heap structures (for example, prototype chains and function closures),
allowing the developer to write clear and succinct specifications with minimal knowledge of the JavaScript internals.
To verify JavaScript programs, we develop JaVerT, a verification pipeline consisting of: JS-2-JSIL,
a well-tested compiler from JavaScript to JSIL, an intermediate goto language capturing the fundamental dynamic features of JavaScript;
JSIL Verify, a semi-automatic verification tool based on a sound JSIL separation logic;
and verified axiomatic specifications of the JavaScript internal functions.
Using JaVerT, we verify functional correctness properties of:
data-structure libraries (key-value map, priority queue) written in an object-oriented style;
operations on data structures such as binary search trees (BSTs) and lists; examples illustrating function closures;
and test cases from the official ECMAScript test suite. The verification times suggest that reasoning about larger,
more complex code using JaVerT is feasible.
},
doi = {10.1145/3158138},
pdf = {https://psvg.doc.ic.ac.uk/publications/FragosoSantos2018JaVerT.pdf}
}
@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 = {\textbf{POPL 2019}: 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},
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},
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{ct-wasm,
author = {Conrad Watt and John Renner and Natalie Popescu and Sunjay Cauligi and Deian Stefan},
title = {{CT-Wasm}: Type-Driven Secure Cryptography for the Web Ecosystem},
optnote = {Under submission.},
conf = {POPL 2019},
booktitle = {\textbf{POPL 2019}: Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages},
year = {2019},
month = jan,
abstract = {A significant amount of both client and server-side cryptography is implemented in JavaScript. Despite widespread concerns about its security, no other language has been able to match the convenience that comes from its ubiquitous support on the “web ecosystem” - the wide variety of technologies that collectively underpins the modern World Wide Web. With the introduction of the new WebAssembly bytecode language (Wasm) into the web ecosystem, we have a unique opportunity to advance a principled alternative to existing JavaScript cryptography use cases which does not compromise this convenience.
We present Constant-Time WebAssembly (CT-Wasm), a type-driven, strict extension to WebAssembly which facilitates the verifiably secure implementation of cryptographic algorithms. CT-Wasm’s type system ensures that code written in CT-Wasm is both information flow secure and resistant to timing side channel attacks; like base Wasm, these guarantees are verifiable in linear time. Building on an existing Wasm mechanization, we mechanize the full CT-Wasm specification, prove soundness of the extended type system, implement a verified type checker, and give several proofs of the language’s security properties.
We provide two implementations of CT-Wasm: an OCaml reference interpreter and a native implementation for Node.js and Chromium that extends Google’s V8 engine. We also implement a CT-Wasm to Wasm rewrite tool that allows developers to reap the benefits of CT-Wasm’s type system today, while developing cryptographic algorithms for base Wasm environments. We evaluate the language, our implementations, and supporting tools by porting several cryptographic primitives - Salsa20, SHA-256, and TEA - and the full TweetNaCl library. We find that CT-Wasm is fast, expressive, and generates code that we experimentally measure to be constant-time.},
pdf = {https://arxiv.org/pdf/1808.01348.pdf}
}
@inproceedings{CSEJS,
author = {{Fragoso Santos}, Jos{\'{e}} and Maksimovi\'{c}, Petar and Sampaio, Gabriela and Gardner, Philippa},
title = {{JaVerT 2.0}: Compositional Symbolic Execution for {JavaScript}},
conf = {POPL 2019},
booktitle = {\textbf{POPL 2019}: Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages},
year = {2019},
month = jan,
optnote = {Submitted for publication},
abstract = {
We propose a novel, unified approach to the development of compositional symbolic execution tools, bridging the gap between classical symbolic execution and compositional program reasoning based on separation logic. Using this approach, we build a new analysis tool for JavaScript that follows the semantics of the language without any simplifications, with support for whole-program symbolic testing, verification, and, for the first time, automatic compositional testing based on bi-abduction. The meta-theory underpinning the tool is developed in a modular way, streamlining the proofs and informing the implementation. Our explicit treatment of symbolic execution errors allows us to give meaningful feedback to the developer during whole-program symbolic testing and guides the inference of resource of the bi-abductive execution. We evaluate the performance of our tool on a number of JavaScript data-structure libraries, demonstrating the scalability of whole-program symbolic testing, an improvement over our previous work on JavaScript verification, and automatic creation of useful specifications using bi-abduction.},
pdf = {http://vtss.doc.ic.ac.uk/publications/FragosoSantos2019JaVerT.pdf}
}
@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},
optnote = {To appear},
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}
}
@inproceedings{Dolan:2018:BDR:3192366.3192421,
author = {Dolan, Stephen and Sivaramakrishnan, KC and Madhavapeddy, Anil},
title = {Bounding Data Races in Space and Time},
booktitle = {\textbf{PLDI 2018}: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation},
series = {PLDI 2018},
conf = {PLDI 2018},
year = {2018},
month = jun,
isbn = {978-1-4503-5698-5},
location = {Philadelphia, PA, USA},
pages = {242--255},
numpages = {14},
url = {http://doi.acm.org/10.1145/3192366.3192421},
doi = {10.1145/3192366.3192421},
acmid = {3192421},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {operational semantics, weak memory models},
pdf = {http://kcsrk.info/papers/pldi18-memory.pdf},
abstract = {We propose a new semantics for shared-memory parallel programs that gives strong guarantees even in the presence of data races. Our \emph{local data race freedom} property guarantees that all data-race-free portions of programs exhibit sequential semantics. We provide a straightforward operational semantics and an equivalent axiomatic model, and evaluate an implementation for the OCaml programming language. Our evaluation demonstrates that it is possible to balance a comprehensible memory model with a reasonable (no overhead on x86, $\sim$0.6\% on ARM) sequential performance trade-off in a mainstream programming language.}
}
@phdthesis{PichonPhD,
author = {Pichon-Pharabod, Jean},
title = {A no-thin-air memory model for programming languages},
school = {University of Cambridge},
year = 2018,
abstract = {Many hardware and compiler optimisations introduced to speed up single-threaded programs also introduce additional, sometimes surprising, behaviours for concurrent programs with shared mutable state. How many of these extra behaviours occur in practice depends on the combination of the hardware, compiler, runtime, etc. that make up the platform. A memory model, which prescribes what values each read of a concurrent program can read, allows programmers to determine whether a program behaves as expected without having to worry about the details of the platform. However, capturing these behaviours in a memory model without also including undesirable ``out-of-thin-air'' behaviours that do not occur in practice has proved elusive. The memory model of C and C++ allows out-of-thin-air behaviour, while the Java memory model fails to capture some behaviours that are introduced in practice by compiler optimisations.
In this thesis, we propose a memory model that forbids out-of-thin-air behaviour, yet allows the behaviours that do occur. Our memory model follows operational intuitions of how the hardware and compilers operate. We illustrate that it behaves as desired on a series of litmus tests. We show that it captures at least some of the expected behaviours, that it forms an envelope around some common compiler optimisations, and that it is implementable on common hardware using the expected compilation schemes. We also show that it supports some established programming idioms.}
}
@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},
html = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2219.htm},
month = mar,
year = 2018,
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
optnote = {},
optannote = {},
topic = {Cerberus}
}
@misc{N2220,
optkey = {},
author = {Kayvan Memarian and Victor Gomes and Peter Sewell},
title = {N2220: Clarifying Trap Representations (Q47) v3},
howpublished = {ISO SC22 WG14 N2220},
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 = {Cerberus}
}
@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},
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 = {Cerberus}
}
@misc{N2222,
optkey = {},
author = {Kayvan Memarian and Victor Gomes and Peter Sewell},
title = {N2222: Further Pointer Issues (Q21-Q46)},
howpublished = {ISO SC22 WG14 N2222},
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 = {Cerberus}
}
@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},
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 = {Cerberus}
}
@misc{N2263,
optkey = {},
author = {Kayvan Memarian and Victor Gomes and Peter Sewell},
title = {N2263 Sewell,Clarifying Pointer Provenance (Q1-Q20) v4},
howpublished = {ISO SC22 WG14 N2263},
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 = {Cerberus}
}
@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 = {\textbf{CAV 2019}: Proc. 31st International Conference on Computer-Aided Verification},
optpages = {},
year = {2019},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = jul,
optorganization = {},
optpublisher = {},
note = {(tool paper)},
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}
}
@inproceedings{weakening-webassembly-2019,
author = {Conrad Watt and Andreas Rossberg and Jean Pichon-Pharabod},
title = {Weakening {WebAssembly}},
conf = {OOPSLA 2019},
booktitle = {\textbf{OOPSLA 2019}: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications},
optbooktitle = {},
year = {2019},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = oct,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {Proc. ACM Program. Lang. 3, OOPSLA, Article 133},
optnote = {},
optannote = {},
doi = {10.1145/3360559},
abstract = {WebAssembly (Wasm) is a safe, portable virtual instruction set that can be hosted in a wide range of environments, such as a Web browser. It is a low-level language whose instructions are intended to compile directly to bare hardware. While the initial version of Wasm focussed on single-threaded computation, a recent proposal extends it with low-level support for multiple threads and atomic instructions for synchronised access to shared memory. To support the correct compilation of concurrent programs, it is necessary to give a suitable specification of its memory model.
Wasm's language definition is based on a fully formalised specification that carefully avoids undefined behaviour. We present a substantial extension to this semantics, incorporating a relaxed memory model, along with a few proposed extensions. Wasm's memory model is unique in that its linear address space can be dynamically grown during execution, while all accesses are bounds-checked. This leads to the novel problem of specifying how observations about the size of the memory can propagate between threads. We argue that, considering desirable compilation schemes, we cannot give a sequentially consistent semantics to memory growth.
We show that our model provides sequential consistency for data-race-free executions (SC-DRF). However, because Wasm is to run on the Web, we must also consider interoperability of its model with that of JavaScript. We show, by counter-example, that JavaScript's memory model is not SC-DRF, in contrast to what is claimed in its specification. We propose two axiomatic conditions that should be added to the JavaScript model to correct this difference.
We also describe a prototype SMT-based litmus tool which acts as an oracle for our axiomatic model, visualising its behaviours, including memory resizing.
},
pdf = {https://dl.acm.org/ft_gateway.cfm?id=3360559}
}
@inproceedings{Watt2019Program,
author = {Watt, Conrad and Maksimovic, Petar and Krishnaswami, Neelakantan R. and Gardner, Philippa},
title = {A Program Logic for First-Order Encapsulated {WebAssembly}},
conf = {ECOOP 2019},
booktitle = {\textbf{ECOOP 2019}: Proceedings of the 33 \textsuperscript{rd} European Conference on Object-Oriented Programming). },
pages = {10:1–10:30 },
month = jul,
year = {2019},
doi = { 10.4230/LIPIcs.ECOOP.2019.10},
abstract = { We introduce Wasm Logic, a sound program logic for first-order, encapsulated WebAssembly. We
design a novel assertion syntax, tailored to WebAssembly’s stack-based semantics and the strong
guarantees given by WebAssembly’s type system, and show how to adapt the standard separation
logic triple and proof rules in a principled way to capture WebAssembly’s uncommon structured
control flow. Using Wasm Logic, we specify and verify a simple WebAssembly B-tree library, giving
abstract specifications independent of the underlying implementation. We mechanise Wasm Logic
and its soundness proof in full in Isabelle/HOL. As part of the soundness proof, we formalise
and fully mechanise a novel, big-step semantics of WebAssembly, which we prove equivalent, up
to transitive closure, to the original WebAssembly small-step semantics. Wasm Logic is the first
program logic for WebAssembly, and represents a first step towards the creation of static analysis
tools for WebAssembly.}
}
@techreport{UCAM-CL-TR-947,
author = {Watson, Robert N. M. and Richardson, Alexander and Davis,
Brooks and Baldwin, John and Chisnall, David and Clarke,
Jessica and Filardo, Nathaniel and Moore, Simon W. and
Napierala, Edward and Sewell, Peter and Neumann, Peter G.},
title = {{CHERI C/C++ Programming Guide}},
year = 2020,
month = jun,
url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-947.pdf},
institution = {University of Cambridge, Computer Laboratory},
number = {UCAM-CL-TR-947},
abstract = {This document is a brief introduction to the CHERI C/C++ programming languages. We explain the principles underlying these language variants, and their grounding in CHERI’s multiple architectural instantiations: CHERI-MIPS, CHERI-RISC-V, and Arm’s Morello. We describe the most commonly encountered differences between these dialects and C/C++ on conventional architectures, and where existing software may require minor changes. We document new compiler warnings and errors that may be experienced compiling code with the CHERI Clang/LLVM compiler, and suggest how they may be addressed through typically minor source-code changes. We explain how modest language extensions allow selected software, such as memory allocators, to further refine permissions and bounds on pointers. This guidance is based on our experience adapting the FreeBSD operating-system userspace, and applications such as PostgreSQL and WebKit, to run in a CHERI C/C++ capability-based programming environment. We conclude by recommending further reading.},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
recent = {true}
}
@inproceedings{Xiong2020Data,
author = {Shale Xiong and
Andrea Cerone and
Azalea Raad and
Philippa Gardner},
title = {Data Consistency in Transactional Storage Systems: a Centralised Approach},
conf = {ECOOP 2020},
booktitle = {\textbf{ECOOP 2020}: 34th European Conference on Object-Oriented Programming},
project = {concurrency},
year = {2020},
abstract = {We introduce an interleaving operational semantics for describing the
client-observable behaviour of atomic transactions on distributed key-value stores.
Our semantics builds on abstract states comprising centralised, global key-value
stores and partial client views. We provide operational definitions of consistency
models for our abstract states which we show to be equivalent to the well known
declarative definitions of consistency model on abstract executions. We explore
two applications, verifying that the COPS replicated database and the Clock-SI
partitioned database satisfy their consistency models using trace refinement,
and proving invariant properties of client programs.}
}
@inproceedings{FragosoSantos2020Gillian,
author = {Jos{\'{e}} {Fragoso Santos} and Petar Maksimovic and Sacha{-}{\'{E}}lie Ayoun and Philippa Gardner},
title = { Gillian, Part I: A Multi-language Platform for Symbolic Execution },
conf = {PLDI 2020},
booktitle = {\textbf{PLDI 2020}: Proceedings of the 41st ACM SIGPLAN
International Conference on Programming Language Design and Implementation},
year = {2020},
doi = {10.1145/3385412.3386014},
project = { gillian },
abstract = { We introduce Gillian, a platform for developing symbolic
analysis tools for programming languages. Here, we focus on
the symbolic execution engine at the heart of Gillian, which
is parametric on the memory model of the target language.
We give a formal description of the symbolic analysis and
a modular implementation that closely follows this description.
We prove a parametric soundness result, introducing
restriction on abstract states, which generalises path conditions
used in classical symbolic execution. We instantiate
Gillian to obtain trusted symbolic testing tools for JavaScript
and C, and use these tools to find bugs in real-world code,
thus demonstrating the viability of our parametric approach.}
}
@inproceedings{Sampaio2020Trusted,
author = {Gabriela Sampaio and
Jos{\'{e}} {Fragoso Santos} and
Petar Maksimovic
and Philippa Gardner},
title = {A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications},
conf = {ECOOP 2020},
booktitle = {\textbf{ECOOP 2020}: 34th European Conference on Object-Oriented Programming},
project = { web },
year = {2020},
abstract = {We introduce a trusted infrastructure for symbolic analysis of modern
event-driven Web applications. This infrastructure consists of reference
implementations of the DOM Core Level 1 and UI Events, JavaScript Promises,
and the JavaScript async/await APIs, all underpinned by a simple Core Event
Semantics that is sufficiently expressive to describe the event models underlying
all these APIs. Our reference implementations are trustworthy in that they follow
the API respective standards line-by-line and they are thoroughly tested against
the appropriate official test-suites, passing all the applicable tests. Using the
Core Events Semantics and the reference implementations, we develop JaVerT.Click,
a symbolic execution tool for JavaScript that, for the first time, supports reasoning
about JavaScript programs that use some (possibly all) these APIs. Using JaVerT.Click,
we perform comprehensive symbolic testing of the events module of Cash, a widely-used jQuery
alternative, creating a symbolic test suite with 100 per cent line coverage, establishing bounded
correctness of several essential properties of the module, and discovering two subtle,
previously unknown bugs.}
}
@phdthesis{Xiong2020Parametric,
author = {Shale Xiong},
title = {Parametric Operational Semantics for Consistency Models},
school = {Imperial College London},
year = {2020},
project = {concurrency},
phdthesis = {Y},
abstract = {The cloud has become popular for its low cost, high availability and
high fault-tolerance-queue or de-queue, for example Amazon Web Service (AWS) and
Google Cloud Platform (GCP. Those cloud infrastructures provide fixed interface,
to hide the complex internal implementation that consists of hundreds of thousands
of machines globally that work together as a whole system, known as a distributed
system. Clients of those systems only need to work with the abstract interfaces.
Transactions are the de facto interfaces in modern distributed databases.
Because of the CAP theorem, a distributed system must sacrifice strong consistency
to achieve high availability and high fault-tolerance. Engineers and researchers
have proposed many reference implementations in specific setting for various weak
consistency models. However, there have been little work on formalising the interfaces.
We introduce an interleaving operational semantics for describing such interfaces,
with the focus on the client-observable behaviour of atomic transactions on
distributed key-value stores. Our semantics builds on abstract states comprising
centralised, global key-value stores and partial client views. We provide
operational definitions of consistency models for our key-value stores which
are shown to be equivalent to the well-known declarative definitions of consistency
models for execution graphs. We explore two immediate applications of our semantics:
specific protocols of databases for a specific consistency can be verified in
our centralised semantics; programs can be directly shown to have invariant
properties such as robustness results against a weak consistency model.}
}
@inproceedings{cornucopia,
author = {Nathaniel Wesley Filardo and Brett F. Gutstein and Jonathan Woodruff and Sam Ainsworth and Lucian Paul-Trifu and Brooks Davis and Hongyan Xia and Edward Tomasz Napierala and Alexander Richardson and John Baldwin and David Chisnall and Jessica Clarke and Khilan Gudka and Alexandre Joannou and A. Theodore Markettos and Alfredo Mazzinghi and Robert M. Norton and Michael Roe and Peter Sewell and Stacey Son and Timothy M. Jones and Simon W. Moore and Peter G. Neumann and and Robert N. M. Watson},
conf = {Security and Privacy 2020},
booktitle = {\textbf{Security and Privacy 2020}: Proceedings of the 41st IEEE Symposium on Security and Privacy (SP)},
title = {Cornucopia: Temporal Safety for {CHERI} Heaps},
year = {2020},
volume = {},
issn = {2375-1207},
pages = {1507-1524},
keywords = {},
doi = {10.1109/SP40000.2020.00098},
pdf = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/2020oakland-cornucopia.pdf},
apollourl = {https://www.repository.cam.ac.uk/handle/1810/304040},
publisherurl = {https://doi.ieeecomputersociety.org/10.1109/SP40000.2020.00098},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
month = {may},
abstract = {Use-after-free violations of temporal memory safety continue to plague software systems, underpinning many high-impact exploits. The CHERI capability system shows great promise in achieving C and C++language spatial memory safety, preventing out-of-bounds accesses. Enforcing language-level temporal safety on CHERI requires capability revocation, traditionally achieved either via table lookups (avoided for performance in the CHERI design) or by identifying capabilities in memory to revoke them (similar to a garbage-collector sweep). CHERIvoke,a prior feasibility study, suggested that CHERI’s tagged capabilities could make this latter strategy viable, but modeled only architectural limits and did not consider the full implementation or evaluation of the approach.
Cornucopia is a lightweight capability revocation system for CHERI that implements non-probabilistic C/C++temporal memory safety for standard heap allocations. It extends the CheriBSD virtual-memory subsystem to track capability flow through memory and provides a concurrent kernel-resident revocation service that is amenable to multi-processor and hardware acceleration. We demonstrate an average overhead of less than 2\% and a worst-case of 8.9\% for concurrent revocation on compatible SPECCPU2006 benchmarks on a multi-core CHERI CPU on FPGA, and we validate Cornucopia against the Juliet test suite’s corpus of temporally unsafe programs. We test its compatibility with a large corpus of C programs by using a revoking allocator as the system allocator while booting multi-user CheriBSD. Cornucopia is a viable strategy for always-on temporal heap memory safety, suitable for production environments.
},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
recent = {true}
}
@inproceedings{TaDa2014,
year = {2014},
month = jul,
isbn = {978-3-662-44201-2},
booktitle = {\textbf{ECOOP 2014}},
conf = {ECOOP 2014},
volume = {8586},
series = {Lecture Notes in Computer Science},
editor = {Jones, Richard},
doi = {10.1007/978-3-662-44202-9_9},
title = {{TaDA}: A Logic for Time and Data Abstraction},
url = {http://dx.doi.org/10.1007/978-3-662-44202-9_9},
publisher = {Springer Berlin Heidelberg},
author = {da Rocha Pinto, Pedro and Dinsdale-Young, Thomas and Gardner, Philippa},
pages = {207-231},
language = {English},
abstract = {To avoid data races, concurrent operations should either be at distinct times or on distinct data. Atomicity is the abstraction that an operation takes effect at a single, discrete instant in time, with linearisability being a well-known correctness condition which asserts that concurrent operations appear to behave atomically. Disjointness is the abstraction that operations act on distinct data resource, with concurrent separation logics enabling reasoning about threads that appear to operate independently on disjoint resources.
We present TaDA, a program logic that combines the benefits of abstract atomicity and abstract disjointness. Our key contribution is the introduction of atomic triples, which offer an expressive approach to specifying program modules. By building up examples, we show that TaDA supports elegant modular reasoning in a way that was not previously possible.
}
}
@inproceedings{DBLP:conf/esop/GardnerNW14,
author = {Philippa Gardner and
Gian Ntzik and
Adam Wright},
title = {Local Reasoning for the {POSIX} File System},
booktitle = {\textbf{ESOP 2014}: Programming Languages and Systems - 23rd European Symposium on Programming,
Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2014, Grenoble, France},
conf = {ESOP 2014},
pages = {169--188},
year = {2014},
month = apr,
optcrossref = {DBLP:conf/esop/2014},
url = {http://dx.doi.org/10.1007/978-3-642-54833-8_10},
doi = {10.1007/978-3-642-54833-8_10},
timestamp = {Sun, 23 Mar 2014 10:48:25 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/esop/GardnerNW14},
bibsource = {dblp computer science bibliography, http://dblp.org},
abstract = {We provide a program logic for specifying a core subset of the sequential POSIX file system, and for reasoning abstractly about client programs working with the file system.}
}
@article{DBLP:journals/entcs/GardnerRWW14,
author = {Philippa Gardner and
Azalea Raad and
Mark J. Wheelhouse and
Adam Wright},
title = {Abstract Local Reasoning for Concurrent Libraries: Mind the Gap},
journal = {\textbf{MFPS 2014}: Electr. Notes Theor. Comput. Sci.},
conf = {MFPS 2014},
volume = {308},
pages = {147--166},
year = {2014},
month = jun,
url = {http://dx.doi.org/10.1016/j.entcs.2014.10.009},
doi = {10.1016/j.entcs.2014.10.009},
timestamp = {Tue, 04 Nov 2014 10:58:51 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/entcs/GardnerRWW14},
bibsource = {dblp computer science bibliography, http://dblp.org},
abstract = {We study abstract local reasoning for concurrent libraries. There are two main approaches: provide a specification of a library by abstracting from concrete reasoning about an implementation; or provide a direct abstract library specification, justified by refining to an implementation. Both approaches have a significant gap in their reasoning, due to a mismatch between the abstract connectivity of the abstract data structures and the concrete connectivity of the concrete heap representations. We demonstrate this gap using structural separation logic (SSL) for specifying a concurrent tree library and concurrent abstract predicates (CAP) for reasoning about a concrete tree implementation. The gap between the abstract and concrete connectivity emerges as a mismatch between the SSL tree predicates and CAP heap predicates. This gap is closed by an interface function I which links the abstract and concrete connectivity. In the accompanying technical report, we generalise our SSL reasoning and results to arbitrary concurrent data libraries.}
}
@inproceedings{daRochaPinto2016Modular,
title = {Modular Termination Verification for Non-blocking Concurrency},
author = {{da Rocha Pinto}, Pedro and Dinsdale-Young, Thomas and Gardner, Philippa and Sutherland, Julian},
booktitle = {\textbf{ESOP 2016}: Proceedings of the 25th European Symposium on Programming},
conf = {ESOP 2016},
year = {2016},
month = apr,
pages = {176--201},
url = {http://dx.doi.org/10.1007/978-3-662-49498-1_8},
doi = {10.1007/978-3-662-49498-1_8},
pdf = {http://www.doc.ic.ac.uk/~pmd09/research/publications/2016/esop/modular-termination-verification-for-non-blocking-concurrency.pdf},
abstract = {We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. With Total-TaDA, we can specify constraints on a thread's concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for non-blocking algorithms, e.g. a counter and a stack. Our specifications can express lock- and wait-freedom. More generally, they can express that one operation cannot impede the progress of another, a new non-blocking property we call non-impedance. Moreover, our approach is modular. We can verify the operations of a module independently, and build up modules on top of each other.},
project = { concurrency, tada }
}
@inproceedings{Ntzik2015Fault,
title = {{Fault-tolerant Resource Reasoning}},
author = {Ntzik, Gian and {da Rocha Pinto}, Pedro and Gardner, Philippa},
booktitle = {\textbf{APLAS 2015}: Proceedings of the 13th Asian Symposium on Programming Languages and Systems},
conf = {APLAS 2015},
year = {2015},
month = dec,
pages = {169--188},
url = {http://dx.doi.org/10.1007/978-3-319-26529-2_10},
doi = {10.1007/978-3-319-26529-2_10},
pdf = {http://www.doc.ic.ac.uk/~pmd09/research/publications/2015/aplas/fault-tolerant-resource-reasoning.pdf},
abstract = {Separation logic has been successful at verifying that programs do not crash due to illegal use of resources. The underlying assumption, however, is that machines do not fail. In practice, machines can fail unpredictably for various reasons, e.g. power loss, corrupting resources. Critical software, e.g. file systems, employ recovery methods to mitigate these effects. We introduce an extension of the Views framework to reason about such methods. We use concurrent separation logic as an instance of the framework to illustrate our reasoning, and explore programs using write-ahead logging, e.g. an ARIES recovery algorithm.}
}
@inproceedings{daRochaPinto2015Steps,
title = {{Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)}},
author = {{da Rocha Pinto}, Pedro and Dinsdale-Young, Thomas and Gardner, Philippa},
booktitle = {\textbf{MFPS 2015}: Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics},
conf = {MFPS 2015},
year = {2015},
month = jun,
pages = {3--18},
url = {http://www.sciencedirect.com/science/article/pii/S1571066115000699},
doi = {10.1016/j.entcs.2015.12.002},
pdf = {http://www.doc.ic.ac.uk/~pmd09/research/publications/2015/mfps/steps-in-modular-specifications-for-concurrent-modules.pdf},
abstract = {The specification of a concurrent program module is a difficult problem. The specifications must be strong enough to enable reasoning about the intended clients without reference to the underlying module implementation. We survey a range of verification techniques for specifying concurrent modules, in particular highlighting four key concepts: auxiliary state, interference abstraction, resource ownership and atomicity. We show how these concepts combine to provide powerful approaches to specifying concurrent modules.}
}
@inproceedings{icaptso-esop,
author = {Filip Sieczkowski and Kasper Svendsen and Lars Birkedal and Jean Pichon-Pharabod},
title = {A Separation Logic for Fictional Sequential Consistency},
optcrossref = {},
optkey = {},
booktitle = {\textbf{ESOP 2015}},
conf = {ESOP 2015},
optpages = {},
year = 2015,
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = apr,
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
doi = {10.1007/978-3-662-46669-8_30},
abstract = {To improve performance, modern multiprocessors and programming languages typically implement \emph{relaxed} memory models that
do not require all processors/threads to observe memory operations in
the same order. To relieve programmers from having to reason directly
about these relaxed behaviors, languages often provide efficient synchronization primitives and concurrent data structures with stronger high-level guarantees about memory reorderings. For instance, locks usually
ensure that when a thread acquires a lock, it can observe all memory
operations of the releasing thread, prior to the release. When used correctly, these synchronization primitives and data structures allow clients
to recover a fiction of a \emph{sequentially consistent} memory model.
In this paper we propose a new proof system, iCAP-TSO, that captures
this fiction formally, for a language with a TSO memory model. The
logic supports reasoning about libraries that directly exploit the relaxed
memory model to achieve maximum efficiency. When these libraries provide sufficient guarantees, the logic hides the underlying complexity and
admits standard separation logic rules for reasoning about their more
high-level clients.
}
}
@inproceedings{CoLoSL2015,
author = {Azalea Raad and Jules Villard and Philippa Gardner},
title = {{CoLoSL}: Concurrent Local Subjective Logic},
optcrossref = {},
optkey = {},
booktitle = {\textbf{ESOP 2015}},
conf = {ESOP 2015},
optpages = {},
year = {2015},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = apr,
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
doi = {10.1007/978-3-662-46669-8_29},
pdf = {http://www.doc.ic.ac.uk/~azalea/papers/CoLoSL.pdf},
abstract = {A key difficulty in verifying shared-memory concurrent programs is reasoning compositionally about each thread in isolation. Existing
verification techniques for fine-grained concurrency typically require reasoning about either the entire shared state or disjoint parts of the shared
state, impeding compositionality. This paper introduces the program logic
CoLoSL, where each thread is verified with respect to its subjective view
of the global shared state. This subjective view describes only that part of
the state accessed by the thread. Subjective views may arbitrarily overlap
with each other, and expand and contract depending on the resource
required by the thread. This flexibility gives rise to small specifications
and, hence, more compositional reasoning for concurrent programs. We
demonstrate our reasoning on a range of examples, including a concurrent
computation of a spanning tree of a graph.
}
}
@article{DBLP:journals/corr/ChakrabortyHSV15,
author = {Soham Chakraborty and
Thomas A. Henzinger and
Ali Sezgin and
Viktor Vafeiadis},
title = {Aspect-oriented linearizability proofs},
journal = {\textbf{Logical Methods in Computer Science}},
volume = {11},
number = {1},
pages = {1--33},
year = {2015},
month = apr,
url = {http://arxiv.org/abs/1502.07639},
doi = {10.2168/LMCS-11(1:20)2015},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/ChakrabortyHSV15},
bibsource = {dblp computer science bibliography, http://dblp.org},
abstract = {Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates. In response, we propose a more modular way of checking linearizability of concurrent queue algorithms that does not involve identifying linearization points. We reduce the task of proving linearizability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof. }
}
@inproceedings{ocaml14tls,
author = {Hannes Mehnert and David Kaloper Mersinjak},
title = {Transport {L}ayer {S}ecurity purely in {O}{C}aml},
booktitle = {Proceedings of the ACM OCaml 2014 Workshop},
conf = {OCaml 2014},
year = 2014,
month = sep,
url = {https://ocaml.org/meetings/ocaml/2014/ocaml2014_4.pdf},
abstract = {Transport Layer Security (TLS) is probably the most
widely deployed security protocol on the Internet. It is used to
setup virtual private networks, secure various services such as web
and email, etc. In this paper we describe our clean slate TLS
implementation developed in OCaml. Our motivating goals are
reliability, robustness, and API conciseness. While our
implementation is still a work in progress and lacks some of the
protocol features (such as client authentication and session
resumption), it already interoperates with other existing TLS
implementations. Preliminary performance evaluation shows that our
library is roughly five times slower compared to OpenSSL, but we
expect to improve our performance.}
}
@inproceedings{DBLP:conf/RelMiCS/HoareSMSVZO14,
author = {Tony Hoare and
Stephan van Staden and
Bernhard M{\"{o}}ller and
Georg Struth and
Jules Villard and
Huibiao Zhu and
Peter W. O'Hearn},
title = {Developments in Concurrent {Kleene} Algebra},
booktitle = {\textbf{RAMiCS 2014}: Relational and Algebraic Methods in Computer Science - 14th International
Conference, Marienstatt, Germany},
conf = {RAMiCS 2014},
pages = {1--18},
year = {2014},
month = apr,
optcrossref = {DBLP:conf/RelMiCS/2014},
url = {http://dx.doi.org/10.1007/978-3-319-06251-8_1},
doi = {10.1007/978-3-319-06251-8_1},
timestamp = {Tue, 08 Apr 2014 19:30:22 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/RelMiCS/HoareSMSVZO14},
bibsource = {dblp computer science bibliography, http://dblp.org},
abstract = {This report summarises recent progress in the research of its co-authors towards the construction of links between algebraic presentations of the principles of programming and the exploitation of concurrency in modern programming practice. The research concentrates on the construction of a realistic family of partial order models for Concurrent Kleene Algebra (aka, the Laws of Programming). The main elements of the model are objects and the events in which they engage. Further primitive concepts are traces, errors and failures, and transferrable ownership. In terms of these we can define other concepts which have proved useful in reasoning about concurrent programs, for example causal dependency and independence, sequentiality and concurrency, allocation and disposal, synchrony and asynchrony, sharing and locality, input and output.}
}
@misc{31c3tls,
optkey = {},
author = {David Kaloper Mer{\v{s}}injak and Hannes Mehnert},
title = {Trustworthy secure modular operating system engineering},
howpublished = {Invited talk at 31st Chaos Communication
Congress (31C3)},
month = jan,
year = 2015,
optnote = {},
optannote = {},
abstract = {We present Mirage OS, a modular library operating system developed from scratch in the functional programming language OCaml. Each service, called unikernel, is an OCaml application using libraries such as a TCP/IP stack, DNS. It is either compiled to a Xen virtual machine image or to a Unix binary (for development). State in 2014 is that it runs on x86 and arm, we implemented a clean-slate TLS (1.0, 1.1, 1.2), X.509, ASN.1 stack, crypto primitives, Off-the-record. We also have TCP/IP, HTTP, a persistent branchable store (similar to git) - all implemented in OCaml. A virtual machine serving data via https is roughly 2MB in size - no libc inside :)}
}
@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 = {},
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.
}
}
@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.
},
booktitle = {\textbf{USENIX Security 2015}: 24th {USENIX} Security Symposium, Washington,
D.C., USA},
conf = {USENIX Security 2015},
pages = {223--238},
year = {2015},
month = aug,
optcrossref = {DBLP:conf/uss/2015},
url = {https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/kaloper-mersinjak},
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}
}
@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.
},
booktitle = {\textbf{SOSP 2015}: Proceedings of the 25th Symposium on Operating Systems Principles,
Monterey, CA, USA},
conf = {SOSP 2015},
pages = {38--53},
year = {2015},
month = oct,
optcrossref = {DBLP:conf/sosp/2015},
url = {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}
}
@inproceedings{nqsb-testing,
author = {David Kaloper-Mer{\v s}injak and Hannes Mehnert},
title = {Not-quite-so-broken {TLS} 1.3 mechanised conformance checking},
booktitle = {{TLSv1.3} -- Ready or Not? ({TRON}) workshop},
conf = {TRON workshop 2016},
year = {2016},
month = feb,
pdf = {https://www.cl.cam.ac.uk/~hm519/tron.pdf},
abstract = {We present a set of tools to aid TLS 1.3 implementors, all derived from a single TLS implementation/model. These include an automated offline TLS protocol conformance checker, a test oracle validating recorded sessions, a tool replicating recorded sessions with other implementations, and an interactive online handshake visualisation.
The conformance checker repeatedly runs a user-provided TLS implementation, attempting to establish TLS sessions with it; the checker explores the TLS parameter space to determine feature coverage of the provided implementation. The test oracle takes a recorded session between two endpoints and decides whether the session was conformant with the specification. The replication utility re-runs one side of a recorded session against another TLS implementation, and observes its behaviour. The online visualisation accepts connections from clients and presents the TLS session as an interactive sequence diagram.
All of these tools are based on our clean-slate nqsb-TLS implementation/model. It already supports TLS 1.0-1.2, and interoperates with a broad range of other TLS implementations. We are currently extending nqsb-TLS with TLS 1.3 support, and tracking the progress of the TLS 1.3 draft, adapting our implementation/model accordingly.
We invite the community to use our tools while implementing the TLS 1.3 RFC, and provide feedback on deviations in the interpretation thereof. This process enables the community to converge to a single, mechanically checkable TLS 1.3 model, as implemented by nqsb-TLS.}
}
@inproceedings{biglater,
author = {Kasper Svendsen and Filip Sieczkowski and Lars Birkedal},
title = {Transfinite Step-indexing: Decoupling Concrete and Logical Steps},
booktitle = {\textbf{ESOP 2016}},
conf = {ESOP 2016},
year = 2016,
month = apr,
pages = {727--751},
url = {http://dx.doi.org/10.1007/978-3-662-49498-1_28},
doi = {10.1007/978-3-662-49498-1_28},
pdf = {http://www.cs.au.dk/~birke/papers/biglater-conf.pdf},
abstract = { Step-indexing has proven to be a powerful technique for defining logical relations for languages with advanced type systems and models of expressive program logics. In both cases, the model is stratified using natural numbers to solve a recursive equation that has no naive solutions. As a result of this stratification, current models require that each unfolding of the recursive equation -- each logical step -- must coincide with a concrete reduction step. This tight coupling is problematic for applications where the number of logical steps cannot be statically bounded.
In this paper we demonstrate that this tight coupling between logical and concrete steps is artificial and show how to loosen it using transfinite step-indexing. We present a logical relation that supports an arbitrary but finite number of logical steps for each concrete step. }
}
@inproceedings{Ntzik2015Reasoning,
title = {{Reasoning about the {POSIX} File System: Local Update and Global Pathnames}},
author = {Ntzik, Gian and Gardner, Philippa},
booktitle = {\textbf{OOPSLA 2015}: Proceedings of the 30th Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications},
conf = {OOPSLA 2015},
year = {2015},
month = oct,
abstract = {We introduce a program logic for specifying a core sequential subset of the POSIX file system and for reasoning abstractly about client programs working with the file system. The challenge is to reason about the combination of local directory update and global pathname traversal (including '..' and symbolic links) which may overlap the directories being updated. Existing reasoning techniques are either based on first-order logic and do not scale, or on separation logic and can only handle linear pathnames (no '..' or symbolic links). We introduce fusion logic for reasoning about local update and global pathname traversal, introducing a novel effect frame rule to propagate the effect of a local update on overlapping pathnames. We apply our reasoning to the standard recursive remove utility (rm -r), discovering bugs in well-known implementations.}
}
@inproceedings{DBLP:conf/vstte/SezginT15,
author = {Ali Sezgin and
Serdar Tasiran},
title = {Moving Around: Lipton's Reduction for {TSO} - (Regular Submission)},
booktitle = {\textbf{VSTTE 2015}: Verified Software: Theories, Tools, and Experiments - 7th International
Conference, San Francisco, CA, USA.
Revised Selected Papers},
conf = {VSTTE 2015},
pages = {165--182},
year = {2015},
month = jul,
optcrossref = {DBLP:conf/vstte/2015},
url = {http://dx.doi.org/10.1007/978-3-319-29613-5_10},
doi = {10.1007/978-3-319-29613-5_10},
timestamp = {Fri, 12 Feb 2016 10:43:40 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/vstte/SezginT15},
bibsource = {dblp computer science bibliography, http://dblp.org},
abstract = {We generalize Lipton’s reduction theory, hitherto limited to SC, for TSO programs. We demonstrate the use of our theory by specifying the conditions under which a particular write is SC-like (i.e. placing a fence immediately after the write does not constrain the behavior of the overall program) and a library implementation can be safely used (i.e. compositionality). Our theory is complete: a program has only SC behaviors iff there is a proof that establishes that every write in the program is SC-like. We adapt the notion of program abstraction to TSO analysis via our theory. We define precisely what is meant by abstraction, and propose a methodology by which one can obtain via abstraction SC summaries of a program which may have non-SC behaviors. Finally, we show how checking whether a write instruction is SC-like can be mechanized. We describe a transformation in which the execution of each thread of the original program (under TSO) is simulated by the execution of two tightly coupled threads in the new program (under SC).}
}
@inproceedings{GomesStruth16,
author = {Victor B. F. Gomes and
Georg Struth},
title = {Modal {K}leene algebra applied to program correctness},
booktitle = {\textbf{FM 2016}: Formal Methods -- 21st International Symposium,
Limassol},
conf = {FM 2016},
year = {2016},
month = nov,
editor = {John S. Fitzgerald and
Stefania Gnesi and
Constance L. Heitmeyer},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
pages = {310--325},
opturl = {http://dx.doi.org/10.1007/978-3-319-48989-6_19},
doi = {10.1007/978-3-319-48989-6_19},
abstract = {
Modal Kleene algebras are relatives of dynamic logics that support
program construction and verification by equational reasoning. We
describe their application in implementing versatile program
correctness components in interactive theorem provers such as
Isabelle/HOL. Starting from a weakest precondition based component
with a simple relational store model, we show how variants for Hoare
logic, strongest postconditions and program refinement can be built
in a principled way. Modularity of the approach is demonstrated
by variants that capture program termination and recursion,
memory models for programs with pointers, and program trace
semantics.
},
url = {https://www.repository.cam.ac.uk/handle/1810/260625},
pdf = {http://www.cl.cam.ac.uk/~pes20/rems/papers/GomesStruthMKA.pdf}
}
@inproceedings{KSB17,
author = {Morten Krogh-Jespersen and
Kasper Svendsen and
Lars Birkedal},
title = {A Relational Model of Types-and-Effects in Higher-Order
Concurrent Separation Logic},
booktitle = {\textbf{POPL 2017}: The 44st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
Programming Languages, Paris, France},
optpages = {179--192},
year = {2017},
conf = {POPL 2017},
month = jan,
isbn = {978-1-4503-4660-3},
location = {Paris, France},
pages = {218--231},
numpages = {14},
url = {http://doi.acm.org/10.1145/3009837.3009877},
doi = {10.1145/3009837.3009877},
acmid = {3009877},
publisher = {ACM},
address = {New York, NY, USA},
abstract = {
Recently we have seen a renewed interest in programming languages that tame the complexity of state and concurrency through refined type systems with more fine-grained control over effects. In addition to simplifying reasoning and eliminating whole classes of bugs, statically tracking effects opens the door to advanced compiler optimizations.
In this paper we present a relational model of a type-and-effect system for a higher-order, concurrent programming language. The model precisely captures the semantic invariants expressed by the effect annotations. We demonstrate that these invariants are strong enough to prove advanced program transformations, including automatic parallelization of expressions with suitably disjoint effects. The model also supports refinement proofs between abstract data types implementations with different internal data representations, including proofs that fine-grained concurrent algorithms refine their coarse-grained counterparts. This is the first model for such an expressive language that supports both effect-based optimizations and data abstraction.
The logical relation is defined in Iris, a state-of-the-art higher-order concurrent separation logic. This greatly simplifies proving well-definedness of the logical relation and also provides us with a powerful logic for reasoning in the model.}
}
@inproceedings{Caper,
author = {Thomas Dinsdale{-}Young and
Pedro da Rocha Pinto and
Kristoffer Just Andersen and
Lars Birkedal},
title = {{Caper: Automatic Verification for Fine-grained Concurrency}},
booktitle = {Proc. \textbf{ESOP 2017}: 26th European Symposium on Programming},
conf = {ESOP 2017},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
year = {2017},
pdf = {https://www.doc.ic.ac.uk/~pmd09/research/publications/2017/esop/caper-automatic-verification-for-fine-grained-concurrency.pdf},
month = apr,
abstract = {Recent program logics based on separation logic emphasise a modular approach to proving functional correctness for fine-grained concurrent programs. However, these logics have no automation support. In this paper, we present Caper, a prototype tool for automated reasoning in such a logic. Caper is based on symbolic execution, integrating reasoning about interference on shared data and about ghost resources that are used to mediate this interference. This enables Caper to verify the functional correctness of fine-grained concurrent algorithms.}
}
@inproceedings{Maps,
author = {Shale Xiong and
Pedro da Rocha Pinto and
Gian Ntzik and
Philippa Gardner},
title = {{Abstract Specifications for Concurrent Maps}},
booktitle = {Proc. \textbf{ESOP 2017}: 26th European Symposium on Programming},
conf = {ESOP 2017},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
year = {2017},
month = apr,
pdf = {https://www.doc.ic.ac.uk/~pmd09/research/publications/2017/esop/abstract-specifications-for-concurrent-maps.pdf},
abstract = {Despite recent advances in reasoning about concurrent data structure libraries, the largest implementations in java.util.concurrent have yet to be verified. The key issue lies in the development of modular specifications, which provide clear logical boundaries between clients and implementations. A solution is to use recent advances in fine-grained concurrency reasoning, in particular the introduction of abstract atomicity to concurrent separation logic reasoning. We present two specifications of concurrent maps, both providing the clear boundaries we seek. We show that these specifications are equivalent, in that they can be built from each other. We show how we can verify client programs, such as a concurrent set and a producer-consumer client. We also give a substantial first proof that the main operations of ConcurrentSkipListMap in java.util.concurrent satisfy the map specification. This work demonstrates that we now have the technology to verify the largest implementations in java.util.concurrent.}
}
@inproceedings{ocaml16conex,
author = {Hannes Mehnert and Louis Gesbert},
title = {Conex --- establishing trust into data repositories},
booktitle = {Proceedings of the ACM \textbf{OCaml 2016} Workshop},
conf = {OCaml 2016},
year = 2016,
month = sep,
url = {https://github.com/hannesm/conex-paper/raw/master/paper.pdf},
abstract = {Opam is a software update system, responsible for
discovering, downloading, building, and installing packages from
community repositories. The data and metadata at each step should be
authenticated to originate from a (transitively) trusted author. Opam
does not include any mechanism to authenticate any step at the moment.
We propose conex, which establishes digital signatures from the package
author to the user. Using conex, neither the distribution server nor
the transport layer need to be trusted. Clients will install
authenticated packages, and notice conex only if signatures cannot be
verified. Authors need to adapt their workflow slightly, an updated
opam publish will be developed. Janitors (repository maintainers) need
to adapt their workflow to emit cryptographic signatures to the
repository (in addition to pressing merge PR buttons).}
}
@inproceedings{ocaml16libtls,
author = {Enguerrand Decorne and Jeremy Yallop and David Mer{\v{s}}injak},
title = {OCaml inside: a drop-in replacement for libtls (extended abstract)},
booktitle = {Proceedings of the ACM \textbf{OCaml 2016} Workshop},
conf = {OCaml 2016},
year = 2016,
month = sep,
url = {https://www.cl.cam.ac.uk/users/jdy22/papers/ocaml-inside-a-drop-in-replacement-for-libtls.pdf},
abstract = {The C programming language pervades systems software. An operating
system in the Unix tradition consists of a kernel, written
in C, and a collection of libraries and executables, also written in
C, which communicate in large part via APIs defined as C types
and functions. Systems built in C typically suffer from a number of
problems, ranging from buffer overflows and other violations that
follow inevitably from unrestricted access to memory, to awkward
APIs that result from an inexpressive type system and a lack of
automatic memory management.
The openssl library, which implements the cryptographic protocols
TLS and SSL, suffers from both these problems. The lack
of bounds checking in C led to the notorious Heartbleed bug in
2014; a study two years earlier found that almost no clients of
openssl use the library correctly, apparently due to its unhelpful
interface (Georgiev et al. 2012).
In response to the Heartbleed bug, the OpenBSD team created
libressl, a fork of openssl with the aim of correcting the deficiencies.
One early fruit of the libressl project is libtls, a
much simpler, more disciplined interface to the TLS protocol implementation
in libressl.
However, libtls is still built in C, and so is still vulnerable
to potential buffer overflows, type errors, and similar defects. In
this talk we describe one approach to avoiding these problems,
namely replacing libtls with a fully compatible library written in
OCaml. Our library, libnqsb-tls1, matches the libtls function-for-function, but the implementation contains no C; instead, it it
wraps the pure OCaml TLS implementation ocaml-tls (Kaloper-Mer{\v{s}}injak et al. 2015)}
}
@inproceedings{haas_et_al:LIPIcs:2016:6180,
author = {Andreas Haas and Thomas A. Henzinger and Andreas Holzer and Christoph M. Kirsch and Michael Lippautz and Hannes Payer and Ali Sezgin and Ana Sokolova and Helmut Veith},
abstract = {The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Nevertheless, for applications that do not require all guarantees offered by linearizability, recent research has focused on improving performance and scalability of concurrent data structures by relaxing their semantics.
In this paper, we present local linearizability, a relaxed consistency
condition that is applicable to container-type concurrent data
structures like pools, queues, and stacks. While linearizability requires that the effect of each operation is observed by all threads at the same time, local linearizability only requires that for each thread T, the effects of its local insertion operations and the effects of those removal operations that remove values inserted by T are observed by all threads at the same time. We investigate theoretical and practical properties of local linearizability and its relationship to many existing consistency conditions. We present a generic implementation method for locally linearizable data structures that uses existing linearizable data structures as building blocks. Our implementations show performance and scalability improvements over the original building blocks and outperform the fastest existing container-type implementations.},
title = {{Local Linearizability for Concurrent Container-Type Data Structures}},
booktitle = {27th International Conference on Concurrency Theory (\textbf{CONCUR 2016})},
conf = {CONCUR 2016},
pages = {6:1--6:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
isbn = {978-3-95977-017-0},
issn = {1868-8969},
year = {2016},
month = aug,
volume = {59},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
doi = {10.4230/LIPIcs.CONCUR.2016.6},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2016/6180/pdf/LIPIcs-CONCUR-2016-6.pdf}
}
@article{GomesGHSW16,
author = {Victor B. F. Gomes and
Walter Guttmann and
Peter H{\"{o}}fner and
Georg Struth and
Tjark Weber},
title = {Kleene Algebras with Domain},
journal = {Archive of Formal Proofs},
volume = {2016},
year = {2016},
month = apr,
url = {https://www.isa-afp.org/entries/KAD.shtml},
abstract = {Kleene algebras with domain are Kleene algebras endowed with an operation that maps each element of the algebra to its domain of definition (or its complement) in abstract fashion. They form a simple algebraic basis for Hoare logics, dynamic logics or predicate transformer semantics. We formalise a modular hierarchy of algebras with domain and antidomain (domain complement) operations in Isabelle/HOL that ranges from domain and antidomain semigroups to modal Kleene algebras and divergence Kleene algebras. We link these algebras with models of binary relations and program traces. We include some examples from modal logics, termination and program analysis.}
}
@article{GomesS16,
author = {Victor B. F. Gomes and
Georg Struth},
title = {Program Construction and Verification Components Based on {K}leene Algebra},
journal = {Archive of Formal Proofs},
volume = {2016},
year = {2016},
month = jun,
url = {https://www.isa-afp.org/entries/Algebraic_VCs.shtml},
abstract = {Variants of Kleene algebra support program construction and verification by algebraic reasoning. This entry provides a verification component for Hoare logic based on Kleene algebra with tests, verification components for weakest preconditions and strongest postconditions based on Kleene algebra with domain and a component for step-wise refinement based on refinement Kleene algebra with tests. In addition to these components for the partial correctness of while programs, a verification component for total correctness based on divergence Kleene algebras and one for (partial correctness) of recursive programs based on domain quantales are provided. Finally we have integrated memory models for programs with pointers and a program trace semantics into the weakest precondition component.}
}
@inproceedings{Raad2016Verifying,
title = {Verifying Concurrent Graph Algorithms},
author = {Raad, Azalea and Hobor, Aquinas and Villard, Jules and Gardner, Philippa},
booktitle = {Proc. \textbf{APLAS 2016}: 14th Asian Symposium on Programming Languages and Systems},
conf = {APLAS 2016},
year = {2016},
month = nov,
pages = {314--334},
url = {http://dx.doi.org/10.1007/978-3-319-47958-3_17},
doi = {10.1007/978-3-319-47958-3_17},
abstract = {We show how to verify four challenging concurrent finegrained graph-manipulating algorithms, including graph copy, a speculatively parallel Dijkstra, graph marking and spanning tree. We develop a reasoning method for such algorithms that dynamically tracks the contributions and responsibilities of each thread operating on a graph, even in cases of arbitrary recursive thread creation. We demonstrate how to use a logic without abstraction (CoLoSL) to carry out abstract reasoning in the style of iCAP, by building the abstraction into the proof structure rather than incorporating it into the semantic model of the logic.}
}
@inproceedings{Raad2016DOM,
title = {{DOM:} Specification and Client Reasoning},
author = {Raad, Azalea and {Fragoso Santos}, Jos{\'{e}} and Gardner, Philippa},
booktitle = {Proc. \textbf{APLAS 2016}: 14th Asian Symposium on Programming Languages and Systems},
conf = {APLAS 2016},
year = {2016},
month = nov,
pages = {401--422},
url = {http://dx.doi.org/10.1007/978-3-319-47958-3_21},
doi = {10.1007/978-3-319-47958-3_21},
abstract = {We present an axiomatic specification of a key fragment of DOM using structural separation logic. This specfication allows us to develop modular reasoning about client programs that call the DOM.}
}
@inproceedings{Kaloper-Mersinjak:2016:GPD:2976022.2976028,
author = {Kaloper-Mer\v{s}injak, David and Yallop, Jeremy},
title = {Generic Partially-static Data (Extended Abstract)},
booktitle = {Proceedings of the 1st International Workshop on Type-Driven Development},
conf = {TyDe 2016},
series = {TyDe 2016},
year = {2016},
month = sep,
isbn = {978-1-4503-4435-7},
location = {Nara, Japan},
pages = {39--40},
numpages = {2},
url = {http://doi.acm.org/10.1145/2976022.2976028},
doi = {10.1145/2976022.2976028},
acmid = {2976028},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {generic programming, partial evaluation, staging},
pdf = {http://dl.acm.org/ft_gateway.cfm?id=2976028&ftid=1783813&dwn=1&CFID=738558588&CFTOKEN=28095393},
abstract = {We describe a generic approach to defining partially-static data
and corresponding operations.}
}
@phdthesis{Ntzik2017Reasoning,
author = {Ntzik, Gian},
title = {Reasoning About {POSIX} File Systems},
school = {Imperial College London},
month = sep,
year = {2016},
opttype = {phdthesis},
url = {https://psvg.doc.ic.ac.uk/publications/Ntzik2017Reasoning.pdf},
abstract = {POSIX is a standard for operating systems, with a substantial
part devoted to specifying file-system operations. File-system operations
exhibit complex concurrent behaviour, comprising multiple actions affecting
different parts of the state: typically, multiple atomic reads followed by
an atomic update. However, the standard's description of concurrent
behaviour is unsatisfactory: it is fragmented; contains ambiguities; and is
generally under-specified. We provide a formal concurrent specification of
POSIX file systems and demonstrate scalable reasoning for clients. Our
speciation is based on a concurrent specification language, which uses a
modern concurrent separation logic for reasoning about abstract atomic
operations, and an associated refinement calculus. Our reasoning about
clients highlights an important difference between reasoning about modules
built over a heap, where the interference on the shared state is restricted
to the operations of the module, and modules built over a file system, where
the interference cannot be restricted as the file system is a public
namespace. We introduce specifications conditional on context invariants
used to restrict the interference, and apply our reasoning to lock files and
named pipes. Program reasoning based on separation logic has been successful
at verifying that programs do not crash due to illegal use of resources,
such invalid memory accesses. The underlying assumption of separation
logics, however, is that machines do not fail. In practice, machines can
fail unpredictably for various reasons, such as power loss, corrupting
resources or resulting in permanent data loss. Critical software, such as
file systems and databases, employ recovery methods to mitigate these
effects. We introduce an extension of the Views framework to reason about
programs in the presence of such events and their associated recovery
methods. We use concurrent separation logic as an instance of the framework
to illustrate our reasoning, and explore programs using write-ahead logging,
such a stylised ARIES recovery algorithm.}
}
@phdthesis{daRochaPinto2017Reasoning,
author = {{da Rocha Pinto}, Pedro},
title = {Reasoning with Time and Data Abstractions},
school = {Imperial College London},
year = {2016},
month = sep,
url = {https://psvg.doc.ic.ac.uk/publications/daRochaPinto2017Reasoning.pdf},
abstract = {In this thesis, we address the problem of verifying the
functional correctness of concurrent programs, with emphasis on fine-grained
concurrent data structures. Reasoning about such programs is challenging
since data can be concurrently accessed by multiple threads: the reasoning
must account for the interference between threads, which is often subtle. To
reason about interference, concurrent operations should either be at
distinct times or on distinct data. We present TaDA, a sound program logic
for verifying clients and implementations that use abstract specifications
that incorporate both abstract atomicity---the abstraction that operations
take effect at a single, discrete instant in time---and abstract
disjointness---the abstraction that operations act on distinct data resources.
Our key contribution is the introduction of atomic triples, which offer an
expressive approach for specifying program modules. We also present
Total-TaDA, a sound extension of TaDA with which we can verify total
correctness of concurrent programs, i.e. that such programs both produce the
correct result and terminate. With Total-TaDA, we can specify constraints on
a thread=92s concurrent environment that are necessary to guarantee
termination. This allows us to verify total correctness for nonblocking
algorithms and express lock- and wait-freedom. More generally, the abstract
specifications can express that one operation cannot impede the progress of
another, a new non-blocking property that we call non-impedance. Finally, we
describe how to extend TaDA for proving abstract atomicity for data
structures that make use of helping---where one thread is performing an
abstract operation on behalf of another---and speculation---where an abstract
operation is determined by future behaviour.}
}
@phdthesis{Raad2017Abstraction,
author = {Raad, Azalea},
title = {Abstraction, Refinement and Concurrent Reasoning},
school = {Imperial College London},
year = {2016},
month = sep,
url = {https://psvg.doc.ic.ac.uk/publications/Raad2017Abstraction.pdf},
opttype = {phdthesis},
abstract = {This thesis explores the challenges in abstract library
specification, library refinement and reasoning about fine-grained
concurrent programs.For abstract library specification, this thesis applies
structural separation logic (SSL) to formally specify the behaviour of
several libraries in an abstract, local and compositional manner. This
thesis further generalises the theory of SSL to allow for library
specifications that are language independent. Most notably, we specify a
fragment of the Document Object Model (DOM) library. This result is
compelling as it significantly improves upon existing DOM formalisms in that
the specifications produced are local, compositional and
language-independent. Concerning library refinement, this thesis explores
two existing approaches to library refinement for separation logic,
identifying their advantages and limitations in different settings. This
thesis then introduces a hybrid approach to refinement, combining the
strengths of both techniques for simple scalable library refinement. These
ideas are then adapted to refinement for SSL by presenting a JavaScript
implementation of the DOM fragment studied and establishing its correctness
with respect to its specification using the hybrid refinement approach.As to
concurrent reasoning, this thesis introduces concurrent local subjective
logic (CoLoSL) for compositional reasoning about fine-grained concurrent
programs. CoLoSL introduces subjective views, where each thread is verified
with respect to a customised local view of the state, as well as the general
composition and framing of interference relations, allowing for better proof
reuse.}
}
@inproceedings{Cerone2017Algebraic,
author = {Cerone, Andrea and Gotsman, Alexey and Yang, Hongseok},
title = {Algebraic Laws for Weak Consistency},
booktitle = {\textbf{CONCUR 2017}: Proceedings of 28th International Conference on Concurrency Theory},
conf = {CONCUR 2017},
year = {2017},
month = sep,
url = {https://psvg.doc.ic.ac.uk/publications/Cerone2017Algebraic.html},
doi = {10.4230/LIPIcs.CONCUR.2017.26},
abstract = {Modern distributed systems often rely on so called
weakly-consistent databases, which achieve scalability by sacrificing the
consistency guarantee of distributed transaction processing. Such databases
have been formalised in two different styles, one based on abstract
executions and the other based on dependency graphs. The choice between
these styles has been made according to intended applications. The former
has been used for specifying and verifying the implementation of these
databases, while the latter for proving properties of client programs of the
databases. In this paper, we present a set of novel algebraic laws (i.e.
inequations) that connect these two styles of specifications. The laws
relate binary relations used in a specification based on abstract
executions, to those used in a specification based on dependency graphs. We
then show that this algebraic connection gives rise to so called robustness
criteria, conditions which ensure that a client program of a
weakly-consistent database does not exhibit anomalous behaviours due to weak
consistency. These criteria make it easy to reason about these client
programs, and may become a basis for dynamic or static program analyses. For
a certain class of consistency models specifications, we prove a full
abstraction result that connects the two styles of specifications.}
}
@inproceedings{DBLP:conf/cade/SantosGMN17,
author = {Jos{\'{e}} Fragoso Santos and
Philippa Gardner and
Petar Maksimovic and
Daiva Naudziuniene},
editor = {Leonardo de Moura},
title = {Towards Logic-Based Verification of {JavaScript} Programs},
booktitle = {\textbf{CADE 2017}: 26th International
Conference on Automated Deduction},
conf = {CADE 2017},
series = {Lecture Notes in Computer Science},
volume = {10395},
pages = {8--25},
publisher = {Springer},
month = aug,
year = {2017},
opturl = {https://doi.org/10.1007/978-3-319-63046-5_2},
url = {https://psvg.doc.ic.ac.uk/publications/FragosoSantos2017Towards.html},
doi = {10.1007/978-3-319-63046-5_2},
timestamp = {Wed, 12 Jul 2017 10:22:36 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/cade/SantosGMN17},
bibsource = {dblp computer science bibliography},
abstract = {In this position paper, we argue for what we believe is a correct pathway to achieving scalable symbolic verification of JavaScript based on separation logic. We highlight the difficulties imposed by the language, the current state-of-the-art in the literature, and the sequence of steps that needs to be taken. We briefly describe Open image in new window , our semi-automatic toolchain for JavaScript verification.}
}
@inproceedings{gomes-oopsla2017,
author = {Victor B. F. Gomes and Martin Kleppmann and Dominic P. Mulligan and Alastair R. Beresford},
title = {Verifying Strong Eventual Consistency in Distributed Systems},
booktitle = {\textbf{OOPSLA 2017}: Proceedings of the {ACM} {SIGPLAN} International
Conference on Object-Oriented Programming, Systems, Languages, and
Applications ({OOPSLA})},
conf = {OOPSLA 2017},
pages = {109:1--109:28},
articleno = {109},
numpages = {28},
url = {http://doi.acm.org/10.1145/3133933},
doi = {10.1145/3133933},
year = {2017},
month = oct,
note = {Distinguished Paper award},
abstract = {Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network. However, despite decades of research, algorithms for achieving consistency in replicated systems are still poorly understood. Indeed, many published algorithms have later been shown to be incorrect, even some that were accompanied by supposed mechanised proofs of correctness. In this work, we focus on the correctness of Conflict-free Replicated Data Types (CRDTs), a class of algorithm that provides strong eventual consistency guarantees for replicated data. We develop a modular and reusable framework in the Isabelle/HOL interactive proof assistant for verifying the correctness of CRDT algorithms. We avoid correctness issues that have dogged previous mechanised proofs in this area by including a network model in our formalisation, and proving that our theorems hold in all possible network behaviours. Our axiomatic network model is a standard abstraction that accurately reflects the behaviour of real-world computer networks. Moreover, we identify an abstract convergence theorem, a property of order relations, which provides a formal definition of strong eventual consistency. We then obtain the first machine-checked correctness theorems for three concrete CRDTs: the Replicated Growable Array, the Observed-Remove Set, and an Increment-Decrement Counter. We find that our framework is highly reusable, developing proofs of correctness for the latter two CRDTs in a few hours and with relatively little CRDT-specific code.}
}
@inproceedings{matache-aplas2017,
author = {Cristina Matache and Victor B. F. Gomes and Dominic P. Mulligan},
title = {Programming and proving with classical types},
booktitle = {\textbf{APLAS 2017}: Proceedings of the 15th {Asian} Symposium on Programming Languages and Systems},
conf = {APLAS 2017},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-71237-6_11},
doi = {10.1007/978-3-319-71237-6_11},
month = nov,
optnote = {To appear},
abstract = {
The propositions-as-types correspondence is ordinarily presented as linking the metatheory of typed $\lambda $-calculi and the proof theory of intuitionistic logic. Griffin observed that this correspondence could be extended to classical logic through the use of control operators. This observation set off a flurry of further research, leading to the development of Parigot's $\lambda \mu $-calculus. In this work, we use the $\lambda \mu $-calculus as the foundation for a system of proof terms for classical first-order logic. In particular, we define an extended call-by-value $\lambda \mu $-calculus with a type system in correspondence with full classical logic. We extend the language with polymorphic types, add a host of data types in `direct style', and prove several metatheoretical properties. All of our proofs and definitions are mechanised in Isabelle/HOL, and we automatically obtain an interpreter for a system of proof terms cum programming language---called $\mu $ML---using Isabelle's code generation mechanism. Atop our proof terms, we build a prototype LCF-style interactive theorem prover---called $\mu $TP---for classical first-order logic, capable of synthesising $\mu $ML programs from completed tactic-driven proofs. We present example closed $\mu $ML programs with classical tautologies for types, including some inexpressible as closed programs in the original $\lambda \mu $-calculus, and some example tactic-driven $\mu $TP proofs of classical tautologies.}
}
@article{DBLP:journals/corr/BirkedalDJST17,
author = {Lars Birkedal and
Thomas Dinsdale{-}Young and
Guilhem Jaber and
Kasper Svendsen and
Nikos Tzevelekos},
title = {Trace Properties from Separation Logic Specifications},
journal = {CoRR},
volume = {abs/1702.02972},
year = {2017},
month = feb,
url = {http://arxiv.org/abs/1702.02972},
pdf = {https://arxiv.org/pdf/1702.02972},
timestamp = {Wed, 07 Jun 2017 14:40:31 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/BirkedalDJST17},
bibsource = {dblp computer science bibliography, http://dblp.org},
abstract = {We propose a formal approach for relating abstract separation logic library specifications with the trace properties they enforce on interactions between a client and a library. Separation logic with abstract predicates enforces a resource discipline that constrains when and how calls may be made between a client and a library. Intuitively, this can enforce a protocol on the interaction trace. This intuition is broadly used in the separation logic community but has not previously been formalised. We provide just such a formalisation. Our approach is based on using wrappers which instrument library code to induce execution traces for the properties under examination. By considering a separation logic extended with trace resources, we prove that when a library satisfies its separation logic specification then its wrapped version satisfies the same specification and, moreover, maintains the trace properties as an invariant. Consequently, any client and library implementation that are correct with respect to the separation logic specification will satisfy the trace properties.}
}
@inproceedings{SvendsenEtAl2018,
author = {Svendsen, Kasper and Pichon-Pharabod, Jean and Doko, Marko and Lahav, Ori and Vafeiadis, Viktor},
title = {A separation logic for a promising semantics},
booktitle = {\textbf{{ESOP 2018}}},
pdf = {https://www.cl.cam.ac.uk/~jp622/a_separation_logic_for_a_promising_semantics.pdf},
conf = {{ESOP 2018}},
year = {2018},
abstract = {We present SLR, the first expressive program logic for reasoning about concurrent programs under a weak memory model addressing the out-of-thin-air problem. Our logic includes the standard features from existing logics, such as RSL and GPS, that were previously known to be sound only under stronger memory models: (1) separation, (2) per-location invariants, and (3) ownership transfer via release-acquire synchronisation—as well as novel features for reasoning about (4) the absence of out-of-thin-air behaviours and (5) coherence. The logic is proved sound over the recent ``promising'' memory model of Kang et al., using a substantially different argument to soundness proofs of logics for simpler memory models.}
}
@article{Bauereiss:2017,
author = {Bauerei{\ss}, Thomas
and Pesenti Gritti, Armando
and Popescu, Andrei
and Raimondi, Franco},
title = {CoSMed: A Confidentiality-Verified Social Media Platform},
journal = {\textbf{J. Automated Reasoning}},
optjournal = {\textbf{Journal of Automated Reasoning}},
year = {2017},
month = dec,
day = {02},
abstract = {This paper describes progress with our agenda of formal verification of information flow security for realistic systems. We present CoSMed, a social media platform with verified document confidentiality. The system's kernel is implemented and verified in the proof assistant Isabelle/HOL. For verification, we employ the framework of Bounded-Deducibility (BD) Security, previously introduced for the conference system CoCon. CoSMed is a second major case study in this framework. For CoSMed, the static topology of declassification bounds and triggers that characterized previous instances of BD Security has to give way to a dynamic integration of the triggers as part of the bounds. We also show that, from a theoretical viewpoint, the removal of triggers from the notion of BD Security does not restrict its expressiveness.},
issn = {1573-0670},
doi = {10.1007/s10817-017-9443-3},
url = {https://doi.org/10.1007/s10817-017-9443-3}
}
@article{Gardner2017Verified,
author = {Gardner, Philippa},
title = {Verified trustworthy software systems},
optjournal = {\textbf{Philosophical Transactions of the Royal Society of London A}: Mathematical, Physical and Engineering Sciences},
journal = {\textbf{Philosophical Transactions of the Royal Society of London A}},
year = {2017},
volume = {375},
number = {2104},
month = sep,
issn = {1364-503X},
abstract = {Modern society is faced with a fundamental problem:
the reliability of complex, evolving software systems on
which society critically depends cannot be guaranteed by
the established, non-mathematical computer engineering
techniques such as informal prose specification and
ad hoc testing. The situation is worsening: modern
companies are moving fast, leaving little time for code
analysis and testing; the behaviour of concurrent and
distributed programs cannot be adequately assessed
using traditional testing methods; users of mobile
applications often neglect to apply software fixes;
and malicious users increasingly exploit even simple
programming errors, causing major security disruptions.
Building trustworthy, reliable software is becoming
harder and harder to achieve, while new business and
cybersecurity challenges make it of escalating critical
importance},
doi = {10.1098/rsta.2015.0408},
pdf = {http://rsta.royalsocietypublishing.org/content/375/2104/20150408.full.pdf},
publisher = {The Royal Society}
}
@inproceedings{DongolJRA2018,
author = {Brijesh Dongol and
Radha Jagadeesan and
James Riely and
Alasdair Armstrong},
title = {On abstraction and compositionality for weak-memory linearisability},
booktitle = {\textbf{{VMCAI} 2018}: Verification, Model Checking, and Abstract Interpretation - 19th International
Conference},
abstract = {Linearisability is the de facto standard correctness
condition for concurrent objects. Classical
linearisability assumes that the effect of a method
is captured entirely by the allowed sequences of
calls and returns. This assumption is inadequate in
the presence of relaxed memory models, where
happens-before relations are also of importance. In
this paper, we develop hb-linearisability for
relaxed memory models by extending the classical
notion with happens-before information. We con-
sider two variants: Real time hb-linearisability,
which adopts the classical view that time runs on a
single global clock, and causal hb-linearisability,
which eschews real-time and is appropriate for
systems without a global clock. For both variants,
we prove abstraction (so that programmers can reason
about a client program using the sequential speci
cation of an object rather than its more complex
concurrent implementation) and composition (so that
reasoning about independent objects can be conducted
in isolation).},
conf = {VMCAI 2018},
pages = {183--204},
month = jan,
year = {2018},
editor = {Isil Dillig and
Jens Palsberg},
series = {LNCS},
publisher = {Springer},
url = {https://doi.org/10.1007/978-3-319-73721-8_9},
doi = {10.1007/978-3-319-73721-8_9}
}
@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 = {\textbf{J. ACM}},
opthowpublished = {},
month = dec,
year = 2018,
issue_date = {December 2018},
volume = {66},
number = {1},
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},
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.
}
}
@article{Dinsdale-Young2018perspective,
author = {Dinsdale-Young, Thomas and {da Rocha Pinto}, Pedro and Gardner, Philippa},
title = {A Perspective on Specifying and Verifying Concurrent Modules},
journal = {\textbf{Journal of Logical and Algebraic Methods in Programming}},
year = {2018},
volume = {98},
pages = {1--25},
month = aug,
issn = {2352-2208},
abstract = {The specification of a concurrent program module, and the verification of implementations and clients with respect to such a specification, are difficult problems. A specification should be general enough that any reasonable implementation satisfies it, yet precise enough that it can be used by any reasonable client. We survey a range of techniques for specifying concurrent modules, using the example of a counter module to illustrate the benefits and limitations of each. In particular, we highlight four key concepts underpinning these techniques: auxiliary state, interference abstraction, resource ownership and atomicity. We demonstrate how these concepts can be combined to achieve two powerful approaches for specifying concurrent modules and verifying implementations and clients, which remove the limitations highlighted by the counter example.},
doi = {10.1016/j.jlamp.2018.03.003},
keywords = {Concurrency, Specification, Program verification},
url = {http://www.sciencedirect.com/science/article/pii/S2352220817300871},
pdf = {http://psvg.doc.ic.ac.uk/publications/Dinsdale-Young2018perspective.pdf}
}
@inproceedings{Ntzik2018Concurrent,
author = {Ntzik, Gian and {da Rocha Pinto}, Pedro and Sutherland, Julian and Gardner, Philippa},
title = {A Concurrent Specification of {POSIX} File Systems },
booktitle = {\textbf{ECOOP 2018}: 32nd European Conference on Object-Oriented Programming},
optbooktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018).},
conf = {ECOOP 2018},
year = {2018},
month = jul,
abstract = {POSIX is a standard for operating systems, with a substantial part devoted to specifying
file-system operations. File-system operations exhibit complex concurrent behaviour, comprising
multiple actions affecting different parts of the state: typically, multiple atomic reads followed by
an atomic update. However, the standard’s description of concurrent behaviour is unsatisfactory:
it is fragmented; contains ambiguities; and is generally under-specified. We provide a formal
concurrent specification of POSIX file systems and demonstrate scalable reasoning for clients.
Our specification is based on a concurrent specification language, which uses a modern concurrent
separation logic for reasoning about abstract atomic operations, and an associated refinement
calculus. Our reasoning about clients highlights an important difference between reasoning about
modules built over a heap, where the interference on the shared state is restricted to the operations
of the module, and modules built over a file system, where the interference cannot be restricted
as the file system is a public namespace. We introduce specifications conditional on context
invariants used to restrict the interference, and apply our reasoning to the example of lock files.},
doi = {10.4230/LIPIcs.ECOOP.2018.4},
pdf = {http://psvg.doc.ic.ac.uk/publications/Ntzik2018Concurrent.pdf}
}
@inproceedings{DBLP:conf/ppdp/SantosMGDG18,
author = {Jos{\'{e}} Fragoso Santos and
Petar Maksimovic and
Th{\'{e}}otime Grohens and
Julian Dolby and
Philippa Gardner},
title = {Symbolic Execution for {JavaScript}},
booktitle = {\textbf{PPDP 2018}: Proceedings of the 20th International Symposium on Principles and
Practice of Declarative Programming},
conf = {PPDP 2018},
pages = {11:1--11:14},
year = {2018},
month = sep,
optcrossref = {DBLP:conf/ppdp/2018},
url = {http://doi.acm.org/10.1145/3236950.3236956},
doi = {10.1145/3236950.3236956},
timestamp = {Tue, 14 Aug 2018 20:44:23 +0200},
biburl = {https://dblp.org/rec/bib/conf/ppdp/SantosMGDG18},
bibsource = {dblp computer science bibliography, https://dblp.org},
abstract = {We present a framework for trustworthy symbolic execution of JavaScripts programs, whose aim is to assist developers in the testing of their code: the developer writes symbolic tests for which the framework provides concrete counter-models. We create the framework following a new, general methodology for designing compositional program analyses for dynamic languages. We prove that the underlying symbolic execution is sound and does not generate false positives. We establish additional trust by using the theory to precisely guide the implementation and by thorough testing. We apply our framework to whole-program symbolic testing of real-world JavaScript libraries and compositional debugging of separation logic specifications of JavaScript programs.},
pdf = {}
}
This file was generated by bibtex2html 1.99.