Cheri-research/cheri-cap-lib
1
0
Fork 0
Code Issues 1 Pull Requests Actions Packages Projects Releases Wiki Activity

Update and rename readme.md to readme.adoc

Browse Source
This commit is contained in:
Alexandre Joannou
2022-09-30 12:22:47 +01:00
committed by GitHub
parent 149733072a
commit 49e6e07a70
2 changed files with 87 additions and 49 deletions
Download Patch File Download Diff File Expand all files Collapse all files

87
readme.adoc Normal file
View File

@@ -0,0 +1,87 @@
:toc: macro
:toclevels: 4
:toc-title:
:toc-placement!:
:source-highlighter:
++++
<br/>
++++
[discrete]
= CHERI CAP LIB
++++
<br/>
++++
The https://github.com/CTSRD-CHERI/cheri-cap-lib[cheri-cap-lib] repository
provides an RTL API for CHERI capabilities, as well as a reference
implementation of it. It aims to serve as a central implementation providing
various wrappers to avoid the need for multiplicity of implementation efforts.
This is particularly desirable when considering the verification work already
spent and the overall tricky nature of the algorithms involved.
The explicit goal of CHERI CAP LIB is to provide a set of relatively low level
operation to interact with CHERI capabilities, and allow the user to abstract
away the specifics of the published
https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/2019tc-cheri-concentrate.pdf[capability format]
as much as reasonably possible. Other implementations could easily comply to the
CHERI CAP LIB API.
The CHERI CAP LIB API is here to guaranty that subtleties in capability
manipulations are handled correctly. This means that direct bit manipulation on
CHERI capabilities bypassing the provided functions can very easily lead to
nonsense capabilities. For this reason, the CHERI CAP LIB API is more in the
style of a set of accessors (java interface / haskell typeclass, etc...) rather
than a simple struct-style interface with direct field manipulation. Again, this
is deliberate and necessary to the good behaviour of capability operations.
Currently, the implementation of the API is in Bluespec System Verilog and
wrappers are available in Verilog and Blarney.
[discrete]
== Contents
toc::[]
:sectnums:
== The CHERI CAP LIB API
[source, bsv]
----
function Bool isValidCap (t cap);
function t setValidCap (t cap, Bool valid);
function Bit#(flg) getFlags (t cap);
function t setFlags (t cap, Bit#(flg) flags);
function HardPerms getHardPerms (t cap);
function t setHardPerms (t cap, HardPerms hardperms);
function SoftPerms getSoftPerms (t cap);
function t setSoftPerms (t cap, SoftPerms softperms);
function Bit#(31) getPerms (t cap);
function t setPerms (t cap, Bit#(31) perms);
function Kind getKind (t cap);
function Bool isSentry (t cap);
function Bool isSealedWithType (t cap);
function Bool isSealed (t cap);
function Bit#(ot) getType (t cap);
function Exact#(t) setType (t cap, Bit#(ot) otype);
function Bit#(n) getAddr (t cap);
function Exact#(t) setAddr (t cap, Bit#(n) addr);
function t maskAddr (t cap, Bit#(maskable_bits) mask);
function Bit#(n) getOffset (t cap);
function Exact#(t) modifyOffset (t cap, Bit#(n) offset, Bool doInc);
function Exact#(t) setOffset (t cap, Bit#(n) offset);
function Exact#(t) incOffset (t cap, Bit#(n) inc);
function Bit#(n) getBase (t cap);
function Bit#(TAdd#(n, 1)) getTop (t cap);
function Bit#(TAdd#(n, 1)) getLength (t cap);
function Bool isInBounds (t cap, Bool isTopIncluded);
function Exact#(t) setBounds (t cap, Bit#(n) length);
function t nullWithAddr (Bit#(n) addr);
function t almightyCap;
function t nullCap;
function Bool validAsType (t dummy, Bit#(n) checkType);
function t fromMem (Tuple2#(Bool, Bit#(mem_sz)) mem_cap);
function Tuple2#(Bool, Bit#(mem_sz)) toMem (t cap);
----

49
readme.md
View File

@@ -1,49 +0,0 @@
# CHERI CAP LIB
The [cheri-cap-lib](https://github.com/CTSRD-CHERI/cheri-cap-lib.git) repository is meant to gather several specific implementations of CHERI capabilities and provide a common interface.
The `CHERICap` Bluespec typeclass in [CHERICap.bsv](CHERICap.bsv) captures the intended API to CHERI capabilities.
```bsv
function Bool isValidCap (t cap);
function t setValidCap (t cap, Bool valid);
function Bit#(flg) getFlags (t cap);
function t setFlags (t cap, Bit#(flg) flags);
function HardPerms getHardPerms (t cap);
function t setHardPerms (t cap, HardPerms hardperms);
function SoftPerms getSoftPerms (t cap);
function t setSoftPerms (t cap, SoftPerms softperms);
function Bit#(31) getPerms (t cap);
function t setPerms (t cap, Bit#(31) perms);
function Kind getKind (t cap);
function Bool isSentry (t cap);
function Bool isSealedWithType (t cap);
function Bool isSealed (t cap);
function Bit#(ot) getType (t cap);
function Exact#(t) setType (t cap, Bit#(ot) otype);
function Bit#(n) getAddr (t cap);
function Exact#(t) setAddr (t cap, Bit#(n) addr);
function t maskAddr (t cap, Bit#(maskable_bits) mask);
function Bit#(n) getOffset (t cap);
function Exact#(t) modifyOffset (t cap, Bit#(n) offset, Bool doInc);
function Exact#(t) setOffset (t cap, Bit#(n) offset);
function Exact#(t) incOffset (t cap, Bit#(n) inc);
function Bit#(n) getBase (t cap);
function Bit#(TAdd#(n, 1)) getTop (t cap);
function Bit#(TAdd#(n, 1)) getLength (t cap);
function Bool isInBounds (t cap, Bool isTopIncluded);
function Exact#(t) setBounds (t cap, Bit#(n) length);
function t nullWithAddr (Bit#(n) addr);
function t almightyCap;
function t nullCap;
function Bool validAsType (t dummy, Bit#(n) checkType);
function t fromMem (Tuple2#(Bool, Bit#(mem_sz)) mem_cap);
function Tuple2#(Bool, Bit#(mem_sz)) toMem (t cap);
```
The main currently used CHERI capability implementation using the "CHERI concentrate" format can be found in [CHERICC_Fat.bsv](CHERICC_Fat.bsv).
It is possible to export verilog wrappers for the [CHERICC_Fat.bsv](CHERICC_Fat.bsv) implementation of the `CHERICap` typeclass methods by runing `make verilog-wrappers`. It is also possible to export [blarney](https://github.com/mn416/blarney.git) wrappers by running `make blarney-wrappers`.
# TODO
- pull in the various known BSV implementations
- pull in the existing testing infrastructure