Imports and Mappings

Two declarations sit at the top of every .fi file: import brings an external C or Rust source file into scope under a chosen alias, and Mapping puts a memory region declared in the .fis into the protection domain’s address space.

Imports

ImportDecl ::= 'import' '"' FilePath '"' 'as' ident ';'
FilePath   ::= ident '.' ('c' | 'rs')

An import declaration names the external implementation that backs the PD’s computation events. The path is a single bare file name (no directories) ending in .c or .rs; the parser dispatches on the extension to record it as a C or Rust source. The alias becomes the prefix on every external call inside the PD.

import "eth.c" as eth;             // call: eth.send_frame(...)
import "dd.c" as dd;               // call: dd.forward_packet(...)
import "driver.rs" as driver;      // Rust source — same call shape

Multiple imports are allowed, and they may interleave with mappings — order does not matter for parsing. Each alias must be unique within the file.

Mappings

MappingDecl ::= SecurityLabel? 'Mapping' ident '(' region (',' vaddr)? ',' perms (',' cached)? ')' ';'

region      ::= ident                      // a MemoryRegion declared in .fis
vaddr       ::= hex                        // explicit virtual address (optional)
perms       ::= string_literal             // 'r', 'rw', 'rx', 'rwx', 'x', 'wx'
cached      ::= bool_literal               // default: false

A mapping declaration installs a MemoryRegion into the PD’s address space. The mapping’s name becomes a globally-visible symbol inside the PD; the Constructor block can then reference its .vaddr, .paddr, or .size.

Fields

• Security label — High or Low prefix, default Low. The mapping inherits the region’s confidentiality; the type-checker rejects a Low mapping over a High region. See Information-Flow Labels below.
• Name — the mapping’s own identifier. Distinct from the region’s name; one region can have multiple mappings under different names.
• Region — the MemoryRegion declared in the .fis file.
• Vaddr (optional) — pin the mapping at a specific virtual address. If omitted, the loader allocates one. Hex literal.
• Permissions — a quoted string of r/w/x characters. Order and case are insensitive: "rw" and "WR" are equivalent. Write-only is rejected; at least r or x must be present. The accepted set is r, rw, rx, rwx, x, wx.
• Cached (optional, default false) — whether the mapping is cached in the CPU MMU. Device MMIO regions are typically false.

Examples

// Anonymous shared buffer at allocator-chosen vaddr, read-write, uncached.
Low Mapping ring_buffer(ring_buffer_outer, "rw", false);

// Same region, default cached flag (false).
Mapping packet_buffer(packet_buffer_outer, "rw");

// Pinned vaddr — useful for debugging or for binding two PDs to a
// shared layout that pre-allocates virtual addresses.
Low Mapping eth0(eth0, 0x2_000_000, "rw");

// High-side mapping. Backed by a High MemoryRegion; rejected if the PD
// or the region's label disagrees.
High Mapping eth_clk(eth_clk, 0x2_200_000, "rw");

// Read-only mapping (data-diode input).
Low Mapping input_buf(eth_outer_output, "r");

Information-flow labels

Both MemoryRegion and Mapping declarations may carry a High or Low prefix. The two-level lattice is:

flows_to(Low,  Low)  = true
flows_to(Low,  High) = true       // upgrade is fine
flows_to(High, Low)  = false      // downgrade is rejected
flows_to(High, High) = true

In source: Low is the default — omitting the prefix is equivalent to writing Low. Place the prefix before the MemoryRegion / Mapping keyword; placing it elsewhere is a parse error.

The validator runs after parsing and rejects any mapping that violates flows_to(region.label, mapping.label). The data-diode demo uses this to enforce one-way information flow at the type-checker.

Validation

• Each Mapping’s region must reference a declared MemoryRegion.
• Permission strings must contain at least one of r or x. "w" alone is rejected.
• A pinned vaddr must be aligned to the region’s page size.
• Mapping names are unique within the same .fi file.