topic.ISA_semantics.bib
@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c 'topic:"ISA_semantics" or topictwo:"ISA_semantics"' -ob topic.ISA_semantics.bib sewellbib2.bib}}
@inproceedings{DBLP:conf/micro/GrayKMPSS15,
author = {Kathryn E. Gray and
Gabriel Kerneis and
Dominic P. Mulligan and
Christopher Pulte and
Susmit Sarkar and
Peter Sewell},
title = {An integrated concurrency and core-{ISA} architectural envelope definition,
and test oracle, for {IBM} {POWER} multiprocessors},
abstract = {Weakly consistent multiprocessors such as ARM and IBM POWER have been with us for decades, but their subtle programmer-visible concurrency behaviour remains challenging, both to implement and to use; the traditional architecture documentation, with its mix of prose and pseudocode, leaves much unclear.
In this paper we show how a precise architectural envelope model for such architectures can be defined, taking IBM POWER as our example. Our model specifies, for an arbitrary test program, the set of all its allowable executions, not just those of some particular implementation. The model integrates an operational concurrency model with an ISA model for the fixed-point non-vector user-mode instruction set (largely automatically derived from the vendor pseudocode, and expressed in a new ISA description language). The key question is the interface between these two: allowing all the required concurrency behaviour, without overcommitting to some particular microarchitectural implementation, requires a novel abstract structure.
Our model is expressed in a mathematically rigorous language that can be automatically translated to an executable test-oracle tool; this lets one either interactively explore or exhaustively compute the set of all allowed behaviours of intricate test cases, to provide a reference for hardware and software development.
},
conf = {MICRO 2015},
booktitle = {Proceedings of the 48th International Symposium on Microarchitecture (Waikiki)},
pages = {635--646},
year = {2015},
month = dec,
optcrossref = {DBLP:conf/micro/2015},
opturl = {http://doi.acm.org/10.1145/2830772.2830775},
pdf = {http://www.cl.cam.ac.uk/~pes20/micro-48-2015.pdf},
doi = {10.1145/2830772.2830775},
timestamp = {Sun, 10 Jan 2016 12:42:56 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/micro/GrayKMPSS15},
bibsource = {dblp computer science bibliography, http://dblp.org},
topic = {Power_and_ARM},
topictwo = {ISA_semantics}
}
@inproceedings{DBLP:conf/popl/FlurGPSSMDS16,
author = {Shaked Flur and
Kathryn E. Gray and
Christopher Pulte and
Susmit Sarkar and
Ali Sezgin and
Luc Maranget and
Will Deacon and
Peter Sewell},
title = {Modelling the {ARMv8} architecture, operationally: concurrency and {ISA}},
abstract = {In this paper we develop semantics for key aspects of the ARMv8 multiprocessor architecture: the concurrency model and much of the 64-bit application-level instruction set (ISA). Our goal is to clarify what the range of architecturally allowable behaviour is, and thereby to support future work on formal verification, analysis, and testing of concurrent ARM software and hardware.
Establishing such models with high confidence is intrinsically difficult: it involves capturing the vendor's architectural intent, aspects of which (especially for concurrency) have not previously been precisely defined. We therefore first develop a concurrency model with a microarchitectural flavour, abstracting from many hardware implementation concerns but still close to hardware-designer intuition. This means it can be discussed in detail with ARM architects. We then develop a more abstract model, better suited for use as an architectural specification, which we prove sound w.r.t.~the first.
The instruction semantics involves further difficulties, handling the mass of detail and the subtle intensional information required to interface to the concurrency model. We have a novel ISA description language, with a lightweight dependent type system, letting us do both with a rather direct representation of the ARM reference manual instruction descriptions.
We build a tool from the combined semantics that lets one explore, either interactively or exhaustively, the full range of architecturally allowed behaviour, for litmus tests and (small) ELF executables. We prove correctness of some optimisations needed for tool performance.
We validate the models by discussion with ARM staff, and by comparison against ARM hardware behaviour, for ISA single- instruction tests and concurrent litmus tests.},
conf = {POPL 2016},
booktitle = {Proceedings of the 43rd {ACM} {SIGPLAN-SIGACT} Symposium on
Principles of Programming Languages (St. Petersburg,
FL, USA)},
pages = {608--621},
year = {2016},
month = jan,
optcrossref = {DBLP:conf/popl/2016},
opturl = {http://doi.acm.org/10.1145/2837614.2837615},
pdf = {http://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf},
project = {http://www.cl.cam.ac.uk/~sf502/popl16/index.html},
optproject = {http://www.cl.cam.ac.uk/~pes20/popl16-armv8/},
doi = {10.1145/2837614.2837615},
timestamp = {Fri, 08 Jan 2016 18:18:25 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/FlurGPSSMDS16},
bibsource = {dblp computer science bibliography, http://dblp.org},
topic = {Power_and_ARM},
topictwo = {ISA_semantics}
}
@inproceedings{mixed17,
author = {Shaked Flur and Susmit Sarkar and Christopher Pulte and Kyndylan Nienhuis and Luc Maranget and Kathryn E. Gray and Ali Sezgin and Mark Batty and Peter Sewell},
title = {Mixed-size Concurrency: {ARM}, {POWER}, {C/C++11}, and {SC}},
conf = {POPL 2017},
booktitle = {Proceedings of the 44th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
Programming Languages (Paris)},
year = {2017},
month = jan,
pages = {429--442},
numpages = {14},
opturl = {http://doi.acm.org/10.1145/3009837.3009839},
doi = {10.1145/3009837.3009839},
project = {http://www.cl.cam.ac.uk/users/pes20/popl17/},
abstract = {Previous work on the semantics of relaxed shared-memory concurrency has only considered the case in which each load reads the data of exactly one store. In practice, however, multiprocessors support mixed-size accesses, and these are used by systems software and (to some degree) exposed at the C/C++ language level. A semantic foundation for software, therefore, has to address them.
We investigate the mixed-size behaviour of ARMv8 and IBM POWER architectures and implementations: by experiment, by developing semantic models, by testing the correspondence between these, and by discussion with ARM and IBM staff. This turns out to be surprisingly subtle, and on the way we have to revisit the fundamental concepts of coherence and sequential consistency, which change in this setting. In particular, we show that adding a memory barrier between each instruction does not restore sequential consistency. We go on to extend the C/C++11 model to support non-atomic mixed-size memory accesses.
This is a necessary step towards semantics for real-world shared-memory concurrent code, beyond litmus tests.
},
pdf = {http://www.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf},
topic = {Power_and_ARM},
topictwo = {ISA_semantics},
recent = {false}
}
@inproceedings{armv8-mca,
author = {Christopher Pulte and Shaked Flur and Will Deacon and Jon French and Susmit Sarkar and Peter Sewell},
title = {{Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8}},
optcrossref = {},
optkey = {},
conf = {POPL 2018},
booktitle = {Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages},
optpages = {},
year = {2018},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
doi = {10.1145/3158107},
month = jan,
optorganization = {},
optpublisher = {},
optnote = {Draft},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/armv8-mca/armv8-mca-draft.pdf},
project = {http://www.cl.cam.ac.uk/~pes20/armv8-mca/},
errata = {https://www.cl.cam.ac.uk/~pes20/armv8-mca/errata.html},
abstract = {ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8. Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified by the potential benefits. In particular, the model was originally \emph{non-multicopy-atomic}: writes could become visible to some other threads before becoming visible to all --- but this has not been exploited in production implementations, the corresponding potential hardware optimisations are thought to have insufficient benefits in the ARM context, and it gives rise to subtle complications when combined with other ARMv8 features. The ARMv8 architecture has therefore been revised: it now has a multicopy-atomic model. It has also been simplified in other respects, including more straightforward notions of dependency, and the architecture now includes a formal concurrency model.
In this paper we detail these changes and discuss their motivation. We define two formal concurrency models: an operational one, simplifying the Flowing model of Flur et al., and the axiomatic model of the revised ARMv8 specification. The models were developed by an academic group and by ARM staff, respectively, and this extended collaboration partly motivated the above changes. We prove the equivalence of the two models. The operational model is integrated into an executable exploration tool with new web interface, demonstrated by exhaustively checking the possible behaviours of a loop-unrolled version of a Linux kernel lock implementation, a previously known bug due to unprevented speculation, and a fixed version.},
topic = {Power_and_ARM},
topictwo = {ISA_semantics},
optrecent = {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 = {Proceedings of the 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.
},
apollourl = {https://www.repository.cam.ac.uk/handle/1810/288588},
pdf = {http://www.cl.cam.ac.uk/users/pes20/sail/sail-popl2019.pdf},
supplementarymaterial = {http://www.cl.cam.ac.uk/users/pes20/sail/popl2019.html},
topic = {ISA_semantics},
topictwo = {cheri},
cheriformal = {true},
project = {http://www.cl.cam.ac.uk/~pes20/sail/},
elver = {true},
optrecent = {true}
}
@inproceedings{sail-arw18,
author = { Alasdair Armstrong and
Thomas Bauereiss and
Brian Campbell and
Shaked Flur and
Kathryn E. Gray and
Prashanth Mundkur and
Robert M.~Norton and
Christopher Pulte and
Alastair Reid and
Peter Sewell and
Ian Stark and
Mark Wassell},
title = {Detailed Models of Instruction Set Architectures: From
Pseudocode to Formal Semantics},
optcrossref = {},
optkey = {},
conf = {Automated Reasoning Workshop (ARW) 2018},
booktitle = {Proc. Automated Reasoning Workshop},
year = {2018},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
pages = {23--24},
month = apr,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {Two-page abstract},
optnote = {Proceedings available at \url{https://www.cl.cam.ac.uk/events/arw2018/arw2018-proc.pdf}},
optannote = {},
project = {http://www.cl.cam.ac.uk/~pes20/sail/},
pdf = {http://www.cl.cam.ac.uk/~pes20/sail/2018-04-12-arw-paper.pdf},
abstract = {Processor instruction set architectures (ISAs) are typically specified using a mixture of prose and
pseudocode. We present ongoing work on expressing such specifications rigorously and automatically trans-
lating them to interactive theorem prover definitions, making them amenable to mechanised proof. Our ISA
descriptions are written in Sail—a custom ISA specification language designed to support idioms from var-
ious processor vendor’s pseudocode, with lightweight dependent typing for bitvectors, targeting a variety of
use cases including sequential and concurrent ISA semantics. From Sail we aim to portably generate usable
theorem prover definitions for multiple provers, including Isabelle, HOL4, and Coq. We are focusing on the
full ARMv8.3-A specification, CHERI-MIPS, and RISC-V, together with fragments of IBM POWER and x86.},
topic = {ISA_semantics},
topic2 = {cheri},
cheriformal = {true}
}
@inproceedings{sail-arw18-minisail,
author = {Alasdair Armstrong and Neel Krishnaswami and Peter Sewell and Mark Wassell},
title = {Formalisation of {MiniSail} in the {Isabelle} Theorem Prover},
optcrossref = {},
optkey = {},
conf = {Automated Reasoning Workshop (ARW) 2018},
booktitle = {Proc. Automated Reasoning Workshop},
year = {2018},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
pages = {27--28},
month = apr,
optaddress = {},
optorganization = {},
optpublisher = {},
note = {Two-page abstract},
optnote = {Proceedings available at \url{https://www.cl.cam.ac.uk/events/arw2018/arw2018-proc.pdf}},
optannote = {},
topic = {ISA_semantics},
project = {http://www.cl.cam.ac.uk/~pes20/sail/},
pdf = {http://www.cl.cam.ac.uk/~pes20/sail/arw18_mpew2.pdf},
abstract = {Sail is a language used to model instruction set architectures. It has an imperative syntax and a
dependent type system. We formalise a core calculus of the language in the Isabelle theorem prover describing
the language syntax, substitution, the type system and operational semantics. A number of classic theorems
such as preservation and progress are then proved. The purpose of this formalisation is to ensure that the full
language is built on sound foundations and to provide a platform for the generation of the implementation of
a type checker and evaluator for the language.}
}
@inproceedings{isla-cav,
optkey = {},
author = {Alasdair Armstrong and Brian Campbell and Ben Simner and Christopher Pulte and Peter Sewell},
title = {Isla: Integrating full-scale {ISA} semantics and axiomatic concurrency models},
conf = {CAV 2021},
booktitle = {Proc. 33rd International Conference on Computer-Aided Verification},
month = jul,
year = {2021},
opteditor = {Alexandra Silva and K. Rustan M. Leino},
opttitle = {Isla: Integrating Full-Scale {ISA} Semantics and Axiomatic Concurrency
Models},
optbooktitle = {Computer Aided Verification - 33rd International Conference, {CAV}
2021, Virtual Event, July 20-23, 2021, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {12759},
pages = {303--316},
publisher = {Springer},
optyear = {2021},
url = {https://doi.org/10.1007/978-3-030-81685-8\_14},
doi = {10.1007/978-3-030-81685-8\_14},
timestamp = {Fri, 23 Jul 2021 16:41:31 +0200},
biburl = {https://dblp.org/rec/conf/cav/ArmstrongCSPS21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
optpdf = {https://www.cl.cam.ac.uk/~pes20/isla/isla-cav2021.pdf},
optnote = {Extended version available at \url{https://www.cl.cam.ac.uk/~pes20/isla/isla-cav2021-extended.pdf}},
pdf = {https://www.cl.cam.ac.uk/~pes20/isla/isla-cav2021-extended.pdf},
elver = {true},
abstract = {
Architecture specifications such as Armv8-A and RISC-V are the ultimate foundation for software verification and the correctness criteria for hardware verification. They should define the allowed sequential and relaxed-memory concurrency behaviour of programs, but hitherto there has been no integration of full-scale instruction-set architecture (ISA) semantics with axiomatic concurrency models, either in mathematics or in tools. These ISA semantics can be surprisingly large and intricate, e.g.~100k+ lines for Armv8-A.
In this paper we present a tool, Isla, for computing the allowed behaviours of concurrent litmus tests with respect to full-scale ISA definitions, in Sail, and arbitrary axiomatic relaxed-memory concurrency models, in the Cat language. It is based on a generic symbolic engine for Sail ISA specifications, which should be valuable also for other verification tasks. We equip the tool with a web interface to make it widely accessible, and illustrate and evaluate it for Armv8-A and RISC-V.
By using full-scale and authoritative ISA semantics, this lets one evaluate litmus tests using arbitrary user instructions with high confidence. Moreover, because these ISA specifications give detailed and validated definitions of the sequential aspects of \emph{systems} functionality, as used by hypervisors and operating systems, e.g.~instruction fetch, exceptions, and address translation, our tool provides a basis for developing concurrency semantics for these. We demonstrate this for the Armv8-A instruction-fetch model and self-modifying code examples of Simner et al.
},
optannote = {},
topic = {Power_and_ARM},
topictwo = {ISA_semantics},
recent = {true}
}
@article{isla-cav-fmsd,
optkey = {},
author = {Alasdair Armstrong and Brian Campbell and Ben Simner and Christopher Pulte and Peter Sewell},
title = {Isla: Integrating full-scale {ISA} semantics and axiomatic concurrency models (extended version)},
journal = {Formal Methods in System Design},
month = may,
year = {2023},
optpages = {303--316},
publisher = {Springer},
optissn = {1572-8102},
optyear = {2021},
url = {https://doi.org/10.1007/s10703-023-00409-y},
doi = {10.1007/s10703-023-00409-y},
pdf = {https://link.springer.com/content/pdf/10.1007/s10703-023-00409-y.pdf},
elver = {true},
abstract = {
Architecture specifications such as Armv8-A and RISC-V are the ultimate foundation for software verification and the correctness criteria for hardware verification. They should define the allowed sequential and relaxed-memory concurrency behaviour of programs, but hitherto there has been no integration of full-scale instruction-set architecture (ISA) semantics with axiomatic concurrency models, either in mathematics or in tools. These ISA semantics can be surprisingly large and intricate, e.g. 100k+ lines for Armv8-A. In this paper we present a tool, Isla, for computing the allowed behaviours of concurrent litmus tests with respect to full-scale ISA definitions, in the Sail language, and arbitrary axiomatic relaxed-memory concurrency models, in the Cat language. It is based on a generic symbolic engine for Sail ISA specifications. We equip the tool with a web interface to make it widely accessible, and illustrate and evaluate it for Armv8-A and RISC-V. The symbolic execution engine is valuable also for other verification tasks: it has been used in automated ISA test generation for the Arm Morello prototype architecture, extending Armv8-A with CHERI capabilities, and for Iris program-logic reasoning about binary code above the Armv8-A and RISC-V ISA specifications. By using full-scale and authoritative ISA semantics, Isla lets one evaluate litmus tests using arbitrary user instructions with high confidence. Moreover, because these ISA specifications give detailed and validated definitions of the sequential aspects of systems functionality, as used by hypervisors and operating systems, e.g. instruction fetch, exceptions, and address translation, our tool provides a basis for developing concurrency semantics for these. We demonstrate this for the Armv8-A instruction-fetch and virtual-memory models and examples of Simner et al.
},
optannote = {},
topic = {Power_and_ARM},
topictwo = {ISA_semantics},
recent = {true}
}
@misc{acs-2020,
optkey = {},
author = {Peter Sewell and Christopher Pulte and Shaked Flur and Mark Batty and Luc Maranget and Alasdair Armstrong},
title = {Multicore Semantics: Making Sense of Relaxed Memory (MPhil slides)},
opthowpublished = {},
month = oct,
year = 2022,
optnote = {\url{https://www.cl.cam.ac.uk/~pes20/slides-acs-2022.pdf}},
url = {https://www.cl.cam.ac.uk/~pes20/slides-acs-2022.pdf},
optannote = {},
recent = {true},
topic = {Power_and_ARM},
topictwo = {ISA_semantics}
}
@inproceedings{morello-proofs-esop2022,
author = {Bauereiss, Thomas and Campbell, Brian and Sewell, Thomas
and Armstrong, Alasdair and Esswood, Lawrence and Stark,
Ian and Barnes, Graeme and Watson, Robert N. M. and Sewell,
Peter},
title = {Verified Security for the {Morello} Capability-enhanced
Prototype {Arm} Architecture},
optcrossref = {},
optkey = {},
conf = {ESOP 2022},
booktitle = {Proceedings of the 31st European Symposium on Programming},
year = {2022},
optbooktitle = {},
optyear = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = apr,
optaddress = {},
optorganization = {},
optpublisher = {},
opteditor = {Ilya Sergey},
opttitle = {Verified Security for the Morello Capability-enhanced Prototype Arm
Architecture},
optbooktitle = {Programming Languages and Systems - 31st European Symposium on Programming,
{ESOP} 2022, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2022, Munich, Germany, April 2-7,
2022, Proceedings},
optseries = {Lecture Notes in Computer Science},
optvolume = {13240},
pages = {174--203},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-030-99336-8\_7},
doi = {10.1007/978-3-030-99336-8\_7},
timestamp = {Fri, 01 Apr 2022 15:49:28 +0200},
biburl = {https://dblp.org/rec/conf/esop/BauereissCSAESB22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
optnote = {},
optannote = {},
abstract = {Memory safety bugs continue to be a major source of security vulnerabilities in our critical infrastructure. The CHERI project has proposed extending conventional architectures with hardware-supported \emph{capabilities} to enable fine-grained memory protection and scalable compartmentalisation, allowing historically memory-unsafe C and C++ to be adapted to deterministically mitigate large classes of vulnerabilities, while requiring only minor changes to existing system software sources. Arm is currently designing and building Morello, a CHERI-enabled prototype architecture, processor, SoC, and board, extending the high-per\-for\-mance Neoverse N1, to enable industrial evaluation of CHERI and pave the way for potential mass-market adoption. However, for such a major new security-oriented architecture feature, it is important to establish high confidence that it does provide the intended protections, and that cannot be done with conventional engineering techniques.
In this paper we put the Morello architecture on a solid mathematical footing from the outset. We define the fundamental security property that Morello aims to provide, reachable capability monotonicity, and prove that the architecture definition satisfies it. This proof is mechanised in Isabelle/HOL, and applies to a translation of the official Arm specification of the Morello instruction-set architecture (ISA) into Isabelle. The main challenge is handling the complexity and scale of a production architecture: 62,000 lines of specification, translated to 210,000 lines of Isabelle. We do so by factoring the proof via a narrow abstraction capturing essential properties of arbitrary CHERI ISAs, expressed above a monadic intra-instruction semantics. We also develop a model-based test generator, which generates instruction-sequence tests that give good specification coverage, used in early testing of the Morello implementation and in Morello QEMU development, and we use Arm's internal test suite to validate our model.
This gives us machine-checked mathematical proofs of whole-ISA security properties of a full-scale industry architecture, at design-time. To the best of our knowledge, this is the first demonstration that that is feasible, and it significantly increases confidence in Morello.
},
pdf = {http://www.cl.cam.ac.uk/~pes20/morello-proofs-esop2022.pdf},
project = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/},
topic = {cheri},
topictwo = {ISA_semantics},
cheriformal = {true},
elver = {true},
recent = {true}
}
@inproceedings{2022-pldi-islaris,
author = {Michael Sammler and Angus Hammond and Rodolphe Lepigre and Brian Campbell and Jean Pichon-Pharabod and Derek Dreyer and Deepak Garg and Peter Sewell},
title = {{Islaris}: Verification of Machine Code Against Authoritative {ISA} Semantics},
optcrossref = {},
optkey = {},
doi = {10.1145/3519939.3523434},
year = {2022},
isbn = {978-1-4503-9265-5/22/06},
conf = {PLDI 2022},
booktitle = {Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
optbooktitle = {San Diego, CA, USA},
optyear = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
month = jun,
optaddress = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
abstract = {
Recent years have seen great advances towards verifying large-scale systems code. However, these verifications are usually based on hand-written assembly or machine-code semantics for the underlying architecture that only cover a small part of the instruction set architecture (ISA). In contrast, other recent work has used Sail to establish formal models for large real-world architectures, including Armv8-A and RISC-V, that are comprehensive (complete enough to boot an operating system or hypervisor) and authoritative (automatically derived from the Arm internal model and validated against the Arm validation suite, and adopted as the official formal specification by RISC-V International, respectively). But the scale and complexity of these models makes them challenging to use as a basis for verification.
In this paper, we propose Islaris, the first system to support verification of machine code above these complete and authoritative real-world ISA specifications. Islaris uses a novel combination of \emph{SMT-solver-based symbolic execution} (the Isla symbolic executor) and \emph{automated reasoning in a foundational program logic} (a new separation logic we derive using Iris in Coq). We show that this approach can handle Armv8-A and RISC-V machine code exercising a wide range of systems features, including installing and calling exception vectors, code parametric on a relocation address offset (from the production pKVM hypervisor); unaligned access faults; memory-mapped IO; and compiled C code using inline assembly and function pointers.
},
pdf = {http://www.cl.cam.ac.uk/~pes20/2022-pldi-islaris.pdf},
project = {https://github.com/rems-project/islaris},
topic = {ISA_semantics},
recent = {true},
elver = {true}
}