Giter VIP home page Giter VIP logo

cheriot-sail's Introduction

CHERIoT Sail model

This repository contains an implementation of the CHERIoT ISA in Sail. It contains an executable description of the CHERIoT instruction set that can be used to build an instruction set emulator and also prove properties of the ISA using Sail's SMT support. A full description of the ISA, including extracts from this repository, can be found in the CHERIoT technical report.

The code is dervied from sail-cheri-riscv and uses the sail-riscv model as a submodule.

Building

The easiest way to use this emulator is to use the dev container for the CHERIoT RTOS.

Alternatively, if you wish to build from source you must first install dependencies, including Sail. For example, on Ubuntu 20.04 we have tested:

sudo apt update
sudo apt install opam z3 libgmp-dev
opam init
opam install sail

Then clone the repo:

git clone --recurse-submodules https://github.com/microsoft/cheriot-sail
cd cheriot-sail

Finally build the C emulator:

make csim

This will produce an executable in c_emulator/cheriot_sim that can be used to run ELF files produced by the CHERIoT compiler.

To build the documentation you must have biber, latexmk and pdflatex and have setup your opam environment as above. Then follow the following commands:

pushd archdoc
make
popd

This will create a file located at archdoc/cheriot-architecture.pdf.

Contributing

This project welcomes contributions and suggestions. Most contributions require you to agree to a Contributor License Agreement (CLA) declaring that you have the right to, and actually do, grant us the rights to use your contribution. For details, visit https://cla.opensource.microsoft.com.

When you submit a pull request, a CLA bot will automatically determine whether you need to provide a CLA and decorate the PR appropriately (e.g., status check, comment). Simply follow the instructions provided by the bot. You will only need to do this once across all repos using our CLA.

This project has adopted the Microsoft Open Source Code of Conduct. For more information see the Code of Conduct FAQ or contact [email protected] with any additional questions or comments.

Trademarks

This project may contain trademarks or logos for projects, products, or services. Authorized use of Microsoft trademarks or logos is subject to and must follow Microsoft's Trademark & Brand Guidelines. Use of Microsoft trademarks or logos in modified versions of this project must not cause confusion or imply Microsoft sponsorship. Any use of third-party trademarks or logos are subject to those third-party's policies.

cheriot-sail's People

Contributors

alasdair avatar arichardson avatar bacam avatar bauereiss avatar davidchisnall avatar elliotb-lowrisc avatar gameboo avatar jrtc27 avatar marnovandermaas avatar microsoftopensource avatar nwf avatar nwf-msr avatar peterrugg avatar petersewell avatar pmundkur avatar rmn30 avatar ronorton avatar vmurali avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

cheriot-sail's Issues

v2? Permuted capability encoding optimized for 33-bit busses

Microsoft's CHERIoT-ibex is optimized to be small and so uses a 33-bit memory bus. As a result, capability fetches take two bus cycles (and the two out-of-band bits are ANDed together to form the capability tag, reminiscent of IBM's System/38.)

The current capability layout does not allow for much parallel processing or decompression in the 2nd of those two bus cycles: the cursor/address field is not particularly useful unto itself and the bounds metadata fields are not particularly meaningful without some of the cursor/address bits.

A long while ago (how time flies), Kunyan and I sketched a layout in which we shuffle the bits around a bit, such that the two words shake out containing...

  1. the reserved bit, the 4-bit exponent field, the 9-bit T field, the 9-bit B field, and the middle 9 bits of the address (that is, the ones that overlap the shifted T and B fields in decoding).
  2. the 6-bit permissions, the 3-bit otype, and the residual 23 top and bottom bits of the address (the exponent also serves to divide the 23 bits into top and bottom).

This gives all the information needed for decompression in the first word, so that logic can happen in parallel with the 2nd bus cycle.

The non-contiguousness of the address bits is exciting and strongly differentiates CGetLow from CGetAddr. See https://github.com/CTSRD-CHERI/cheri-specification/wiki/Tracking-discussion-for-CGetAddr-vs-CToPtr-vs-as-integer-alias-vs-CGetLow

Libraries accessing Read/Write data through caps stored within PCC

From my understanding, libraries work as follows: if one compartment calls a library function, it can rest assured that the data it sent the library cannot go outside the caps present in the passed arguments. If a second compartment calls the same library function again, the library function cannot access the old data passed by the first compartment unless the second compartment also passes in the necessary caps. The library relies on not having a read/write cap to global memory to ensure the above.

But, one can have a cap with read/write permissions inside the PCC region of a library that can be loaded by the library. This violates the above invariant, and the library can pass confidential data obtained from the first caller to the second caller. Is this behavior expected? If so, how are library calls not subject to the same sanitization as compartments, via the switcher? What is the expected use case of libraries?

Why is MC implicitly given to caps with EX permission? Is there any use case where you want to read caps from the PCC region? I can understand reading read-only data from the PCC region.

CSRs that can be accessed without `PERMIT_ACCESS_SYSTEM_REGISTERS` should be specific to compartments

If a compartment wants to read, for instance, the global time, it can do so with a sentry that has PERMIT_ACCESS_SYSTEM_REGISTERS permission. That way, if we have a system that has empty import and export lists for each compartment, and disjoint PCC and CGP caps between compartments, the compartments will be trivially isolated from each other. In terms of performance impact, a CSRR instruction will be replaced by a <CJALR; CSRR; CRet> sequence.

For the CSRs that are read/write (fflags, etc), we need to spill those during a context switch in the switcher (https://github.com/microsoft/cheriot-rtos/blob/main/sdk/core/switcher/entry.S)

Cap loads through authorities missing load cap and a transitive perm will result in unexpected bit patterns

Following up on microsoft/cheriot-ibex#13, we think that

if ptw_info.ptw_lc == PTW_LC_CLEAR | not(auth_val.permit_load_store_cap) then {
cr.tag = false;
};
should be before, rather than after,
if cr.tag & not(auth_val.permit_load_global) then {
cr.global = false;
cr.permit_load_global = false;
};
if cr.tag & not(auth_val.permit_load_mutable) & not(isCapSealed(cr)) then {
cr.permit_store = false;
cr.permit_load_mutable = false;
};

As written, loading a capability through an authority lacking capability load permission as well as a transitive load {mutable,global} permission results in the transitive permissions being stripped from the loaded value before the tag is cleared. We think it would be less surprising if the tag were cleared and the permission bits not altered, though the use cases we have in mind (telemetry / crash reporting) are pretty narrow.

CSub redundant?

The CSub instruction is currently functionally identical to the RISC-V's sub instruction. The only reason to keep it is to separate pointer operations from integer ones, which could become important in future ISA versions. For example:

  • capability addresses might be reduced to less than XLEN width, freeing up capability encoding bits for other uses. In this case CSub may or may not be the same as sub.
  • if capability registers were separate from integer ones (split register files).

At the very least we should add some discussion of this to the page in ISA reference.

v2? isentry support

We have considered adding indirect sentries to CHERIoT. At least one rationale is to allow library calls to pick up a data segment beyond .text/PCC. (See additional discussion in #39.)

Transitive load permissions vs. sealed capabilities

A second follow-up to microsoft/cheriot-ibex#13

There's inconsistency between

if cr.tag & not(auth_val.permit_load_global) then {
cr.global = false;
cr.permit_load_global = false;
};
if cr.tag & not(auth_val.permit_load_mutable) & not(isCapSealed(cr)) then {
cr.permit_store = false;
cr.permit_load_mutable = false;
};
in that (missing) transitive load global's effects are applied even to sealed capabilities, while load mutable's are not.

We think that the correct thing to do is actually more nuanced:

  • For unsealed load targets,
    • Missing transitive load mutable should clear both store and transitive load mutable permissions.
    • Missing transitive load global should clear both the global "permission" and the transitive load global permission.
  • For sealed load targets,
    • Missing transitive load mutable should, as now, not impact the permissions under seal (that is, the authority missing this permission will have no effect on the loaded capability).
    • Missing transitive load global should clear the global permission of a sealed capability, but not clear the transitive load global permission under seal.

Allowing delayed check for jump/branch instructions

In the case of branch/jump instructions, would like to have the option to delay the PCC-based branch target checks (address bound/permission) to instruction fetch time (errors associated with the branch target instruction), rather than handling it at EX time (error associated with the branch/jump themselves).

The benefit is better performance (checking logic will not be in the critical instruction feth timing path, for example) and fewer changes to execution logic (espically branch instructions).

Sealing and Unsealing Authorities for addresses rather than otypes

The current sealing and unsealing authorities permit sealing and unsealing of specific otypes. This restricts the number of different data authorities to 7 (otype encoded between 9 to 15). It would be useful to have a address-based sealing/unsealing authority as follows:

  • Compartment A has a sealing and unsealing authority for a range of addresses.
  • Compartment A can pass any cap within that range after sealing it, using the sealing authority for that range, to compartment B
  • When the compartment B calls a function of compartment A by passing the sealed cap, compartment A can unseal the cap using the unsealing authority for that range.

This gives a way to have a lot more "types" for sealing.

Is there any issue in having such a sealing type? Perhaps, one of the 7 data sealing otypes can be allotted for such an address-based sealing so that the hardware can perform the necessary checks. I agree that the SW can use one of the otypes and perform such a check manually, but it would be simpler to do the checks in hardware.

MCAUSE/MTVAL for illegal SCR addresses

When r/w an unimplemented SCR address (e.g., 22), Looks like sail is trapping with MCAUSE = 2 and MTVAL=0. Just want to confirm that's indeed the intention (in the case of PERM_SR violation it returns MCAUSE = 0x1c).

Broken pattern matches on otypes

In src/cheri_cap_common.sail's isCapSentry function and the execute clause for CSeal in src/cheri_insts.sail there are pattern matchs on an otype that uses names for global let bindings in some of the cases. For example,

  match unsigned(cap.otype) {
    otype_sentry => true,
    otype_sentry_id => true,
    otype_sentry_ie => true,
    _  => false
  }

Unfortunately Sail treats these as fresh variable bindings and so it always uses the first clause. (The current development version of Sail now produces "redundant case" warnings for these.)

Changing them to use comparisons should work:

  match unsigned(cap.otype) {
    ty if ty == otype_sentry => true,
    ...

Optimise bounds encoding

There is an opportunity to adopt a trick from CHERI Concentrate to slightly optimise the capability bounds encoding. In CHERI Concentrate the top bit of the length is implied from the exponent in a similar way to the IEEE floating point mantissa. We could adopt the same technique by reducing the T field by one bit to 8-bits and using this freed bit to create a full 5-bit exponent. This would result in some spare exponent values, one of which could be used to encode the denormal case. The resulting encoding would have the same precision and representable bounds as the existing one, but would also support exponents greater than 14, giving better precision for very large allocations.

Local violations should be non-trapping

Violations of permit-store-local should silently clear the tag bit. This changes was made in Ibex, because it makes it possible to have a non-trapping memcpy without needing to inspect every byte. We should update the spec.

Intended use for reserved bit in capabilities

Sorry to raise it as an issue, perhaps this should go into a mailing list - please let me know if you have one.

I was wondering if there's any intended use for the reserved bit in the CherIoT? The main reason I would like to reclaim the space is to have better granularities for bigger bounds, between 2^(9+14) to 2^32. It looks like lack of big buffer support in CherIoT is a reason to avoid it even for applications that don't require 64-bit datatypes except for big buffer references.

ISA Specification bug: Bounds check during taken branches and jumps is either redundant or wrong

It looks like the bounds check uses "minimum-inst-bytes" when checking if a taken address is in-bounds. This means that if the jump/branch target is a 32-bit instruction, where the last 16 bits are out-of-bounds, we will get an out-of-bounds error after fetching the target instruction, which kind of defeats the purpose w.r.t. triaging why the branch or the jump failed; we might as well not do out-of-bounds checks during jumps/taken-branches and wait for the instruction fetch to perform the bounds check.

A potential scenario where this exception (as it is spec-ed currently) becomes useless is as follows:
We have a compressed trampoline initially, allowing us to jump correctly to the trampoline and out of it with just a 2-byte bounds. Now the trampoline is removed and the code is inlined (perhaps some JIT-optimization). When we are debugging/trap handling an out-of-bounds exception because of this, we will still want access to the old PC, so that we can fix the PC bounds there. The way the spec is, we will lose the previous PC information in this scenario, which is not ideal.

Potential fixes:
a) check for 4-bytes in-bounds on taken-branch/jump. This has the problem if the target is a single instruction compressed trampoline with precisely set bounds - we will cause a spurious exception while executing the previous branch/jump.
b) store the previous PC and taken-ness in some micro-architectural state, and if the new instruction's fetch fails check for boundedness, set the EPC with the previous PC if the taken-ness is set. If taken-ness is not set, set EPC to current PC.
c) store the previous PC and taken-ness in some architectural state, and every boundedness failure during instruction fetch stores the previous PC and current PC. This could be easier for writing the trap handlers - the return address for the trap handler is still the current PC, but the fix of the bounds will be done on the previous PC as opposed to (b) where the trap handler has to compute the PC to return to.

Tasks

No tasks being tracked yet.

Extending support for DII execution mode

The following features when in DII mode are needed in order to use the sail model in the design verification flow.

  1. Handling interrupts. If an instruction packet is flagged with an interrupt, the sail model should perform interrupt handling (e.g., update MSTATUS.MIE if interrupt is taken) based on the current MIE status.
  2. Similar to #1, it's also desirable to be able to model a bus error for the load/store and instruction fetch interfaces. Actually - if we can have a generalized way to make the sail model to talk to a volatile peripheral it would be great.
  3. Adding a status-dump pseudo-instruction so that we can dump all architecturally visible registers and use that as a checkpoint against RTL simulation.

v2? cgp as SCR

Right now, CGP is just an ISA name for one of the GPRs reachable by all register selectors. We have contemplated instead converting it to a SCR. That SCR would likely be ambiently readable, via AUICGP as well as the existing SCR access instructions, but would require ASR to modify, restricting modification to the TCB switcher.1 As we already consider library code as running within the calling compartment,2 this does not change the security model.

The effect on code density should be investigated: does freeing up a GPR eliminate enough spills to offset the cost of fetching CGP via AUICGP in all cases?

Footnotes

  1. Requiring ASR to modify means that a compartment and the libraries it calls cannot foul up its CGP. The switcher could also rely on the constancy of this SCR outside itself, but it's not clear that there would be significant gains.

  2. Though the fast unsealer and perhaps other "privileged libraries" blur the text here, as they manipulate secrets not exposed to the calling compartment.

v2: Split sentries by direction

We have reserved space for, but do not presently implement, differentiating forward and backward sentries. There would then be at least five forms: forward with IRQ {preserved, disabled, enabled} and backward with IRQ {enabled, disabled}.

The ISA itself would need some tweaking: cjalr would need to seal PCC as one of the reverse types rather than one of the forward types, and cj and cjalr would need to differentiate between return and non-return transfers. Likely, absent any other encoding changes, this would enshrine cj ra (that is, cjalr x0, ra) as being a return instruction and prohibit its use for forward transfers, requiring modest toolchain work.

Clean up MTDC

We inherited the MTDC (trap default capability) special capability register from upstream but it isn't needed as we don't support hybrid mode. It would make more sense to get rid of it and keep only MScratchC, MEPCC and MTCC. This would need a few changes in ISA and RTOS:

  1. MTDC currently contains the RW root on reset. We'd need to put it somewhere else, perhaps in the c1/x1 GPR?
  2. The RTOS would need to switch to using MScratchC as a scratch register instead of MTDC! This should be trivial.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.