Skip to content

Commit d1f6575

Browse files
author
Axel Heider
committed
reorder capability chapter
Show the encoding first so it is easier to find. Signed-off-by: Axel Heider <[email protected]>
1 parent 3ad0a46 commit d1f6575

File tree

1 file changed

+108
-98
lines changed

1 file changed

+108
-98
lines changed

src/cap-description.adoc

+108-98
Original file line numberDiff line numberDiff line change
@@ -14,32 +14,64 @@ define XLENMAX to be widest XLEN that the implementation supports.
1414
XLENMAX without including the tag bit. The value of CLEN is always calculated
1515
based on XLENMAX regardless of the effective XLEN value.
1616

17+
[#section_cap_encoding]
18+
=== Capability Encoding
19+
20+
ifdef::cheri_v9_annotations[]
21+
NOTE: *CHERI v9 Note:* The encoding changes eliminate the concept of the
22+
in-memory format, and also increase precision for RV32. When EF=0, T and B
23+
are now shifted right rather than left within the address. Also, the bounds
24+
decoding for XLENMAX=32 uses a trick (see bit T8) to save one bit when encoding
25+
the exponent.
26+
endif::[]
27+
28+
The components of a capability except the tag are encoded as shown in
29+
xref:cap_encoding_xlen32[xrefstyle=short] for XLENMAX=32 and
30+
xref:cap_encoding_xlen64[xrefstyle=short] for XLENMAX=64. Each memory location
31+
or register able to hold a capability must also store the tag as out of band
32+
information that software cannot directly set or clear. The capability metadata
33+
is held in the most significant bits and the address is held in the least
34+
significant bits.
35+
36+
.Capability encoding for XLENMAX=32
37+
[#cap_encoding_xlen32]
38+
include::img/cap-encoding-xlen32.edn[]
39+
40+
.Capability encoding for XLENMAX=64
41+
[#cap_encoding_xlen64]
42+
include::img/cap-encoding-xlen64.edn[]
43+
44+
Reserved bits are available for future extensions to {cheri_base_ext_name}.
45+
46+
NOTE: Reserved bits must be 0 in valid capabilities.
47+
1748
=== Components of a Capability
1849

1950
Capabilities contain the software accessible fields described in this section.
2051

2152
[#section_tag]
2253
==== Tag
2354

24-
An additional hardware managed bit added to addressable memory and registers.
25-
It is stored separately and may be referred to as "out of band". It indicates
26-
whether a register or CLEN-aligned memory location contains a valid capability.
27-
If the tag is set, the capability is valid and can be dereferenced (contingent
28-
on checks such as permissions or bounds).
55+
The tag is an additional hardware managed bit added to addressable memory and
56+
registers. It is stored separately and may be referred to as "out of band". It
57+
indicates whether a register or CLEN-aligned memory location contains a valid
58+
capability. If the tag is set, the capability is valid and can be dereferenced
59+
(contingent on checks such as permissions or bounds).
2960

3061
The capability is invalid if the tag is clear. Using an invalid capability to
3162
dereference memory or authorize any operation gives rise to exceptions. All
3263
capabilities derived from invalid capabilities are themselves invalid i.e.
3364
their tags are 0.
3465

35-
3666
All locations in registers or memory able to hold a capability are CLEN+1 bits
3767
wide including the tag bit. Those locations are referred as being _CLEN-bit_ or
3868
_capability_ wide in this specification.
3969

4070
[#section_cap_perms]
4171
==== Architectural Permissions (AP)
4272

73+
===== Description
74+
4375
ifdef::cheri_v9_annotations[]
4476
WARNING: *CHERI v9 Note:* The permissions are encoded differently in this
4577
specification.
@@ -75,7 +107,7 @@ Execute Permission (X):: Allow instruction execution.
75107
[#asr_perm,reftext="ASR-permission"]
76108
Access System Registers Permission (ASR):: Allow access to privileged CSRs.
77109

78-
===== Permission Encoding
110+
===== Encoding
79111

80112
The bit width of the permissions field depends on the value of XLENMAX as shown
81113
in xref:perms_bit_width[xrefstyle=short]. A {cap_rv32_perms_width}-bit vector
@@ -192,7 +224,9 @@ also seals the return address capability (if any) since it is the entry point
192224
to the caller function.
193225

194226
[#section_cap_bounds]
195-
==== Bounds
227+
==== Bounds (EF, T, TE, B, BE)
228+
229+
===== Concept
196230

197231
ifdef::cheri_v9_annotations[]
198232
NOTE: *CHERI v9 Note:* The bounds mantissa width is different in XLENMAX=32.
@@ -262,52 +296,8 @@ xref:exp_bit_width[xrefstyle=short].
262296
NOTE: The address and bounds must be representable in valid capabilities i.e.
263297
when the tag is set (see xref:section_cap_malformed[xrefstyle=short]).
264298

265-
==== Address
266-
267-
XLENMAX integer value that encodes the byte-address of a memory location.
268-
269-
.Address widths depending on XLENMAX
270-
[#address_bit_width,options=header,align="center",width="55%"]
271-
|==============================================================================
272-
^| XLENMAX ^| Address width
273-
^| 32 ^| {cap_rv32_addr_width}
274-
^| 64 ^| {cap_rv64_addr_width}
275-
|==============================================================================
276-
277-
==== Reserved Bits
278-
279-
Reserved bits available for future extensions to {cheri_base_ext_name}.
280-
281-
NOTE: Reserved bits must be 0 in valid capabilities.
282-
283-
[#section_cap_encoding]
284-
=== Capability Encoding
285-
286-
ifdef::cheri_v9_annotations[]
287-
NOTE: *CHERI v9 Note:* The encoding changes eliminate the concept of the
288-
in-memory format, and also increase precision for RV32. When EF=0, T and B
289-
are now shifted right rather than left within the address. Also, the bounds
290-
decoding for XLENMAX=32 uses a trick (see bit T8) to save one bit when encoding
291-
the exponent.
292-
endif::[]
293-
294-
The components of a capability are encoded as shown in
295-
xref:cap_encoding_xlen32[xrefstyle=short] and
296-
xref:cap_encoding_xlen64[xrefstyle=short] when XLENMAX=32 and XLENMAX=64
297-
respectively.
298-
299-
.Capability encoding when XLENMAX=32
300-
[#cap_encoding_xlen32]
301-
include::img/cap-encoding-xlen32.edn[]
302-
303-
.Capability encoding when XLENMAX=64
304-
[#cap_encoding_xlen64]
305-
include::img/cap-encoding-xlen64.edn[]
306-
307-
Each memory location or register able to hold a capability must also store the
308-
tag as out of band information that software cannot directly set or clear. The
309-
capability metadata is held in the most significant bits and the address
310-
is held in the least significant bits.
299+
[#section_cap_bounds_decoding]
300+
===== Decoding
311301

312302
The metadata is encoded in a compressed format cite:[woodruff2019cheri]. It
313303
uses a floating point representation to encode the bounds relative to the
@@ -427,23 +417,49 @@ if ( (E < (CAP_MAX_E - 1)) & (t[XLENMAX: XLENMAX - 1] - b[XLENMAX - 1] > 1) )
427417
That is, invert the most significant bit of _t_ if the decoded length of the
428418
capability is larger than E.
429419

430-
[#section_null_inf_cap]
431-
=== NULL and Infinite Capabilities
420+
[#section_cap_malformed]
421+
===== Malformed Bounds
432422

433-
ifdef::cheri_v9_annotations[]
434-
NOTE: *CHERI v9 Note:* Encoding <<null-cap>> as zeros removes the need for
435-
the difference between in-memory and architectural format.
436-
endif::[]
423+
A capability is _malformed_ if its encoding does not describe a valid
424+
capability because its bounds cannot be correctly decoded. The following check
425+
indicates whether a capability is malformed.
426+
427+
```
428+
malformedMSB = (E == CAP_MAX_E && B[MW - 1:MW - 2] != 0)
429+
|| (E == CAP_MAX_E - 1 && B[MW - 1] != 0)
430+
malformedLSB = (E < 0)
431+
malformed = !EF && (malformedMSB || malformedLSB)
432+
```
437433

438-
The <<null-cap>> capability is represented with 0 in all fields. This implies
439-
that <<null-cap>> has no permissions and its exponent E is CAP_MAX_E e.g. 52
440-
when XLENMAX=64, so its bounds cover the entire address space such that the
441-
expanded base is 0 and top is 2^XLENMAX^. In contrast, the <<infinite-cap>>
442-
capability grants all permissions while its bounds also cover the whole address
443-
space.
434+
NOTE: The check is for malformed _bounds_, so it does not include reserved
435+
bits!
444436

445-
NOTE: The <<infinite-cap>> capability is also known as 'default', 'almighty',
446-
or 'root' capability.
437+
Capabilities with malformed bounds are always invalid anywhere in the system
438+
i.e. their tags are always 0.
439+
440+
==== Address
441+
442+
XLENMAX integer value that encodes the byte-address of a memory location.
443+
444+
.Address widths depending on XLENMAX
445+
[#address_bit_width,options=header,align="center",width="55%"]
446+
|==============================================================================
447+
^| XLENMAX ^| Address width
448+
^| 32 ^| {cap_rv32_addr_width}
449+
^| 64 ^| {cap_rv64_addr_width}
450+
|==============================================================================
451+
452+
453+
[#section_special_caps]
454+
=== Special Capabilities
455+
456+
[#section_null_cap]
457+
==== NULL Capability
458+
459+
The <<null-cap>> capability is represented with 0 in all fields. This implies
460+
that it has no permissions and its exponent E is CAP_MAX_E (52 for XLENMAX=64,
461+
24 for XLENMAX=32), so its bounds cover the entire address space such that the
462+
expanded base is 0 and top is 2^XLENMAX^.
447463

448464
.Field values of the NULL capability
449465
[#null-cap,reftext="NULL",options=header,align=center,width="55%",cols="1,1,3"]
@@ -459,10 +475,25 @@ or 'root' capability.
459475
| B | zeros | Base address bits
460476
| B~E~ | zeros | Exponent bits
461477
| Address | zeros | Capability address
478+
| Reserved| zeros | All reserved fields
462479
|==============================================================================
463480

481+
ifdef::cheri_v9_annotations[]
482+
NOTE: *CHERI v9 Note:* Encoding <<null-cap>> as zeros removes the need for
483+
the difference between in-memory and architectural format.
484+
endif::[]
485+
486+
[#section_infinite_cap]
487+
==== Infinite Capability
488+
489+
The <<infinite-cap>> capability grants all permissions while its bounds also
490+
cover the whole address space.
491+
492+
NOTE: The <<infinite-cap>> capability is also known as 'default', 'almighty',
493+
or 'root' capability.
494+
464495
.Field values of the Infinite capability
465-
[#infinite-cap,reftext="Infinity"]
496+
[#infinite-cap,reftext="Infinite"]
466497
[options=header,width="100%",align=center,width="55%",cols="1,1,3"]
467498
|==============================================================================
468499
| Field | Value | Comment
@@ -476,20 +507,20 @@ or 'root' capability.
476507
| B | zeros | Base address bits
477508
| B~E~ | zeros | Exponent bits
478509
| Address | zeros | Capability address
510+
| Reserved| zeros | All reserved fields
479511
|==============================================================================
480512

481513
[#section_cap_representable_check]
482514
=== Representable Limit Check
483515

484516
Pointer arithmetic on capabilities must be checked to ensure that the new
485-
address is within the capability's representable region described in
486-
xref:section_cap_encoding[xrefstyle=short]. The new address, after pointer
487-
arithmetic, is within the representable region if decompressing the
488-
capability's bounds with the original and new addresses yields the same base
489-
and top addresses. In other words, given a capability with address _a_ and the
490-
new address `a' = a + x`, the bounds _b_ and _t_ are decoded using _a_ and the
491-
new bounds _b'_ and _t'_ are decoded using _a'_. The new address is within the
492-
capability's representable region if `b == b' && t == t'`.
517+
address is within the capability's representable region described by the bounds.
518+
The new address, after pointer arithmetic, is within the representable region if
519+
decompressing the capability's bounds with the original and new addresses yields
520+
the same base and top addresses. In other words, given a capability with address
521+
_a_ and the new address `a' = a + x`, the bounds _b_ and _t_ are decoded using
522+
_a_ and the new bounds _b'_ and _t'_ are decoded using _a'_. The new address is
523+
within the capability's representable region if `b == b' && t == t'`.
493524

494525
Changing a capability's address to a value outside the representable region
495526
unconditionally clears the capability's tag.
@@ -500,24 +531,3 @@ then the bounds will need to be recalculated. Instructions like <<CINCOFFSET>>
500531
and <<CSETADDR>> update the address field but do not recalculate the bounds.
501532
Therefore, if the leading 1 moves relative to when the bounds were calculated
502533
then the tag is cleared on the result as the encoding has been invalidated.
503-
504-
[#section_cap_malformed]
505-
=== Malformed Capability Bounds
506-
507-
A capability is _malformed_ if its encoding does not describe a valid
508-
capability because its bounds cannot be correctly decoded. The following check
509-
indicates whether a capability is malformed.
510-
511-
```
512-
malformedMSB = (E == CAP_MAX_E && B[MW - 1:MW - 2] != 0)
513-
|| (E == CAP_MAX_E - 1 && B[MW - 1] != 0)
514-
malformedLSB = (E < 0)
515-
malformed = !EF && (malformedMSB || malformedLSB)
516-
```
517-
518-
NOTE: The check is for malformed _bounds_, so it does not include reserved
519-
bits!
520-
521-
Capabilities with malformed bounds are always invalid anywhere in the system
522-
i.e. their tags are always 0.
523-

0 commit comments

Comments
 (0)