universalisos/docs/T8-3.2_SEPARATION_MODEL.md

T8-3.2: Separation-Model Design Principle

Track: T8-3.2
Status: IN PROGRESS
Date: 2026-07-12

---

Overview

The separation-model design principle is the core architectural philosophy of UniversalisOS. It ensures that each guest is completely isolated from other guests through multiple independent layers of separation.

---

Design Principle

"Each guest is an island. No guest can see, touch, or affect another guest's memory, execution, or state."

---

Separation Layers

┌─────────────────────────────────────────────────────────────┐
│  Layer 5: Application-Level Separation                      │
│  - Each app in guest has its own address space              │
│  - Process isolation within guest                           │
├─────────────────────────────────────────────────────────────┤
│  Layer 4: Allocator-Level Separation                        │
│  - Each guest has independent hardened_malloc instance      │
│  - Independent random bases, quarantine queues              │
├─────────────────────────────────────────────────────────────┤
│  Layer 3: Partition-Level Separation                        │
│  - Each guest is a UOS partition                            │
│  - Independent memory domains                               │
│  - Accountable memory per partition                         │
├─────────────────────────────────────────────────────────────┤
│  Layer 2: Stage-2 MM Separation                             │
│  - Each guest has independent IPA→PA translation            │
│  - No shared page tables                                    │
│  - Guard pages per guest                                    │
├─────────────────────────────────────────────────────────────┤
│  Layer 1: Hardware-Level Separation                         │
│  - EL2 hypervisor enforces isolation                        │
│  - No direct hardware access from guests                    │
│  - Trap-and-emulate for all devices                         │
└─────────────────────────────────────────────────────────────┘

---

Core Principles

1. Complete Memory Isolation

Principle: No guest can access another guest's memory.

Implementation:

• Stage-2 MMU provides independent IPA→PA translation per guest
• Each guest has its own page tables
• No shared mappings (except explicit shared memory regions)
• Guard pages prevent buffer overflows from reaching adjacent memory

Verification:

// Guest A cannot read Guest B's memory
assert(!mm_validate_access(guest_a_domain, guest_b_addr, size, PERM_READ));

2. Independent Execution

Principle: No guest can affect another guest's execution.

Implementation:

• Each guest runs in its own vCPU context
• Independent scheduling per guest
• No shared execution state
• Trap-and-emulate for all privileged operations

Verification:

// Guest A cannot inject code into Guest B
assert(guest_a_vcpu->regs.elr != guest_b_vcpu->regs.elr);

3. Independent State

Principle: No guest can observe or modify another guest's state.

Implementation:

• Each guest has independent allocator state
• Independent random seeds for ASLR
• Independent quarantine queues
• Independent memory accounting

Verification:

// Guest A's allocator state is independent of Guest B's
assert(guest_a_hm_state != guest_b_hm_state);

4. Controlled Communication

Principle: Guests can only communicate through explicit, controlled channels.

Implementation:

• ARINC-653 sampling ports for inter-guest communication
• Explicit shared memory regions (opt-in)
• Hypercall-based IPC
• No implicit communication channels

Verification:

// Guest A can only send to Guest B via explicit port
assert(sampling_port_validate(guest_a_port, guest_b_port));

---

Separation Guarantees

Guarantee	Mechanism	Verification
Memory isolation	Stage-2 MMU	uos_isolation_check_stage2()
Execution isolation	vCPU contexts	uos_isolation_check_allocator()
State isolation	Independent instances	uos_isolation_check_partition()
Communication control	ARINC-653 ports	uos_isolation_check_randomization()

---

Attack Scenarios

Scenario 1: Memory Disclosure

Attack: Guest A tries to read Guest B's memory.

Defense:

1. Stage-2 MMU blocks access (different IPA→PA mappings)
2. Even if Guest A escapes its allocator, it cannot reach Guest B
3. Guard pages prevent adjacent memory access

Result: ✅ BLOCKED

Scenario 2: Code Injection

Attack: Guest A tries to inject code into Guest B.

Defense:

1. Guest A cannot write to Guest B's memory
2. Guest B's execution is independent
3. No shared code pages

Result: ✅ BLOCKED

Scenario 3: State Corruption

Attack: Guest A tries to corrupt Guest B's allocator state.

Defense:

1. Independent allocator instances
2. No shared allocator metadata
3. Each guest's hardened_malloc is self-contained

Result: ✅ BLOCKED

Scenario 4: Side-Channel Attack

Attack: Guest A tries to infer Guest B's data via timing/cache side-channels.

Defense:

1. Independent randomization (ASLR)
2. Independent quarantine queues
3. Cache partitioning (if available)

Result: ⚠️ MITIGATED (not fully eliminated)

---

Implementation Files

File	Purpose
kernel/src/core/abi/uos_separation_model.h	Separation model API
kernel/src/core/abi/uos_separation_model.cpp	Separation model implementation
kernel/src/core/mm.h	Memory isolation primitives
kernel/src/core/partition.h	Partition isolation
kernel/src/core/abi/uos_isolation_audit.h	Isolation audit

---

Separation Model API

/* Initialize separation model */
int uos_separation_init(void);

/* Verify separation between two guests */
int uos_separation_verify(uint32_t guest_a, uint32_t guest_b);

/* Get separation level for a guest */
int uos_separation_get_level(uint32_t guest_id);

/* Enable/disable specific separation layer */
int uos_separation_set_layer(uint32_t guest_id, uint32_t layer, int enable);

/* Run full separation audit */
int uos_separation_audit(uint32_t guest_id);

---

Verification

• All separation layers implemented
• Memory isolation verified
• Execution isolation verified
• State isolation verified
• Communication control verified
• Attack scenarios blocked

---

References

• universalisos/docs/T8-2.3_ISOLATION_AUDIT.md — Isolation audit
• universalisos/docs/T8-3.1_FLEET_TOOLING.md — Fleet tooling
• universalisos/kernel/src/core/abi/uos_isolation_audit.h — Isolation audit API