RESEARCH
Papers & Evidence
Read our technical papers and experimental results detailing the microvisor design and evaluation.
Publications
This paper presents the formal design of ZMatrix, a microvisor that enforces security invariants below the operating system kernel. We detail the architecture, prove key correctness properties, and demonstrate how hardware virtualization can be used to create an immutable trust boundary.
We measure the overhead of hardware-assisted mediation across diverse workloads. Results show sub-5% impact on real-world applications, with syscall interposition adding less than 200ns per call.
A formal treatment of process isolation using extended page tables. We prove non-interference properties and show that, under the hardware model, processes cannot observe or influence each other's execution—even with kernel-level privileges.
Benchmarks & Evaluation
Negligible overhead on compute-intensive workloads. The microvisor's mediation path is optimized to avoid unnecessary exits.
Syscall-heavy workloads see modest overhead. Each mediated call adds ~170ns on average.
High-frequency operations remain fast. Hardware-assisted checks avoid software instrumentation costs.
ZMatrix adds per-container isolation without disrupting orchestration. Policy enforcement scales linearly.
Technical Documentation
Policy Language Reference
Complete specification of the ZMatrix policy DSL, including syntax, semantics, and compiler internals.
Integration Guide
Step-by-step instructions for deploying ZMatrix on bare-metal servers, VMs, and container hosts.
Formal Proofs
Coq and Isabelle/HOL proofs for core security properties: isolation, non-interference, and integrity.
API Reference
Low-level API documentation for runtime introspection, policy queries, and attestation endpoints.
Open Research Collaboration
We welcome collaboration with academic institutions and security researchers. If you're interested in formal verification, OS security, or hardware-assisted isolation, reach out to discuss potential projects.