ALIGNUX — Estado del proyecto
Un sistema operativo nuevo, sobre el núcleo mejor probado del mundo
ALIGNUX reconstruye la capa de servicios de un sistema operativo desde cero, apoyándose en el microkernel seL4 y en su verificación formal, para devolver al usuario el control de sus datos y de su máquina.
Cargando datos…
Mapa de verificación formal (septiembre de 2026)
La corrección funcional de seL4 está verificada en x86-64 sin MCS. La configuración MCS está verificada solo en RISC-V (Proofcraft, 2026). ALIGNUX usa seL4 16.0.0 en una configuración concreta; no afirma una verificación que no le corresponde.
x86-64 · sin MCS
verificadoBase del MVP en QEMU.
RISC-V · MCS
verificado (2026)Referencia de la planificación MCS.
x86-64 · MCS
sin verificarConfiguración de ejecución; se comunica sin ambigüedad.
Arquitectura: mecanismos dentro, políticas fuera
El kernel ofrece mecanismos (capacidades, IPC, programación); ALIGNUX define las políticas en servicios de espacio de usuario, cada uno en su propio dominio de protección (PD).
La pila, de arriba abajo
- seL4 16.0.0 — microkernel con capacidades y programación MCS.
- Microkit 2.3.1 — composición de PDs (SDF, asignación de recursos).
- Servicios Rust
no_std— memgr, namesrv, resmgr, vfs, drv_block, shell. - Adaptadores auditados en C — init, drv_uart.
Los ocho dominios de protección del MVP
| Dominio | Lenguaje | Rol |
|---|---|---|
init | C (auditado) | Arranque y composición inicial. |
memgr | Rust no_std | Particiones de Untyped y cuotas de memoria. |
namesrv | Rust no_std | Nombres → capacidades con ACL. |
resmgr | Rust no_std | PCI/ACPI y reparto de dispositivos. |
drv_block | Rust no_std | Disco (virtio-blk) con IOMMU. |
vfs | Rust no_std | Sistema de archivos nativo. |
shell | Rust no_std | Consola de pruebas. |
drv_uart | C (auditado) | Consola serie (patrón sDDF). |
Tres reglas que no se negocian
- Los nombres no conceden autoridad. Solo las capacidades otorgan acceso.
- Todo servidor pasivo ejecuta con el scheduling context donado por su cliente.
- Drivers «IOMMU-first». Todo DMA declara su
<io_address_space>(ADR-06).
Lo que ALIGNUX no es (todavía)
- No hay GUI antes de M4 (W-01).
- No hay POSIX nativo (W-02); la compatibilidad será un servidor/VM aislada en M5.
- No hay gestor dinámico antes de G1+G2 (W-04).
- No hay parches al núcleo en el MVP (W-03).
Por qué seL4 y no los otros
La elección de seL4 no es una moda: es el único núcleo de propósito general con corrección funcional formalmente verificada, un modelo de capacidades que minimiza la superficie de compromiso, y una planificación MCS apta para tiempo real.
| Núcleo | Verificación formal | Modelo | Nota para ALIGNUX |
|---|---|---|---|
| seL4 | Sí (funcional) | Microkernel + capacidades | Base elegida. |
| Linux | No | Monolítico | Referencia de compatibilidad (M5). |
| Minix 3 | No | Microkernel | Inspiración de servidores reincidentes. |
| GNU Hurd | No | Multi-servidor (Mach) | Referencia de POSIX como servicio. |
| Redox | No | Microkernel (Rust) | Referencia de stack Rust. |
Una precisión que el informe original ya hacía bien
El informe técnico distingue entre la corrección funcional del núcleo (verificada en ciertas configuraciones) y la corrección del sistema ALIGNUX en su conjunto (que solo podrá afirmarse con su propia evidencia, por configuración y por plataforma).
Roadmap: seis fases, cero atajos
Cada fase cierra con una puerta (Gate) que demuestra el criterio de salida de forma automática.
Cargando milestones…
Dependencias críticas
- M1 depende de M0 (toolchain y arranque).
- M2 depende de M1 (resmgr para asignar dispositivos).
- M3 solo arranca con M1–M2 cerrados (política W-04).
- M4 (AERO X16) depende del dominio de QEMU en M0–M3.
Backlog: 69 tareas con dueño y criterio de «hecho»
Cada tarea tiene criterio de aceptación medible, test de nivel L0–L6 asignado y trazabilidad a su especificación.
Cargando contadores…
Lista completa en GitHub Issues.
Política Won't: los «no» que protegen el proyecto
- W-01 — sin GUI antes de M4.
- W-02 — sin POSIX nativo; compatibilidad = servidor/VM aislada.
- W-03 — sin parches al núcleo en el MVP.
- W-04 — sin gestor dinámico antes de G1+G2.
- W-05 — no se afirma en público que «ALIGNUX está verificado» sin especificar qué, dónde y en qué configuración.
Validación: ningún avance sin su prueba
La pirámide de verificación detecta cada fallo en el nivel más bajo posible; L0–L4 bloquean el merge, L5 abre un issue, L6 es hardware.
Las seis puertas del proyecto
Cargando puertas…
La pirámide de verificación
| Nivel | Qué | Presupuesto | Bloquea |
|---|---|---|---|
| L0 | Estática (fmt, clippy, SDF, IDL) | < 3 min | merge |
| L1 | Unitaria | < 5 min | merge |
| L2 | Propiedades (10 000 casos) | < 10 min | merge |
| L3 | Integración (boot QEMU + consola + RPC) | < 15 min | merge |
| L4 | Inyección de fallos | < 30 min | main |
| L5 | Profunda (fuzzing 24 h, props 1 M, mutación) | nightly | issue |
| L6 | Hardware real (RC) | release | gate |
Los cuatro pipelines que lo ejecutan
- PR — L0 → L1/L2 → L3 → gate.
- Main — todo PR + L4 + diff de autoridad + cobertura ≥ 80 % + build reproducible (2 runners).
- Nightly — fuzzing, propiedades profundas, mutación, audit de dependencias.
- Release — build reproducible ×2, suite completa, artefactos firmados, SBOM.
Reglas anti-huecos
- Contratos versionados (la IDL sube de versión al cambiar).
- Autoridad declarativa (diff entre permisos reales y SDF).
- Golden boot log (arranque comparado estructuralmente).
- Cobertura ratchet ≥ 80 % (nunca baja).
- Trazabilidad
// verifies: T-x, S-x. - Sin merges directos a main.
Riesgos: once vigilados, tres aceptados
Cargando riesgos…
Aceptados conscientemente
- El arranque queda fuera del perímetro verificado.
- No hay pruebas binarias de seguridad en x86-64.
- MCS no está verificado en x86-64 (se comunica sin ambigüedad).
Fuentes
Las decisiones de ALIGNUX se apoyan en documentación verificable. Cada tarjeta indica qué decisión sostiene.