[PATCH] lib: sbi: Refresh the root memregion count after sanitize_domain()

[Nickolai Zeldovich]

From: Nickolai Zeldovich <nickolai.zeldovich at gmail.com>

root_add_memregion() counts the regions once, but sanitize_domain()
removes covered regions on every iteration, so the merge step's memmove
uses a stale count and runs past the terminating entry.  It stays in
bounds today only because the array has ROOT_REGION_MAX + 1 slots.

Recompute the count after each sanitize_domain().

Fixes: 0d5629381731 ("lib: sbi: Fix sbi_domain_root_add_memregion() for merging memregions")
Signed-off-by: Nickolai Zeldovich <nickolai.zeldovich at gmail.com>
Co-Authored-By: Claude Fable 5.1 <noreply at anthropic.com>
---
This bug was found in the process of formally verifying the correctness
of OpenSBI on top of the Sail RISC-V semantics using Lean.

Summary:

root_add_memregion() computes root_memregs_count once, then loops
sanitize_domain() + merge. sanitize_domain() can remove regions (any
region covered by a superset region is dropped and the array shifted
down), but the local count is never refreshed, so the merge step's
sbi_memmove(nreg1, nreg1 + 1, sizeof(*nreg1) * (root_memregs_count -
i1)) moves more entries than exist and runs past the array's terminating
entry. Today this stays inside the allocation only because the array is
allocated with ROOT_REGION_MAX + 1 slots and the stale count is bounded
by ROOT_REGION_MAX. Recompute the count after each sanitize_domain().

An execution that triggers it:

struct sbi_domain_memregion is 24 bytes (order, base, flags); the root
array has 33 slots (sbi_calloc(…, ROOT_REGION_MAX + 1)), the last one
the all-zero terminator (order == 0).

1. During sbi_domain_init() and the driver cold-inits, regions are added
   one at a time through sbi_domain_root_add_memregion(). Suppose N
   regions are registered so far (the virt platform registers 7 by the
   end of boot: firmware RW/RX, UART, CLINT MSWI, CLINT MTIMER, PLIC in
   two pieces, the all-RAM catch-all; N grows to 7).
2. A caller adds a region R that strictly covers an existing region S
   (same flags, S inside R). The ACLINT driver does this on virt: it
   registers the MSWI window 0x2000000/0x4000 and the MTIMER window
   0x2004000/0xc000 separately, and sanitize_domain() merges them when a
   covering 2^16 CLINT region appears. On entry root_memregs_count = N
   (say 7) and root.regions[7] is the terminator.
3. root_add_memregion() appends R at index 7, increments the local count
   to 8 and writes the terminator at index 8.
4. sanitize_domain() sorts, then finds S covered by R and removes it:
   sbi_memmove(&regions[i], &regions[i+1], 24 * (count - i)) with its
   OWN recomputed count, shifting the tail (including the terminator)
   down by one. The array now holds 7 live regions and the terminator at
   index 7. root_add_memregion()'s local root_memregs_count is still 8.
5. The merge loop (sbi_domain_for_each_memregion, which stops at the
   terminator) finds two adjacent same-order same-flag regions at
   indices i1 - 1 and i1 and merges them: nreg->order++, then
   sbi_memmove(nreg1, nreg1 + 1, 24 * (root_memregs_count - i1)). With
   the stale 8 this copies 8 - i1 entries starting at index i1 + 1, i.e.
   up to and including index 8, while the live data plus terminator end
   at index 7. It reads one entry beyond the terminator (index 8, inside
   the 33-slot allocation, all zero after calloc) and writes it over
   index 7.
6. Result: nothing visibly wrong *today*, because the over-read lands on
   a zeroed slot inside the allocation and copying zeros over the
   terminator's position leaves a terminator there. Every extra removal
   widens the gap by one slot. Two conditions turn it into a real fault:
   (a) 32 registered regions, where index 32 is the terminator and the
   over-read reaches index 33, past the sbi_calloc block, pulling heap-
   neighbour bytes into the region table (a non-zero order there extends
   the table with a bogus region that lands in the PMP configuration of
   every hart); (b) a change that drops + 1 from the allocation or
   reuses the slot, which the current code silently depends on.

The fix recomputes the count from the array (sbi_domain_used_memregions)
after every successful sanitize_domain() so the memmove covers exactly
the remaining regions plus the terminator.

Verification:

Proved: sbi_domain_root_add_memrange() on the virt platform's region
sequence satisfies its contract against a model of the region array. The
proof had to carry the out-of-range tail bytes explicitly to go through
on the unfixed code; with the fix the memmove's range is the live array.

lib/sbi/sbi_domain.c | 6 ++++++ 1 file changed, 6 insertions(+)

FYI, the same change is also filed as GitHub pull request #428:
https://github.com/riscv-software-src/opensbi/pull/428

diff --git a/lib/sbi/sbi_domain.c b/lib/sbi/sbi_domain.c
index b3f5892d..4924e1b1 100644
--- a/lib/sbi/sbi_domain.c
+++ b/lib/sbi/sbi_domain.c
@@ -748,6 +748,12 @@ static int root_add_memregion(const struct sbi_domain_memregion *reg)
 			return rc;
 		}
 
+		/*
+		 * sanitize_domain() may have dropped regions covered by
+		 * another region, so the count is stale at this point.
+		 */
+		root_memregs_count = sbi_domain_used_memregions(&root);
+
 		/* Merge consecutive memregions with same order and flags */
 		reg_merged = false;
 		sbi_domain_for_each_memregion(&root, nreg) {
-- 
2.55.0