Skip to content
hello@kry10.com

Contact

hello@kry10.com

Formal Verification

Built on mathematically proven foundations

Find out why Kry10 builds on a formally verified foundation.

Request a KOS evaluation license

Tested Software

Testing can only tell you about the situations that someone thought to test

Almost all software today is trusted because it's been tested. It’s been run many times, in many conditions, and it seems to work. This approach is a reasonable way to build confidence, but it has its limitations. Testing can only tell you about the situations that someone thought to test.

Proven Software

There's a second, stronger way to establish trust: proof

Remember Pythagoras's theorem from school? Where a² + b² = c². Nobody had to test every possible triangle to know the rule always holds, because it's proven true for all of them, not just the triangles someone happened to check. 

With formal verification, we can apply that same idea to software. Instead of testing a sample set of situations and hoping nothing was missed, formal verification mathematically proves that a given property is true in every situation. 

WHAT ARE FORMAL METHODS?

Formal methods are mathematical techniques used to prove that software will behave as specified. Instead of sampling inputs the way testing does, a machine-checked proof shows that an implementation conforms to its specification and cannot diverge from it.

A proven foundation

Because some responsibilities are too important to trust to probability

The distinction between ‘tested’ and ‘proven’ is the whole idea behind KOS. Most operating systems, including the ones running critical infrastructure today, are in the first category — TESTED. KOS is built on a foundation in the second category — PROVEN. 

This means whole classes of vulnerabilities cannot exist within KOS's foundation.

What’s proven and what isn't

Click on a section for more information

  1. seL4® is formally verified right now

    At the base of KOS is the seL4® microkernel. This microkernel is stripped to its essential functions, managing memory, running processes, and handling communication between them, implemented in roughly 10,000 lines of code.

    A conventional monolithic kernel like Linux runs tens of millions of lines of code in privileged mode. With seL4® 's much smaller footprint, there is a much smaller attack surface, before proof is even considered.

    What makes seL4® different is that its implementation has a machine-checked mathematical proof that it behaves exactly according to a formal specification. In addition, seL4® has proofs that the specification itself provides the isolation properties, confidentiality and integrity, needed to build secure systems on top of it. Access to memory, threads, CPU time, and inter-process communication is governed by fine-grained, capability-based access control. The access-control behavior is also part of what's been proven.

    The result is that whole categories of vulnerability, buffer overflows, memory corruption, privilege escalation, undefined behavior, are ruled out in the kernel by proof, not reduced in likelihood by testing. Whether or not a fuzzer or a red team could find such a flaw in the kernel is irrelevant because the whole category of flaw has been provably eliminated from the code.

  2. The KOS engine's formal verification is in progress

    Kry10 is currently formally verifying the KOS components that configure the system, run the updates and enforce communication.

    Application code, optional drivers, microVM workloads and Linux-side code in containers will not be verified. Verification stops at the trusted boundary our client determines, and KOS gives the means to enforce that boundary.

  3. Your applications benefit even without formal verification

    Verification stops at the trusted boundary you architect and KOS gives you the means to enforce that boundary. This is not a guarantee that everything inside it is proven.

    Because the foundation is verified, a compromised or buggy driver can’t escape its bounds and interfere with the kernel or other components isolated through partitions. Your system is safer whether you formally verify your applications or not

    The same discipline applies to AI workloads. For example, KOS provides a verified sandbox for a model. The model itself is not formally verified, but the container it runs in is.

Get Started

Request a KOS Evaluation License

Get in touch