# 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:**
```c
// 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:**
```c
// 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:**
```c
// 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:**
```c
// 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

```c
/* 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