PSOS: el OS verificado que SRI publicó en 1980 e inspiró seL4 y Fuchsia

⏱️ Lectura: 11 min

PSOS (Provably Secure Operating System), publicado en 1980 por Peter Neumann y su equipo en SRI International, es uno de esos papers que casi todos los investigadores en seguridad de sistemas operativos citan pero que pocos leen directamente. Cuarenta y cinco años después, sus ideas centrales —capacidades como mecanismo primario, diseño jerárquico verificable, separación rigurosa por niveles— son la base sobre la que se construyen los kernels más seguros que se usan hoy: seL4, Genode, Zircon (el núcleo de Fuchsia) y el reciente KataOS de Google.

📑 En este artículo

1. TL;DR
2. Qué dice el paper
3. Contexto histórico: por qué SRI buscaba un OS demostrable
4. La arquitectura de PSOS: capabilities y 17 niveles
5. Datos y cifras
6. Impacto: de PSOS a seL4 y Fuchsia
7. Cómo se ve un kernel moderno basado en capabilities
8. Qué sigue: el resurgimiento formal en 2026
9. Preguntas frecuentes
   1. ¿PSOS se llegó a usar en producción?
   2. ¿Qué son las capabilities en este contexto?
   3. ¿Cuál es la diferencia con un kernel monolítico como Linux?
   4. ¿Por qué importa hoy una idea de hace 45 años?
   5. ¿Quién es Peter Neumann?
   6. ¿Dónde puedo leer el paper original?
10. Referencias

Lo que en 1980 era una propuesta teórica sin implementación completa terminó moldeando, paso a paso, el rumbo de la seguridad de sistemas operativos modernos. En 2026, con vulnerabilidades críticas en kernels monolíticos apareciendo cada mes, el modelo PSOS vuelve a ser referencia obligada.

TL;DR

• PSOS fue propuesto en 1980 por Peter Neumann y equipo en SRI International como el primer OS con seguridad demostrable formalmente.
• Su arquitectura jerárquica de 17 niveles introdujo capabilities (capacidades) como mecanismo principal de control de acceso.
• Usó SPECIAL, un lenguaje de especificación formal pionero, para describir y verificar propiedades de seguridad.
• Nunca se implementó completo, pero influenció KSOS, GEMSOS, EROS, KeyKOS y, finalmente, seL4.
• seL4, primer kernel formalmente verificado de propósito general (2009), es heredero directo de la línea PSOS.
• Fuchsia/Zircon de Google y Genode son sistemas modernos con arquitectura basada en capabilities al estilo PSOS.
• En 2026, con kernels monolíticos sumando vulnerabilidades cada mes, el diseño PSOS recupera vigencia académica e industrial.

Qué dice el paper

El documento original, titulado A Provably Secure Operating System: The System, Its Applications, and Proofs, proponía algo radical para 1980: diseñar un sistema operativo cuyas propiedades de seguridad pudieran demostrarse matemáticamente. No “auditadas”, no “probadas” empíricamente con tests. Demostradas como un teorema.

Para lograrlo, el equipo de SRI combinó dos ideas que hoy son estándar pero entonces eran exóticas: capabilities (tokens protegidos por el kernel que representan el derecho de acceder a un objeto) y una arquitectura por capas donde cada nivel solo puede invocar funciones del nivel inmediatamente inferior. El resultado: un kernel cuyo núcleo de confianza es mínimo y cuya superficie de ataque es analizable formalmente.

El paper no es solo un diseño; es una metodología. Introduce el concepto de Hierarchical Development Methodology (HDM) y el lenguaje SPECIAL para escribir especificaciones formales que después puedan compararse contra el código real. Era, esencialmente, programación con teoremas adjuntos décadas antes de que el término formal methods se volviera popular en industria.

Contexto histórico: por qué SRI buscaba un OS demostrable

A finales de los 70 el Departamento de Defensa de Estados Unidos enfrentaba un problema concreto: las computadoras de tiempo compartido tenían usuarios con distintos niveles de autorización (Confidential, Secret, Top Secret) sobre los mismos datos. ¿Cómo garantizar que un proceso con clearance Secret no leyera datos Top Secret, ni siquiera por canales encubiertos?

El Anderson Report (1972) había planteado la pregunta. El modelo Bell-LaPadula (1973) formalizó el no read up, no write down. El Orange Book (TCSEC, 1983) intentaría estandarizarlo en certificaciones A1, B3, B2, B1. Pero entre el modelo y la certificación faltaba el sistema real: alguien que demostrara que se podía construir un OS multi-nivel y, además, probarlo.

PSOS fue, en parte, esa respuesta. SRI International, contratada por agencias gubernamentales, se propuso diseñar la pieza faltante. Neumann (que sigue activo en SRI en 2026, casi seis décadas después de su llegada) lideró un equipo que incluyó a Richard Boyer, Karl Levitt y Lawrence Robinson, entre otros, varios de ellos pioneros del razonamiento mecanizado.

📌 Nota: SRI International (antes Stanford Research Institute) es el mismo laboratorio donde nacieron el mouse, el segundo nodo de ARPANET y, después, Siri. Su Computer Science Laboratory (CSL) sigue siendo uno de los pocos sitios donde se hace investigación seria de verificación formal aplicada a sistemas reales.

La arquitectura de PSOS: capabilities y 17 niveles

El diseño de PSOS organizaba toda la funcionalidad del sistema en 17 niveles abstractos, del más bajo (registros físicos, manejo de capabilities) al más alto (procesos de usuario, abstracciones de alto nivel). Cada nivel definía un conjunto de tipos abstractos y operaciones sobre esos tipos. Y aquí está el truco: un nivel solo podía usar tipos y operaciones definidos en niveles inferiores.

Algunos niveles representativos (de menor a mayor):

• Nivel 0-2: capability registers, segment management, paging.
• Nivel 3-5: abstract types, interrupts, primitive I/O.
• Nivel 6-9: virtual memory, system processes, naming.
• Nivel 10-13: directories, files, asynchronous I/O.
• Nivel 14-16: command interpreter, user processes, user environment.

El componente conceptual más importante es la capability. Cada capability es un par (referencia a objeto, conjunto de derechos) cuya integridad la garantiza el hardware o el kernel. Si un proceso quiere leer un archivo, no presenta el nombre del archivo: presenta una capability que prueba que tiene permiso. Sin capability, no hay acceso. No hay tabla de ACL global que consultar ni listas de UID que comparar.

Esto resuelve un problema clásico de los kernels monolíticos: la ambient authority. En Linux o Windows, un proceso con UID root puede tocar prácticamente cualquier cosa porque “es root”. En un sistema basado en capabilities, un proceso solo puede tocar aquello para lo que tiene una capability explícita, sin importar quién lo ejecute.

Datos y cifras

• 1980: año del paper definitivo.
• 17 niveles en la jerarquía PSOS.
• ~50 módulos distribuidos entre los niveles.
• SPECIAL: lenguaje de especificación formal usado para describir tipos y operaciones.
• 2009: año en que seL4 logra la primera verificación formal de un kernel general (~200,000 líneas de prueba en Isabelle/HOL para ~10,000 líneas de C).
• 2016: Google inicia desarrollo público de Fuchsia, sistema basado en capabilities heredado del linaje PSOS.
• 2024-2026: cerca de 800 CVE de severidad alta o crítica en kernel Linux por año, según estadísticas públicas del NVD — el contraste con cero exploits aprovechables del kernel verificado de seL4 alimenta el renovado interés.

Impacto: de PSOS a seL4 y Fuchsia

PSOS nunca se implementó por completo. Lo que sí ocurrió es una cadena de descendientes que llegan hasta el presente:

• KSOS (Kernelized Secure Operating System, ~1980): intento de implementar parcialmente las ideas PSOS sobre PDP-11.
• GEMSOS (1980s): kernel comercial certificado A1 por TCSEC, también heredero directo.
• KeyKOS (Key Logic, 1980s): primer sistema verdaderamente capability-based en producción comercial, sobre System/370.
• EROS (1990s, Jonathan Shapiro): reescritura moderna y open source de KeyKOS, introduce persistencia ortogonal.
• Coyotos (2000s): sucesor de EROS, diseñado explícitamente para verificación formal.
• seL4 (2009, NICTA/Data61): primera verificación formal completa de un kernel L4 estándar. Probado correcto respecto a su especificación, sin race conditions, sin null pointer dereferences, sin overflows.
• Genode (2008-presente): framework de OS basado en componentes y capabilities, usable hoy como sistema desktop sobre seL4 o NOVA.
• Fuchsia / Zircon (Google, 2016-): kernel capability-based usado en Nest Hub y experimentalmente en otros productos.
• KataOS (Google Research, 2022): OS embebido sobre seL4 con drivers en Rust verificado.

La línea genealógica no es metafórica: Neumann publicó trabajos junto a Shapiro; varios ingenieros de seL4 citan PSOS como referencia fundacional; y los conceptos de thread y endpoint en seL4 son evolución reconocible de los tipos abstractos en SPECIAL.

💭 Clave: seL4 no es solo un kernel verificado; es la prueba empírica de que la apuesta de Neumann en 1980 era correcta. Veintinueve años después del paper, alguien finalmente lo construyó y demostró el teorema.

Cómo se ve un kernel moderno basado en capabilities

Para entender por qué PSOS importa en 2026, conviene ver código real. En seL4 un proceso pide un servicio enviando un mensaje a un endpoint; para hacerlo, necesita una capability sobre ese endpoint. Esquemáticamente:

// seL4 IPC: enviar un mensaje requiere capability
seL4_MessageInfo_t info = seL4_MessageInfo_new(0, 0, 0, 1);
seL4_SetMR(0, 0xCAFE);
seL4_Call(endpoint_cap, info);

Si el proceso no tiene endpoint_cap en su CSpace, la operación falla antes de ejecutar nada. No hay UID que verificar, no hay tabla global de permisos. La autoridad la lleva la capability, no la identidad del proceso. Esa es la herencia directa de PSOS.

El siguiente diagrama muestra el flujo conceptual de una llamada en un sistema basado en capabilities, frente al paradigma tradicional de un kernel monolítico:

flowchart LR
    A["Proceso usuario"] -->|"capability"| B["Kernel verifica"]
    B -->|"valida"| C["Operacion ejecuta"]
    B -->|"falta"| D["Denegado"]
    C --> E["Resultado"]

Qué sigue: el resurgimiento formal en 2026

Varias señales apuntan a que las ideas PSOS están volviendo al centro de la conversación:

• Verificación formal en producción: AWS verifica formalmente firmware de Nitro, Microsoft usa F* en componentes de Hyper-V, Apple ha aplicado verificación en partes del Secure Enclave.
• Rust en kernels: Linux acepta drivers en Rust desde 2022; Asterinas y Hubris son kernels nuevos escritos enteramente en Rust con discusión activa sobre cómo añadirles verificación formal.
• Verificación asistida por IA: proyectos como Aeneas y Verus exploran usar LLMs para asistir pruebas en Lean 4 y Coq, lo que abarata el costo histórico de verificación que mantuvo a PSOS como propuesta mayormente teórica.
• Hardware con capabilities: la arquitectura CHERI (Capability Hardware Enhanced RISC Instructions), implementada experimentalmente en Morello y en propuestas de ARM, lleva las capabilities al silicio. Era exactamente lo que Neumann anticipaba en los niveles más bajos de PSOS.

💡 Tip: Si querés probar un OS capability-based hoy mismo, descargá Genode Sculpt OS: corre sobre NOVA o seL4 y es usable como desktop. Es lo más cerca que vas a estar del espíritu PSOS funcionando en tu laptop.

📖 Resumen en Telegram: Ver resumen

Preguntas frecuentes

¿PSOS se llegó a usar en producción?

No completamente. PSOS fue principalmente un diseño con especificación formal; los esfuerzos de implementación parcial (KSOS) llegaron a prototipos pero no a despliegue masivo. Sus ideas, sin embargo, sí se usan en producción hoy vía seL4 (vehículos autónomos, dispositivos médicos), Fuchsia (Nest Hub) y KataOS.

¿Qué son las capabilities en este contexto?

Una capability es un token no-falsificable que combina una referencia a un objeto con un conjunto de derechos sobre ese objeto. Solo quien tenga la capability puede operar sobre el objeto. Es lo contrario del modelo de ambient authority (UID/GID) que usan Unix y Windows.

¿Cuál es la diferencia con un kernel monolítico como Linux?

Linux integra millones de líneas de código en espacio de kernel: drivers, filesystems, networking. Un solo bug crítico en cualquiera de esos componentes compromete todo el sistema. Un microkernel basado en capabilities, al estilo PSOS, deja solo unas pocas miles de líneas en espacio privilegiado y mueve el resto a espacio de usuario, donde una falla queda contenida.

¿Por qué importa hoy una idea de hace 45 años?

Porque la cantidad de CVE críticos en kernels monolíticos crece año tras año, mientras el costo industrial de las brechas también crece. seL4 demostró que la verificación formal funciona; la pregunta abierta es cómo escalarla a sistemas completos. La arquitectura PSOS sigue siendo la mejor referencia disponible.

¿Quién es Peter Neumann?

Peter G. Neumann es Senior Principal Scientist en el Computer Science Laboratory de SRI International. Lleva más de seis décadas trabajando en seguridad de sistemas. Es editor del foro RISKS Digest desde 1985 y autor de Computer-Related Risks (1995). Sigue activo y publicando en 2026.

¿Dónde puedo leer el paper original?

El paper completo está disponible en el sitio personal de Neumann en SRI: csl.sri.com/users/neumann/psos.pdf. La versión expandida con pruebas fue publicada como SRI Technical Report CSL-116.

Referencias

• A Provably Secure Operating System (SRI, 1980) — paper original de Neumann y equipo.
• seL4 Microkernel — implementación moderna verificada formalmente, heredera directa de la línea PSOS.
• Fuchsia / Zircon (Google) — sistema operativo capability-based en uso comercial.
• Página personal de Peter G. Neumann en SRI — publicaciones y archivos de RISKS Digest.
• Capability-based security (Wikipedia) — visión general del paradigma.
• Genode OS Framework — entorno desktop sobre microkernels como seL4 y NOVA.

📱 ¿Te gusta este contenido? Únete a nuestro canal de Telegram @programacion donde publicamos a diario lo más relevante de tecnología, IA y desarrollo. Resúmenes rápidos, contenido fresco todos los días.