# topic.Cerberus.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c topic:"Cerberus" -ob topic.Cerberus.bib sewellbib2.bib}}

@inproceedings{Cerberus-PLDI16,
author = {
Kayvan Memarian and
Justus Matthiesen and
James Lingard and
Kyndylan Nienhuis and
David Chisnall and
Robert N.M. Watson and
Peter Sewell
},
title = {Into the depths of {C}: elaborating the de facto standards},
abstract = {
C remains central to our computing infrastructure.  It is notionally defined by ISO standards, but in reality the properties of C assumed by systems code and those implemented by compilers have diverged, both from the ISO standards and from each other, and none of these are clearly understood.

We make two contributions to help improve this error-prone situation.  First, we describe an in-depth analysis of the design space for the semantics of pointers and memory in C as it is used in practice.  We articulate many specific questions, build a suite of semantic test cases, gather experimental data from multiple implementations, and survey what C experts believe about the de facto standards.  We identify questions where there is a consensus (either following ISO or differing) and where there are conflicts. We apply all this to an experimental C implemented above capability hardware.  Second, we describe a formal model, Cerberus, for large parts of C.  Cerberus is parameterised on its memory model; it is linkable either with a candidate de facto memory object model, under construction, or with an operational C11 concurrency model; it is defined by elaboration to a much simpler Core language for accessibility, and it is executable as a test oracle on small examples.

This should provide a solid basis for discussion of what mainstream C is now: what programmers and analysis tools can assume and what compilers aim to implement. Ultimately we hope it will be a step towards clear, consistent, and accepted semantics for the various use-cases of C.
},
optcrossref = {},
optkey = {},
conf = {PLDI 2016},
booktitle = {Proceedings of the 37th ACM SIGPLAN conference on Programming Language Design and Implementation},
optpages = {},
year = {2016},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
month = jun,
optorganization = {},
optpublisher = {},
note = {PLDI 2016 Distinguished Paper award},
project = {http://www.cl.cam.ac.uk/~pes20/cerberus},
url = {http://doi.acm.org/10.1145/2908080.2908081},
doi = {10.1145/2908080.2908081},
pdf = {http://www.cl.cam.ac.uk/users/pes20/cerberus/pldi16.pdf},
optannote = {},
topic = {Cerberus},
topictwo = {cheri},
topicthree = {WG14},
cheriformal = {true},
recent = {false}
}

@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 = {Proceedings of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages},
optbooktitle = {},
year = {2019},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optorganization = {},
optpublisher = {},
note = {Proc. ACM Program. Lang. 3, POPL, Article 67. Also available as ISO/IEC JTC1/SC22/WG14 N2311 },
optannote = {},
doi = {10.1145/3290380},
apollourl = {https://www.repository.cam.ac.uk/handle/1810/288833},
pdf = {http://www.cl.cam.ac.uk/users/pes20/cerberus/cerberus-popl2019.pdf},
supplementarymaterial = {http://www.cl.cam.ac.uk/users/pes20/cerberus/supplementary-material-popl2019},
topic = {Cerberus},
topictwo = {cheri},
topicthree = {WG14},
cheriformal = {true},
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.
},
elver = {true},
optrecent = {true}
}

@inproceedings{cerberusBMC,
author = {Stella Lau and Victor B. F. Gomes and Kayvan Memarian and Jean Pichon-Pharabod and Peter Sewell},
title = {{Cerberus-BMC}: a Principled Reference Semantics and Exploration
Tool for Concurrent and Sequential {C}},
optcrossref = {},
optkey = {},
conf = {CAV 2019},
booktitle = {Proc. 31st International Conference on Computer-Aided Verification},
optpages = {},
year = {2019},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
month = jul,
optorganization = {},
optpublisher = {},
optnote = {},
doi = {10.1007/978-3-030-25540-4_22},
optannote = {},
apollourl = {https://www.repository.cam.ac.uk/handle/1810/293121},
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.
},
optrecent = {true},
elver = {true}
}

@inproceedings{2022-popl-vip,
author = {Rodolphe Lepigre and Michael Sammler and Kayvan Memarian and Robbert Krebbers and Derek Dreyer and Peter Sewell},
title = {{VIP}: Verifying Real-World {C} Idioms with Integer-Pointer Casts},
optcrossref = {},
optkey = {},
conf = {POPL 2022},
booktitle = {Proceedings of the 49th ACM SIGPLAN Symposium on Principles of Programming Languages},
optbooktitle = {},
year = {2022},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optorganization = {},
optpublisher = {},
note = {Proc. ACM Program. Lang. 6, POPL, Article 20},
optnote = {},
optannote = {},
doi = {10.1145/3498681},
abstract = {Systems code often requires fine-grained control over memory layout and pointers, expressed using  low-level (e.g.~bitwise) operations on pointer values.
Since these operations go beyond what basic pointer arithmetic in C allows, they are performed with the help of \emph{integer-pointer casts}.
Prior work has explored increasingly realistic memory object models for C that account for the desired semantics of integer-pointer casts while also being sound w.r.t.\ compiler optimisations, culminating in PNVI, the preferred memory object model in ongoing discussions within the ISO WG14 C standards committee.
However, its complexity makes it an unappealing target for verification, and no tools currently exist to verify C programs under PNVI.

In this paper, we introduce VIP, a new memory object model aimed at supporting C verification.
VIP sidesteps the complexities of PNVI with a simple but  effective idea: a new construct that lets programmers express the intended provenances of integer-pointer casts explicitly.
At the same time, we prove VIP compatible with PNVI, thus enabling verification on top of VIP to benefit from PNVI's validation with respect to practice.
In particular, we build a verification tool, RefinedC-VIP, for verifying programs under VIP semantics.
As the name suggests, RefinedC-VIP extends the recently developed RefinedC tool, which is automated yet also produces foundational proofs in Coq.
We evaluate RefinedC-VIP on a range of systems-code idioms, and validate VIP's expressiveness via an implementation in the Cerberus C semantics.},
optapollourl = {https://www.repository.cam.ac.uk/handle/1810/288588},
pdf = {http://www.cl.cam.ac.uk/users/pes20/2022-popl-vip.pdf},
supplementarymaterial = {https://doi.org/10.5281/zenodo.5662349},
topic = {Cerberus},
project = {https://gitlab.mpi-sws.org/iris/refinedc},
elver = {true},
recent = {true}
}

@inproceedings{2023-popl-cn,
author = {Christopher Pulte and Dhruv C. Makwana and Thomas Sewell and Kayvan Memarian and Peter Sewell and Neel Krishnaswami},
title = {CN: Verifying systems {C} code with separation-logic refinement types},
optcrossref = {},
optkey = {},
conf = {POPL 2023},
booktitle = {Proceedings of the 50th ACM SIGPLAN Symposium on Principles of Programming Languages},
optbooktitle = {},
year = {2023},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jan,
optorganization = {},
optpublisher = {},
optnote = {Conditionally accepted},
optnote = {Proc. ACM Program. Lang. 7, POPL, Article 1},
optnote = {},
optannote = {},
doi = {10.1145/3571194},
abstract = {Despite significant progress in the verification of hypervisors, operating systems, and compilers, and in verification tooling, there exists a wide gap between the approaches used in verification projects and conventional development of systems software. We see two main challenges in bringing these closer together: verification handling the complexity of code and semantics of conventional systems software, and verification usability.

We describe an experiment in verification tool design aimed at addressing some aspects of both: we design and implement CN, a separation-logic refinement type system for C systems software, aimed at predictable proof automation, based on a realistic semantics of ISO C. CN reduces refinement typing to decidable propositional logic reasoning, uses first-class resources to support pointer aliasing and pointer arithmetic, features resource inference for iterated separating conjunction, and uses a novel syntactic restriction of ghost variables in specifications to guarantee their successful inference. We implement CN and formalise key aspects of the type system, including a soundness proof of type checking. To demonstrate the usability of CN we use it to verify a substantial component of Google's pKVM hypervisor for Android.
},
optapollourl = {https://www.repository.cam.ac.uk/handle/1810/288588},
pdf = {http://www.cl.cam.ac.uk/users/pes20/cn-draft.pdf},
optsupplementarymaterial = {https://doi.org/10.5281/zenodo.5662349},
topic = {Cerberus},
project = {https://www.cl.cam.ac.uk/~cp526/popl23.html},
elver = {true},
recent = {true}
}