Skip to content

PointSav Documentation

The engineering library for the PointSav platform — operating systems and services for regulated businesses that own their data, their AI, and their record-keeping outright. Where the monorepo holds the code, this wiki holds the reasoning: architecture, services, security, and the governance commitments that bind future development.

PointSav Digital Systems

Last updated · 9b9339a2 · English

Sustrato del micronúcleo seL4

El micronúcleo seL4 es el núcleo de L1, verificado formalmente por demostración matemática, que PointSav ha adoptado como sustrato compartido planificado para sus sistemas operativos — sus propiedades de seguridad están demostradas, no aseveradas mediante pruebas. 1 Este es el sustrato objetivo de la plataforma, no una descripción de cada SO distribuido hoy: os-console, por ejemplo, se distribuye hoy como una aplicación de terminal estándar sin dependencia actual de seL4. PointSav adopta seL4 como materia prima en lugar de construir un núcleo propio, y construye su capa Rust propietaria por encima de él. Donde seL4 es el sustrato en ejecución real, el aislamiento de memoria, los desbordamientos de búfer nulos, los permisos basados en capacidades y la ejecución determinista están garantizados estructuralmente — la base para afirmaciones de seguridad que pueden razonarse formalmente y presentarse a reguladores. Este artículo cubre la justificación arquitectónica, la pila de capas, las restricciones de la cadena de herramientas y la disciplina de lenguaje aplicada por encima del núcleo.

Por qué adoptar en lugar de construir

Una alternativa razonable sería escribir un núcleo propio. PointSav rechaza explícitamente ese camino:

Opción Costo Resultado
Construir un núcleo propio Decenas de millones de dólares; cinco o más años de trabajo de verificación formal Alcanzar un estándar de 2009 en la década de 2030
Adoptar seL4 Cero Ya demostrado; listo para construir sobre él

El principio es usar seL4 como materia prima — como el acero estructural — y construir el valor propietario por encima. El trabajo técnico competitivo de PointSav ocurre en la capa Rust por encima de seL4, no en el núcleo mismo.

La pila de capas

Capa Componente Propietario
L0 — Hardware CPU x86_64 Haswell+ (véase referencia de hardware) Proveedor de hardware
L1 — Micronúcleo seL4 2 Proyecto seL4 (adoptado upstream; parches menores)
L2 — Marco de controladores sDDF (Marco de Controladores de Dispositivos seL4) con VirtIO Ecosistema seL4
L3 — Paquetes del sistema Crates Rust system-* — controladores, red, sistema de archivos PointSav
L4 — Servicios Crates Rust service-* — lógica de aplicación PointSav
L5 — Sistemas operativos Composiciones os-* PointSav
L6 — Aplicaciones Superficies de usuario app-* PointSav

El límite entre L2 (adyacente al núcleo) y L3 (propiedad de PointSav) es la línea que PointSav traza alrededor de su valor propietario. Todo lo que está por debajo es una materia prima adoptada; todo lo que está por encima es propiedad.

Cuando el hardware de destino no admite el arranque nativo de seL4, una máquina virtual invitada Linux o BSD dentro de un hipervisor basado en seL4 proporciona un aislamiento estructural equivalente alrededor del SO invitado. La capa del hipervisor ofrece contención formalmente verificada incluso cuando el invitado en sí es un sistema operativo convencional.

Qué proporciona seL4

Propiedad Qué significa en la práctica
Aislamiento matemático Si service-email falla, service-people no puede sentirlo; el núcleo garantiza el límite
Ejecución determinista Garantías en tiempo real sobre la temporización de instrucciones — importante para los protocolos de sincronización
Seguridad basada en capacidades Los permisos se pasan como tokens de capacidad criptográfica, no como entradas en una tabla de permisos central
Cero desbordamientos de búfer en el núcleo La clase de vulnerabilidad que produce la mayoría de los CVEs de sistemas operativos está matemáticamente excluida del núcleo

El resultado es un sustrato donde las propiedades de seguridad pueden razonarse formalmente en lugar de aseverarse mediante pruebas de penetración. Esto cambia el tipo de afirmaciones de seguridad que pueden presentarse defensiblemente a un regulador, y constituye la base del cumplimiento de prueba continua.

El Microkit y las restricciones de la cadena de herramientas

seL4 es intencionalmente mínimo: proporciona capacidades y comunicación entre procesos y muy poco más. Para hacerlo prácticamente utilizable, PointSav se apoya en el seL4 Microkit, un marco que traduce descripciones de sistema de alto nivel (manifiestos XML, binarios ELF) en las operaciones de capacidad de bajo nivel que el núcleo espera.

El Microkit tiene restricciones. Una está documentada en detalle en el archivo de ingeniería: el constructor x86_64 del Microkit mapea ávidamente Huge Pages de 1 GB para el código del núcleo, y luego no puede "fragmentar" esas páginas en sub-páginas de 4 KB cuando las asignaciones pequeñas posteriores colisionan. La resolución pragmática — colocar el búfer IPC en la parte inferior de la memoria y el núcleo justo por encima — es el tipo de disciplina detallada que exige trabajar en este nivel.

Este es un problema de calidad de vida del Microkit, no un error del núcleo. seL4 funciona según lo diseñado para un sistema de alta seguridad que prioriza el diseño de memoria determinista sobre la conveniencia del desarrollador.

Disciplina de lenguaje

El sustrato aplica un único lenguaje por encima del núcleo: Rust.

Lenguaje Estado Justificación
Rust Obligatorio para todo el código system-*, service-* y os-* Seguridad de memoria sin recolección de basura; se alinea con la verificación formal de seL4
C / C++ Prohibido en L3 y superior Un solo desbordamiento de búfer en C anula el valor de las demostraciones de seL4
Python / JavaScript Prohibido en L3 y superior Requiere tiempos de ejecución pesados; no puede ejecutarse como un Dominio de Protección seL4 sin violar las garantías de aislamiento
WebAssembly Permitido solo para extensiones de usuario invitado Un formato futuro de plugins de usuario; se ejecuta dentro de un tiempo de ejecución Wasm hospedado en Rust, nunca como servicio principal

Permitir un servicio que no sea Rust en un Dominio de Protección reintroduciría la sobrecarga del tiempo de ejecución y la ejecución impredecible que el sustrato del micronúcleo está diseñado para eliminar.

La arquitectura del estado final

La forma a largo plazo del sustrato es un Sistema Operativo de Micronúcleo Multi-Servidor: cada servicio — red, sistema de archivos, lógica de aplicación — se ejecuta como un unikernel aislado que pasa mensajes a través de IPC de seL4. El único trabajo del núcleo es el enrutamiento de hardware y la aplicación de capacidades.

Este es uno de los patrones más difíciles de la informática para implementar correctamente. El sustrato es ahora lo suficientemente maduro — a través de marcos como Genode y compiladores de unikernel basados en Rust — para que un proveedor institucional construya superficies de sistema operativo sobre él.

Véase también

  1. Klein, G., et al. 'seL4: Formal Verification of an OS Kernel.' ACM SOSP, 2009. https://dl.acm.org/doi/10.1145/1629575.1629596 ↩

  2. seL4 Foundation. 'Manual de Referencia seL4.' seL4 Foundation, 2023. https://sel4.systems/Info/Docs/seL4-manual-latest.pdf ↩

Cite this record: /wiki/sel4-microkernel-substrate — revision 9b9339a2, last updated 18 July 2026.

Important Information

Estructura corporativa. PointSav Digital Systems ("PointSav") es actualmente un nombre comercial de Woodfine Capital Projects Inc. ("Woodfine"), con previsión de convertirse en una subsidiaria de propiedad absoluta de Woodfine tras su incorporación. PointSav no ofrece, vende ni solicita por sí mismo valor alguno. Toda oferta de valores asociada a las soluciones inmobiliarias de tenencia directa de Woodfine se realiza exclusivamente por parte de Woodfine, y únicamente por medio del Memorando de Colocación Privada aplicable.

Sin asesoramiento de inversión. El contenido de este wiki se ofrece con fines de ingeniería, operativos, de investigación y de desarrollo. Nada de lo que figura en este wiki constituye asesoramiento de inversión ni una solicitud para invertir en ninguna sociedad o solución de tenencia directa de Woodfine.

Propiedad intelectual. El nombre, el nombre comercial, el logotipo y las marcas de PointSav, junto con todos los productos, servicios y ofertas actuales y futuros de las marcas PointSav y Totebox — así como el software, el código fuente, la documentación, el sistema de diseño y todos los materiales relacionados — son propiedad de Woodfine y sus filiales, salvo los componentes identificados como de código abierto. No se otorga ningún derecho salvo el expresamente establecido en una licencia o acuerdo por escrito. El aviso de marcas completo aparece en el pie de página de cada página de este sitio.

Componentes de código abierto. Algunas partes de la plataforma se ofrecen bajo licencias de código abierto permisivas identificadas en el repositorio correspondiente. El uso de esos componentes se rige por los términos de sus respectivas licencias.

Sin garantía; uso informativo. El contenido de este wiki se ofrece únicamente con fines informativos generales y no constituye una declaración, garantía ni compromiso respecto de la funcionalidad, disponibilidad, precio o hoja de ruta de ningún producto. Algunos artículos describen características, capacidades e hitos planificados o previstos — el lenguaje como "planificado", "previsto", "objetivo", "puede" y "esperado" marca este contenido prospectivo, que está sujeto a cambios y no constituye un compromiso respecto del rendimiento futuro.

Confidencialidad. Cuando un artículo describiría un detalle operativo o de implementación no destinado a divulgación pública, ese artículo no se publica en este wiki. El contenido aquí es documentación de ingeniería de uso general, no configuración específica de clientes.

Jurisdicción. Woodfine Capital Projects Inc. está constituida en Columbia Británica, Canadá. Las referencias a la Sovereign Data Foundation en este wiki describen una iniciativa planificada o prevista únicamente, no una titular de capital actual ni un órgano de gobierno activo.

Cambios a este aviso. PointSav podrá actualizar este aviso periódicamente; rige la versión publicada en esta página.

No es un sistema de presentación de documentos. Este wiki no es un sistema de presentación de valores, un repositorio de divulgación electrónica ni un sustituto de SEDAR+ ni de ningún otro sistema de presentación regulatorio. Las presentaciones formales de valores se realizan a través del sistema de presentación regulatorio correspondiente, no a través de este wiki.

Descargo completo. Este aviso complementa, y no sustituye, el artículo completo de Avisos Legales. En caso de cualquier conflicto, prevalece el artículo de Avisos Legales.

Read the full disclaimer →