diff --git a/readme.adoc b/readme.adoc index 2af1da3..1b89c6f 100644 --- a/readme.adoc +++ b/readme.adoc @@ -1,55 +1,56 @@ -:toc: macro -:toclevels: 4 -:toc-title: -:toc-placement!: -:source-highlighter: - -++++ -
-++++ - -[discrete] -= CHERI CAP LIB - -++++ -
-++++ - -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 +:toc: macro +:toclevels: 4 +:toc-title: +:toc-placement!: +:source-highlighter: + +++++ +
+++++ + +[discrete] += CHERI CAP LIB + +++++ +
+++++ + +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 +operations 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] +and its subsequent iterations as much as reasonably possible. Other +implementations could easily comply with 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 are greatly discouraged as +they will 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...) than in that of a simple struct-style interface with direct +field manipulation. Again, this is deliberate and necessary to easily enforce +well behaved capability manipulations. + +Currently, the implementation of the API is in Bluespec System Verilog and wrappers are available in Verilog and Blarney. -[discrete] -== Contents - -toc::[] - -:sectnums: - +[discrete] +== Contents + +toc::[] + +:sectnums: + == The CHERI CAP LIB API -[source, bsv] ----- +[source, bsv] +---- function Bool isValidCap (t cap); function t setValidCap (t cap, Bool valid); function Bit#(flg) getFlags (t cap); @@ -83,5 +84,5 @@ 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); ----- +function Tuple2#(Bool, Bit#(mem_sz)) toMem (t cap); +----