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 · a1c7d582 · English

PPN: Arquitectura seL4 de Tres Caminos

La pila de nodos de la Red Privada PointSav está diseñada en torno al micronúcleo seL4. Tres opciones de arquitectura definen la hoja de ruta. Son secuenciales: la Opción B es el camino de desarrollo actual; la Opción C requiere que la Opción B se publique y permanezca estable; la Opción A requiere que la Opción C esté completa. Las tres se documentan juntas para que las decisiones tomadas en la Opción B no eliminen las opciones posteriores.

Opción B — Hipervisor seL4 con invitado Linux

Prioridad de desarrollo actual — todavía no es el sistema operativo del nodo PPN en funcionamiento. El código real de arranque de os-infrastructure que correría hoy en un nodo PPN no tiene ninguna integración con seL4: es un stub Multiboot2 de metal desnudo (salida de texto por framebuffer, un escaneo mDNS de pares), y todos los servicios PPN — WireGuard, gestión de flota, enrutamiento de inferencias — se ejecutan hoy sobre Linux convencional, no dentro de un invitado alojado por seL4. Existe trabajo real y sustancial de ingeniería seL4 (un entorno de ejecución de unikernel/dominios de protección aparte, moonshot-sel4-vmm, con dominios de protección de consola/IPC/serie/UART/panel/red comprobados funcionando, incluida una solicitud HTTP real sobre DMA de VirtIO-net), pero todavía no está integrado en el propio camino de arranque de os-infrastructure. El diseño de abajo es el objetivo hacia el que apunta ese trabajo de desarrollo.

Una vez construido: seL4 funcionaría como hipervisor de Tipo 1 a EL2 (AArch64) o con VT-x (x86-64). El VMM CAmkES funcionaría como un dominio de protección seL4 y alojaría una máquina virtual Linux (Debian 12). Todos los servicios PPN — WireGuard, gestión de flota, enrutamiento de inferencias — se ejecutarían dentro de ese invitado Linux.

Hardware
└── Micronúcleo seL4 (EL2 / VT-x)
    └── VMM CAmkES [PD seL4]
        └── Invitado Linux (Debian 12)
            ├── Interfaz de malla WireGuard
            ├── service-vm-fleet
            ├── service-vm-host
            └── os-network-admin

Qué proporciona seL4: El núcleo está formalmente verificado. Ninguna máquina virtual invitada puede acceder a la capa del hipervisor, a la memoria de otro invitado ni a ningún objeto del núcleo seL4 sin una concesión explícita de capacidad seL4. En AArch64 EL2, la prueba de integridad (abril de 2025) extiende esto a una garantía verificada mecánicamente.

Qué no proporciona seL4 en la Opción B: El VMM CAmkES y el invitado Linux no están formalmente verificados. Un invitado Linux comprometido permanece confinado por la topología de capacidades de seL4, pero los servicios dentro del invitado son de confianza entre sí según el modelo de procesos normal de Linux.

Cobertura de seguridad formal:

Arquitectura Afirmación formal Notas
AArch64 EL2 Prueba de integridad seL4 (abril de 2025) Afirmación de seguridad formal válida en el límite del hipervisor
x86-64 Solo corrección funcional Sin prueba de integridad formal; objetivo de desarrollo únicamente

Opción C — Dominios de protección seL4 poseen WireGuard

Estado: previsto/con intención. Requisito: la Opción B se publica y permanece estable durante seis meses o más.

Arquitectura híbrida. Los dominios de protección seL4 son propietarios de WireGuard y del plano de control de red PPN. Una máquina virtual Linux invitada aloja cargas de trabajo no críticas. El límite de seguridad es el dominio de protección WireGuard — la VM Linux no puede modificar las tablas de pares sin pasar por IPC seL4.

Micronúcleo seL4 (EL2 / VT-x)
├── PD: wireguard-control  [tabla de pares WireGuard, gestión CPace]
├── PD: ppn-gate           [aplicación de canales IPC seL4]
└── VMM CAmkES
    └── Invitado Linux (Doorman, flota, telemetría, multimedia)

Al mover la interfaz de malla WireGuard a un dominio de protección seL4, una VM Linux totalmente comprometida no puede acceder a las tablas de pares ni a la capacidad de añadir o eliminar nodos. Las solicitudes de adición de pares fluyen a través de IPC seL4 hacia el dominio wireguard-control, que valida cada solicitud de forma independiente.

Qué cambia respecto a la Opción B: la gestión WireGuard de os-network-admin se mueve de Linux a un PD seL4; el invitado Linux no tiene interfaz wg0; las solicitudes de adición de pares siguen el flujo VM Linux → IPC seL4 → PD wireguard-control → estado del núcleo.

Opción A — Dominios de protección seL4 puros, sin máquinas virtuales

Estado: previsto/con intención. Requisito: la Opción C se publica y permanece estable.

Sin máquinas virtuales. Sin VMM. Cada servicio PPN es un dominio de protección seL4. WireGuard está portado a un PD seL4 sin capa de socket Linux. La gestión de flota y el enrutamiento de servicios son dominios de protección. Esto produce la base informática de confianza más pequeña posible.

Micronúcleo seL4 (EL2 — solo AArch64 para afirmaciones formales)
├── PD: wireguard     [criptografía WireGuard + tabla de pares, solo IPC seL4]
├── PD: fleet-tracker [service-vm-fleet, sin tokio, sin std net]
├── PD: doorman       [enrutamiento de inferencias, basado en IPC seL4]
└── PD: ppn-control   [os-network-admin, ceremonia CPace]

Eliminar el invitado Linux extrae el componente no verificado más grande de la pila. En AArch64 EL2 con la prueba de confidencialidad en curso a mediados de 2026, la Opción A apunta a las tres propiedades CIA en la capa del núcleo — la postura de seguridad más profunda de las tres opciones.

Objetivos de arquitectura de Microkit 2.2.0

Microkit 2.2.0 — el marco recomendado por la Fundación seL4 para nuevos proyectos seL4 — admite estos objetivos de hardware:

Objetivo Arquitectura Virtualización por hardware Verificación
aarch64 AArch64 No (solo EL2) Prueba de integridad (abril de 2025)
x86_64_generic x86-64 No (software TCG) Corrección funcional
x86_64_generic_vtx x86-64 Sí (VT-x/AMD-V) Corrección funcional

La compatibilidad con x86-64 se añadió en Microkit 2.1.0. Esta arquitectura es un objetivo de desarrollo y tiempo de ejecución válido, pero no cuenta con las pruebas de integridad o confidencialidad disponibles en AArch64.

Resumen

Opción seL4 como Linux Base de cómputo de confianza Verificación Estado
B (prioridad actual) Hipervisor VM invitada seL4 + VMM + Linux Integridad AArch64 Prioridad de desarrollo; aún no integrado en el camino de arranque de os-infrastructure
C (previsto) Hipervisor + PD WireGuard VM invitada (limitada) seL4 + VMM + PD WireGuard + Linux Integridad AArch64 Previsto/con intención
A (previsto) SO (todos los componentes) Ninguno Solo seL4 AArch64 todas CIA (en curso) Previsto/con intención

Véase también

Cite this record: /wiki/ppn-three-path-architecture — revision a1c7d582, last updated 29 June 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 →