Hypervision Plane

High-assurance hypervisor (HV), poll-mode VirtIO engine (VIO), and operating system (OS.1) built for zero-copy, hard real-time microVMs, unikernels, and cloud virtualization environments.

The Hypervision Triple: HV, VIO, OS.1

The Hypervision Plane brings together three foundational pillars of modern, capability-governed virtualization: the formally verified seL4 hypervisor wrapper (HV), the freestanding poll-mode VirtIO driver engine (VIO / libvio), and the unified virtualization environment and deployment platform (OS.1). Together, they eliminate legacy QEMU overhead and provide sub-millisecond boot latency with microsecond I/O responsiveness.

Hypervisor Root

HV (Hypervisor)

Root isolation layer powered by the seL4 microkernel. Manages memory via strict capability derivations and runs unprivileged Protection Domains (PDs) in total hardware isolation.

VirtIO Poll Engine

VIO (libvio)

Freestanding C11 VirtIO & NVMe engine engineered with TRON real-time discipline. Zero hidden heap allocations on hot paths, SPDK-style poll-mode queues, and zero-copy ring processing.

Deployment Platform

OS.1

Complete Virtualization Environment (VE) and CI/CD platform unifying HV and VIO to orchestrate Alpine, NetBSD, Erlang BEAM unikernels, and C99 microVM protection domains.

Target VirtIO Cloud Virtualization Environments (VEs)

Synrc Hypervision and VIO target four primary Virtualization Environments (VEs), ranging from bare-metal seL4 microkernels to enterprise cloud hypervisor clusters and containerized orchestration engines.

VE #0 — Native

0) OS.1 VE

Native seL4/Microkit and microVM target providing poll-mode NVMe storage fast paths and sub-millisecond boot latency. Designed to challenge NanoVMs on density, memory footprint, and deterministic real-time discipline.

VE #1 — Foreign

1) Proxmox VE

Seamless integration with Proxmox VE clusters via QEMU/KVM virtio devices and high-performance vhost-user backends over UNIX domain sockets for enterprise cloud workloads.

VE #2 — Virtual Machines

2) NetBSD VirtIO

Direct integration with the seL4 Device Driver Framework (sDDF). Operates isolated Protection Domains (PDs) like libseL4.c and dedicated Crypto Enclaves backed by Trusted Storage Systems (TSS).

VE #3 — Orchestration

3) Kubernetes

Cloud-native microVM virtualization via KubeVirt, libkrun, or crosvm. Enables containerized CI/CD pipelines to run ultra-dense Erlang and C99 workloads under Kubernetes.

The VIO VirtIO Architecture

The architecture of libvio is structured around clean physical module boundaries, strict separation of device front-ends from platform backends, and hard real-time queue discipline.

1. Platform Control-Plane Backends (src/backend/platform/)

Platform abstractions isolate memory translation and interrupt routing via the vio_platform_ops interface across diverse control planes:

Platform Backends

  • platform/sel4/libseL4.c: seL4 Protection Domain & sDDF driver interface. Includes tss_stub.c for isolated Trusted Storage System key persistence.
  • platform/apple/libkrun.c: macOS Hypervisor.framework RAM translation and krun_create_ctx() microVM context creation.
  • platform/linux/liblinux.c: Linux VFIO userspace PCIe passthrough and portable vhost-user UNIX domain socket transport.
  • platform/hyperv/libhyperv.c: Windows Hyper-V and VMBus control-plane integration.
  • platform/netbsd/libbsd.c: NetBSD and BSD /dev/pci character device memory mapping.
/* vio_platform.h Interface Contract */
struct vio_platform_ops {
    void *(*map_memory)(uint64_t phys_addr, 
                        uint32_t len);
    void  (*unmap_memory)(void *virt_addr, 
                          uint32_t len);
    vio_status_t (*register_irq)(uint32_t irq, 
                                 void (*handler)(void *ctx), 
                                 void *ctx);
    void (*mask_irq)(uint32_t irq);
    void (*unmask_irq)(uint32_t irq);
};
2. Low-Latency NVMe Fast Path (src/backend/nvme/)

The local block storage path achieves near-native PCIe performance by granting libvio exclusive ownership of the physical NVMe controller:

SPDK-Style Hardware Driver

Direct PCI BAR MMIO mapping, Controller Capability (CAP) register doorbell stride calculation, and lockless circular Submission Queues (SQ) and Completion Queues (CQ).

Phase-bit toggling enables lockless polling without hardware interrupt latency on hot paths.

/* nvme_qpair.c Submission Fast Path */
uint16_t tail = qpair->sq_tail;
vio_memcpy(&qpair->sq[tail], cmd, sizeof(*cmd));
qpair->sq_tail = (tail + 1) % qpair->size;

/* Ring PCIe MMIO Doorbell */
*qpair->sq_db = qpair->sq_tail;
3. Client Devices (src/devices/)

Modular device front-ends provide lightweight driver interfaces for guest protection domains:

devices/blk.c

VirtIO Block: Poll-mode block I/O backed directly by the high-performance NVMe qpair layer.

devices/net.c

VirtIO Network: Packet transmission and reception queues for virtio-net guests.

devices/console.c

VirtIO Console: Low-latency serial streams for terminal vision and system diagnostics.

devices/crypto.c

VirtIO Crypto: Enclave-isolated encryption/decryption operations backed by TSS key persistence.

devices/bus.c

VirtIO Bus: Unified device enumeration for PCIe and MMIO discovery with minimal devicetree support.

4. VIO Core Components & Protocols (src/core/ & src/util/)

The core VirtIO protocol state engine operates with strict freestanding C11 discipline:

Core Protocol Engine

  • core/queue.c: Split-ring virtqueue layout mechanics (Descriptor Table, Available Ring, Used Ring).
  • core/transport_mmio.c & transport_pci.c: Transport layers for MMIO memory mapped I/O and modern PCIe BAR configuration.
  • core/feature.c: VirtIO 1.x feature bit negotiation protocols.
  • core/config.c: VirtIO device configuration space read/write helpers.

Freestanding Utilities (src/util/)

  • atomic.c / atomic.h: Hardware atomic memory barriers for lockless queue synchronization.
  • list.c / list.h: Intrusive doubly-linked list routines.
  • mem.c / mem.h: Freestanding memory copy/set/compare operations without libc dependency.
  • log.c / log.h: Minimal, non-blocking logging routines.

Verified Test Assurance

The libvio engine is verified by a custom, zero-dependency unit and loopback test suite (make test) covering virtqueue byte movement, device front-ends, NVMe hardware simulation, and platform context creation.

Starting libvio test suite...

Running test_queue_init_invalid... PASS
Running test_queue_init_valid... PASS
Running test_queue_has_used... PASS
Running test_virtio_data_transfer... PASS
Running test_blk_init... PASS
Running test_blk_read_unsupported... PASS
Running test_nvme_qpair_submit_poll... PASS
Running test_libkrun_mapping... PASS
Running test_libkrun_blk_init... PASS
Running test_libkrun_net_init... PASS
Running test_libkrun_create_context... PASS

=== TEST SUMMARY ===
Run: 11
Passed: 11
Failed: 0