How KOS works
The systems that power modern life deserve more than conventional security
Kry10 provides mathematically proven foundations that help keep critical business and infrastructure systems resilient by design.
Software running critical systems has been built in the same way that software has always been built: by testing it until it appeared to work.
KOS is different. The secure foundation of KOS enables you to run applications right on the formally-verified seL4® microkernel. Only your workload runs, with no intermediary and no unnecessary code, on a formally verified foundation. With a small and proven microkernel, you know what you can count on.
The world’s best foundation for the systems society depends on
What is a monolithic kernel
A conventional operating system, with a monolithic kernel, is like an open-plan office.
Every part of the operating system’s kernel shares the same space and resources.
When a threat gets through the ‘front door’, it can move freely throughout the whole building.
Secure Separation
KOS gives every system part its own secured partition, like the rooms in a hotel
With seL4®, most operating-system functionality is forced out of the kernel and into unprivileged, user-level components. KOS adopts what's called a multi-server design. Each service that would otherwise live inside a monolithic kernel instead runs as its own isolated, address-space-separated component with only the privileges it needs.
KOS gives every system part its own secured partition, like the rooms in a hotel, with access only to what it's explicitly been granted. If one component is compromised or crashes, the breach or failure stays contained inside that partition.
KOS enforces specific configurations, creating a trustworthy SBOM that defines what is actually running, rather than a “Software Bill of Hope”, that outlines what you hope is running. Cyber assessment teams can look at a KOS SBOM and know that it is going to work.
Mathematically proven
Safe and Isolated Kernel
-
At the core of most computers is a small piece of software called the kernel, which decides what every other program on the machine is allowed to do.
-
KOS is built on seL4 — the first operating system kernel with a machine-checked mathematical proof that its implementation does exactly what its specification says.
-
Every component runs in its own protected space, with access only to what it has been explicitly granted.
-
The damage doesn’t spread through the whole device the way it can on a conventional system where everything shares the same space.
KOS Features
Foundations for the KOS Architecture
-
Isolation
Independent components are isolated from each other, enabling consolidation of independent functionality of the same or different criticality levels on a single device without increasing security and reliability risks.
-
Explicit access control
Components only access resources or communicate with other components if they have explicit permission to do so. All the possible privileges in the system are known, making it possible to limit the information and control flow in a system.
-
Least privilege
Components do not have more privileges than needed to perform their functions, limiting potential damage caused by misbehaving components.
-
Specification
System components, resources, and their privileges are explicitly defined in a specification. The specification will be used when configuring and running a system and can be analyzed to determine its (and the resulting system's) properties.
-
Supervision and Recovery
System components are monitored at runtime and if they crash for any reason, a supervisor can detect and restart them and dependent components. A 'crash first' approach deals with unexpected or unrecoverable errors.
How it works
Full KOS Architecture
Click on a component for more information
Apps + Drivers
A KOS device can run multiple independent or interdependent applications simultaneously, relying on the underlying isolation to prevent these applications from interfering with each other. Most system developers will develop software that will run at this level.
KOS Infrastructure
KOS provides a set of optional applications that perform the behavior you'd expect from a conventional OS, such as a network stack and file system, application environments, drivers and container support. Only the applications that you choose to include will exist on your system.
seL4® Microkernel
The seL4® microkernel is the foundation of KOS for implementing its operating system primitives. seL4® is the key for providing guarantees about isolation and access control in a KOS-based system.
The KOS engine makes it easy to set up these primitives exactly as you intend without any surprises, and then stops running until you need it to perform secure dynamic updates
Hardware
The physical device or machine that runs KOS. For the operating system, a device is its CPU or SoC and its attached devices such as sensors, actuators, gadgets, media peripherals and connectivity interfaces. The hardware is a critical building block to design a KOS-based system. Hardware options must be evaluated against design requirements in terms of what it provides in terms of the level of performance, the security primitives, the supported peripheral devices, the connectivity options, and the environment it will be deployed in, including whether physical device hardening is necessary.
-
Untrusted, isolatedApps + Drivers
Application isolation
-
Trusted, isolatedKOS Infrastructure
Device isolation
-
Proven integratedUndergoing formal verification KOS EngineFormally verified seL4® Microkernel
-
PhysicalHardware
-
Product detail
-
KOS Capabilities
The highest level of safety, security and resilience, without sacrificing usability
Read more -
Formal Verification
Why formally verified is better than testing
Read more -
Technical Specifications
Build certainty into an uncertain world with secure management of AI workloads.
Read more
