227 lines
7.4 KiB
Markdown
227 lines
7.4 KiB
Markdown
# 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
|