Memory Region Declarations

MemoryRegionDecl ::= SecurityLabel? 'MemoryRegion' ident '(' size (',' page_size)? (',' phys_addr)? ')' ';'
size             ::= hex
page_size        ::= hex      // '0x1000' (4 KiB) | '0x200000' (2 MiB)
phys_addr        ::= hex
SecurityLabel    ::= 'High' | 'Low'

A memory region declaration introduces one named region of physical or virtual memory that protection domains can later map into their address space. MemoryRegion declarations live in .fis system files; they are pure topology and carry no per-PD program logic.

Fields

• Security label (optional, defaults to Low). Tags information-flow level. High regions can be mapped only into PDs that themselves carry flow restrictions consistent with the flows_to lattice — see Information-Flow Labels.
• Name — snake_case identifier; the same name is referenced from Mapping declarations in .fi files.
• Size — required, hex literal, in bytes. Must be a multiple of the region’s page size (validation runs post-parse and reports a size not aligned error if not).
• Page size — optional, defaults to 0x1000 (4 KiB). The other accepted value is 0x200000 (2 MiB / Large). See Page sizes.
• Physical address — optional. When present, must be aligned to the region’s page size. Used for device MMIO regions (clock controller, ethernet registers) where the seL4 loader maps a fixed physical frame rather than allocating one.

Security label and ordering

The label, if present, comes before the MemoryRegion keyword. Omitting it is equivalent to writing Low:

MemoryRegion ring_buffer_outer(0x1000, 0x1000);          // Low (default)
Low MemoryRegion eth0(0x10000, 0x10000, 0x5b040000);     // explicit Low
High MemoryRegion ring_buffer_inner(0x1000, 0x1000);     // High
High MemoryRegion eth_clk(0x1000, 0x1000, 0x5b200000);   // High MMIO

Validation

The following checks run after parsing:

1. size is a positive multiple of page_size.
2. phys_addr (if present) is aligned to page_size.
3. The region name is unique within the system file.

A region is referenced from .fi files by its name; the validator confirms each Mapping’s mem_region points at a declared MemoryRegion.

Examples

// Anonymous shared buffer, default 4 KiB page, allocator-assigned phys_addr.
MemoryRegion ring_buffer_outer(0x1000, 0x1000);

// 2 MiB region — large pages, allocator-assigned phys_addr.
MemoryRegion packet_buffer_outer(0x200000, 0x200000);

// Memory-mapped device (4 KiB MMIO, fixed physical address).
Low MemoryRegion eth_outer_register(0x1000, 0x1000, 0xf000000);

// 64 KiB device register window.
Low MemoryRegion eth0(0x10000, 0x10000, 0x5b040000);

// High-side region (any access from a Low PD will be rejected by the
// information-flow check).
High MemoryRegion eth_clk(0x1000, 0x1000, 0x5b200000);