From c3483a2959c60769f63974366acd8d7c254821c3 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Tue, 26 Nov 2024 14:17:12 +0000 Subject: [PATCH 1/3] properties/props: add prop_null_noperms --- properties/props.sail | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/properties/props.sail b/properties/props.sail index 175a2c8..7f636d7 100644 --- a/properties/props.sail +++ b/properties/props.sail @@ -22,6 +22,14 @@ function prop_nullzero() -> bool = { capEncodable(null_cap) & (capToBits(null_cap) == zeros()) & (null_cap.tag == false) } +$property +/*! + * Check that null_cap has no set permission bits. + */ +function prop_null_noperms() -> bool = { + getCapPerms(null_cap) == zeros() +} + $property function prop_mem_root() -> bool = { capEncodable(root_cap_mem) From 4d78de3019cfb7459b3bb24ce194185f1a506695 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Tue, 26 Nov 2024 14:14:26 +0000 Subject: [PATCH 2/3] archdoc/chap-encoding-sail: prettify & add props --- archdoc/chap-encoding-sail.tex | 50 ++++++++++++++++------------------ properties/props.sail | 25 ++++++++++------- 2 files changed, 38 insertions(+), 37 deletions(-) diff --git a/archdoc/chap-encoding-sail.tex b/archdoc/chap-encoding-sail.tex index 7b70eaa..a18a2ce 100644 --- a/archdoc/chap-encoding-sail.tex +++ b/archdoc/chap-encoding-sail.tex @@ -42,34 +42,30 @@ \section{SMT validation of properties of the capability encoding} Some helper functions are used in the Sail properties: -\medskip -\sailRISCVfn{encodeDecode} - -\medskip -\sailRISCVfn{capEncodable} - -The following functions have been checked to return true for all inputs. - -\medskip -\sailRISCVfn{prop\_decEnc} - -\medskip -\sailRISCVfn{prop\_andperms} +\begin{itemize} + \item \sailRISCVfn{encodeDecode} + \item \sailRISCVfn{capEncodable} +\end{itemize} -\medskip -\sailRISCVfn{prop\_setbounds} +The following nullary properties of the encoding hold. -\medskip -\sailRISCVfn{prop\_setbounds\_monotonic} +\begin{itemize} + \item \sailRISCVfn{prop\_nullzero} + \item \sailRISCVfn{prop\_null\_noperms} + \item \sailRISCVfn{prop\_mem\_root} + \item \sailRISCVfn{prop\_exe\_root} + \item \sailRISCVfn{prop\_seal\_root} +\end{itemize} -\medskip -\sailRISCVfn{prop\_setaddr} - -\medskip -\sailRISCVfn{prop\_repbounds\_c} - -\medskip -\sailRISCVfn{prop\_repbounds} +The following functions have been checked to return true for all inputs. -\medskip -\sailRISCVfn{prop\_crrl\_cram} \ No newline at end of file +\begin{itemize} + \item \sailRISCVfn{prop\_decEnc} + \item \sailRISCVfn{prop\_andperms} + \item \sailRISCVfn{prop\_setbounds} + \item \sailRISCVfn{prop\_setbounds\_monotonic} + \item \sailRISCVfn{prop\_setaddr} + \item \sailRISCVfn{prop\_repbounds\_c} + \item \sailRISCVfn{prop\_repbounds} + \item \sailRISCVfn{prop\_crrl\_cram} +\end{itemize} diff --git a/properties/props.sail b/properties/props.sail index 7f636d7..06ef9eb 100644 --- a/properties/props.sail +++ b/properties/props.sail @@ -19,7 +19,9 @@ $property * Check that null_cap as defined in the Sail encodes to all zeros. */ function prop_nullzero() -> bool = { - capEncodable(null_cap) & (capToBits(null_cap) == zeros()) & (null_cap.tag == false) + capEncodable(null_cap) + & (capToBits(null_cap) == zeros()) + & (null_cap.tag == false) } $property @@ -31,19 +33,22 @@ function prop_null_noperms() -> bool = { } $property -function prop_mem_root() -> bool = { - capEncodable(root_cap_mem) -} +/*! + * Check that [root_cap_mem] is encodable + */ +function prop_mem_root() -> bool = { capEncodable(root_cap_mem) } $property -function prop_exe_root() -> bool = { - capEncodable(root_cap_exe) -} +/*! + * Check that [root_cap_exe] is encodable + */ +function prop_exe_root() -> bool = { capEncodable(root_cap_exe) } $property -function prop_seal_root() -> bool = { - capEncodable(root_cap_seal) -} +/*! + * Check that [root_cap_seal] is encodable + */ +function prop_seal_root() -> bool = { capEncodable(root_cap_seal) } $property /*! From aa84b6ddd52127fe55a5723e312fbd26b8f964fd Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Fri, 8 Nov 2024 19:40:45 +0000 Subject: [PATCH 3/3] CAndPerms: permit clearing GL on sealed caps But require that all other bits in the mask provided to CAndPerms be 1 in order for a tagged sealed input to result in a tagged sealed output. Co-authored-by: Robert Norton --- archdoc/chap-changes.tex | 4 ++++ src/cheri_insts.sail | 22 +++++++++++++++++++--- 2 files changed, 23 insertions(+), 3 deletions(-) diff --git a/archdoc/chap-changes.tex b/archdoc/chap-changes.tex index 091993c..521fd15 100644 --- a/archdoc/chap-changes.tex +++ b/archdoc/chap-changes.tex @@ -45,5 +45,9 @@ \chapter{Version history} Instead, it merely requires that the otype of the sealed input is within bounds to yield a tagged result. The address of a sealing-root capability is now meaningful only to \rvcheriasminsnref{CSeal}. \item[\ghissue{72},\ghpr{74}] Introduce \rvcheriasminsnref{CSetBoundsRoundDown} to facilitate constructing representable slices of buffers. + \item[\ghissue{70},\ghpr{83}] \rvcheriasminsnref{CAndPerm} can now clear \cappermG on sealed caps, so long as that is the only bit being cleared. + Previously, this was possible by round-tripping to memory, loading back through an authority lacking \cappermILG(recall \ghpr{44} and \ghissue{14} above), but not directly as a register-to-register operation. + Presently, we require that the mask provided to \rvcheriasminsnref{CAndPerm} be all-1s except possibly \cappermG; + that is, feeding the result of \rvcheriasminsnref{CGetPerm} on a sealed capability to \rvcheriasminsnref{CAndPerm} will still clear the tag of the result. \end{description} \end{description} diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail index 26457d3..b973292 100644 --- a/src/cheri_insts.sail +++ b/src/cheri_insts.sail @@ -410,7 +410,8 @@ union clause ast = CAndPerm : (regidx, regidx, regidx) * previous value and bits 0 to [cap_perms_width]-1 of integer register *rs2*. * If the resulting set of permissions cannot be represented by the capability * encoding then the result will have a (possibly empty) subset of the ANDed - * permissions. If *cs1* was sealed then *cd*.**tag** is cleared. + * permissions. If *cs1* was sealed and *rs2* codes for clearing anything other + * than Permit_Global, then *cd*.**tag** is cleared. */ function clause execute(CAndPerm(cd, cs1, rs2)) = { let cs1_val = C(cs1); @@ -419,8 +420,23 @@ function clause execute(CAndPerm(cd, cs1, rs2)) = { let perms = getCapPerms(cs1_val); let mask = truncate(rs2_val, cap_perms_width); - let inCap = clearTagIfSealed(cs1_val); - let newCap = setCapPerms(inCap, (perms & mask)); + let newperms = perms & mask; + + /* + * CAndPerm on a sealed cap clears the tag unless the mask is all ones or + * has *only* the global permission clear. + * + * Here, perm_global is a bit vector (in the architectural format used by + * [CAndPerm] and [CGetPerm]) of all zeros except for the global permission + * bit. Its formulation here relies on null_cap having no asserted + * permissions (which we verify in our SMT properties; see + * [prop_null_noperms]). + */ + let perm_global = getCapPerms({ null_cap with global = true }); + let inCap = clearTagIf(cs1_val, + isCapSealed(cs1_val) & ((mask | perm_global) == ones())); + + let newCap = setCapPerms(inCap, newperms); C(cd) = newCap; RETIRE_SUCCESS