Skip to content

Commit

Permalink
Spelling / typo fixes.
Browse files Browse the repository at this point in the history
  • Loading branch information
ronorton committed Jul 19, 2024
1 parent e767a16 commit 344c945
Show file tree
Hide file tree
Showing 5 changed files with 7 additions and 7 deletions.
6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
# CHERIoT Specification and Sail model

This repository contains the specification for the [CHERIoT](https://cheriot.org) ISA.
It consists of a document written in [latex](/archdoc) which includes exerpts of the [reference model](/src) written in [Sail](http://github.com/rems-project/sail).
It consists of a document written in [latex](/archdoc) which includes excerpts of the [reference model](/src) written in [Sail](http://github.com/rems-project/sail).
The [current draft architecture document](https://microsoft.github.io/cheriot-sail/cheriot-architecture.pdf) built from this repository contains a full description of the ISA and its intended use by [CHERIoT RTOS](https://github.com/microsoft/cheriot-rtos/).
The Sail code is used to build an instruction set simulator which is included in the [CHERIoT RTOS dev containter](https://github.com/microsoft/cheriot-rtos/blob/main/docs/GettingStarted.md).
The Sail code is used to build an instruction set simulator which is included in the [CHERIoT RTOS dev container](https://github.com/microsoft/cheriot-rtos/blob/main/docs/GettingStarted.md).
It can also be used to prove [properties](properties) of the ISA using Sail's SMT support.

The architecture is based on the [CHERI specification](https://github.com/CTSRD-CHERI/cheri-specification).
The code is dervied from [sail-cheri-riscv](http://github.com/CTSRD-CHERI/sail-cheri-riscv) and uses [sail-riscv](http://github.com/rems-project/sail-riscv) as a submodule.
The code is derived from [sail-cheri-riscv](http://github.com/CTSRD-CHERI/sail-cheri-riscv) and uses [sail-riscv](http://github.com/rems-project/sail-riscv) as a submodule.

# Building

Expand Down
2 changes: 1 addition & 1 deletion archdoc/chap-abi.tex
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ \section{Export table layout}

\cref{fig:exporttable} shows the layout of the export table for a compartment.
Each export table starts with a copy of the \PCC{} and \CGP{} for the target compartment.
The next 32-bits is the offset of the compartment's error handler realtive to \PCC{}.\cbase{}, or $-1$ if the compartment does not have an error handler.
The next 32-bits is the offset of the compartment's error handler relative to \PCC{}.\cbase{}, or $-1$ if the compartment does not have an error handler.
If an error occurs the switcher may jump to this as described in \cref{sec:errorhandling}.
After the header, the export table is comprised of one 32-bit entry per exported function.
The first 16 bits of each entry provide the displacement from the start of the compartment's \PCC{} to the entry point.
Expand Down
2 changes: 1 addition & 1 deletion archdoc/chap-changes.tex
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ \chapter{Version history}
\item[\ghissue{14}] When loading a sealed capability through an authority lacking \cappermILG,
the loaded capability will lack \cappermG but will retain \cappermILG if present under seal.
This is more in line with our handling of \cappermLM, which does not modify sealed capabilities.
Software accepting sealed capabilities must be prepared to recieve local (that is, \cappermG-lacking) variants,
Software accepting sealed capabilities must be prepared to receive local (that is, \cappermG-lacking) variants,
even if none were ever explicitly constructed.
\end{description}
\end{description}
Expand Down
2 changes: 1 addition & 1 deletion archdoc/chap-cheri-riscv.tex
Original file line number Diff line number Diff line change
Expand Up @@ -748,6 +748,6 @@ \section{Stack high water mark}
Note that only the address of the store is accounted for, not the width.
This means that it is possible for an unaligned store with an address below \mshwmb{} to write bytes above \mshwmb{} without updating \mshwm{}.
For example, a 4-byte store to \mshwmb{}$ - 1$ would write the bytes at \mshwmb{}$\dots{}$\mshwmb$+ 2$ but leave \mshwm{} unchanged, potentially breaking the RTOS's invariant.
In practice this is not a problem as the RTOS will never issue a capability to untrusted code that crosses the stack base and would therefore premit such a write.%
In practice this is not a problem as the RTOS will never issue a capability to untrusted code that crosses the stack base and would therefore permit such a write.%
\footnote{In fact, no such capabilities should exist after the loader has run and initialised the thread data structures.}
Given this, we choose not to unnecessarily complicate the hardware by requiring it to handle this corner case.
2 changes: 1 addition & 1 deletion archdoc/chap-intro.tex
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ \section{The \cherimcuos{} Model}

A \defn{compartment} is a collection of code, data, and capabilities that serves as an invocable security context.
Compartments statically export \keyword{entry-points}, which may be statically imported by other compartments or passed as opaque \keyword{cross-compartment function pointers}.
A compartment they (statically or dynamically) imports an entry point may then invoke it to perform a \keyword{cross-compartment call}.
A compartment that (statically or dynamically) imports an entry point may then invoke it to perform a \keyword{cross-compartment call}.
Such calls are synchronous and transition the calling thread from one compartment to another.
The thread's stack is used, with appropriate bounds adjustment, in both the caller and callee compartment.

Expand Down

0 comments on commit 344c945

Please sign in to comment.