Kernel bare-metal verificato in Rust per Raspberry Pi 4 con task cooperativi, agenti EL0, IPC e MMU W^X
#rust#bare-metal#aarch64#kernel#raspberry-pi#no-std
Flusso di esecuzione di harbor-kernel. Nodi: ingress, router, planner, executor, state, audit. Flusso: da ingress a router (primario); da router a executor (primario); da executor a state (primario); da router a planner (di supporto); da planner a state (di supporto); da executor a audit (feedback).
Problema
Volevo un piccolo kernel Rust per Raspberry Pi 4 che rendesse visibili i meccanismi principali di un sistema operativo: task cooperativi, esecuzione di agenti in EL0, IPC e permessi di memoria W^X. I metadati del repository indicano un ambito sperimentale bare-metal su AArch64; non dichiaro uso in produzione, adozione o risultati di benchmark.
Progettazione del sistema
Ho strutturato il progetto come kernel bare-metal Rust no_std per AArch64. Il design ruota attorno a un modello di task cooperativi, a un confine EL0 per gli agenti, a primitive IPC e a una configurazione della MMU pensata per applicare permessi W^X. Mantengo espliciti i confini in modo che cambi di privilegio, percorsi di comunicazione e permessi di memoria siano ispezionabili come meccanismi del kernel invece che come comportamento nascosto del runtime.
Risultato
Il risultato è un repository pubblico centrato su una base di kernel Rust verificato per Raspberry Pi 4. L'ambito supportato è l'architettura del kernel descritta nei metadati: esecuzione bare-metal, scheduling cooperativo, agenti EL0, IPC e lavoro sulla MMU W^X. Dove i metadati non forniscono dettagli, considero lo stato sconosciuto invece di dedurlo.
Architettura
- kernel Rust no_std
- target AArch64 per Raspberry Pi 4
- modello di task cooperativi
- confine agenti EL0
- primitive IPC
- configurazione MMU W^X
Modello di runtime
- contesto di avvio bare-metal
- scheduling cooperativo
- esecuzione agenti in modalità utente
- IPC orientato ai messaggi
- permessi espliciti dello spazio di indirizzamento
Strumenti
- Rust
- no_std
- AArch64
- Raspberry Pi 4
- GitHub
Affidabilità
- policy di memoria W^X
- separazione dei privilegi con EL0
- flusso di controllo cooperativo
- superficie bare-metal ridotta
- ambito del kernel orientato alla verifica
contesto di avvio bare-metal→scheduling cooperativo→esecuzione agenti in modalità utente→IPC orientato ai messaggi→permessi espliciti dello spazio di indirizzamento
Vincoli
Questo è un progetto bare-metal per Raspberry Pi 4, quindi il design resta vicino all'hardware e non presume un runtime di sistema operativo ospitato, una libreria standard o un normale modello di processo. I metadati del repository non forniscono copertura dei test, dettagli sulle prove, stato di distribuzione o dati di benchmark.
Compromessi
Rust e no_std tengono l'implementazione lontana dalle assunzioni di un runtime ospitato, ma rendono esplicito il lavoro specifico per l'hardware. Lo scheduling cooperativo è più semplice da ispezionare rispetto alla preemption, ma richiede che i task cedano il controllo in modo intenzionale. I confini W^X ed EL0 supportano obiettivi di isolamento al prezzo di maggiore complessità nella MMU e nella gestione del contesto.
Evoluzione
Se continuassi il progetto, renderei più ispezionabile il percorso di verifica: nominare le invarianti che il kernel dichiara di rispettare, documentare come rieseguire i controlli che le stabiliscono e dichiarare che cosa resta non dimostrato.