Dig Deeper Button
Systems Software Use Cases

Use Cases

• Enforce data diode flows between virtualized guests using the BAC, with lower space, weight, and power requirements than a hardware data diode

• Prototype stand-alone security critical components in the HaLVM environment

• Use multiple HaNS network stacks to reduce the trusted computing base in a multi-network solution

Systems Software

Replace bug-prone legacy systems with high-level language solutions.


Galois' systems software offer trusted and assured implementations of many systems components — network stacks, hypervisors, file systems, and device drivers — allowing you to step away from bugging/legacy systems components and replace them with our systems written in high-level languages. This allows us to do rapid prototyping — from network stack to a kernel without the cost of implementing up front with C.

Secure mediated access:
Block Access Controller (BAC)

Useful in streaming video, file based systems, wikis, etc., the Block Access Controller (BAC) is a mediator between clients of possibly different security levels and any kind of read/write storage (disk, FLASH, DRAM). The interface permits block reads and writes, where the reads can be from your own level, or lower levels, and writes are always to your own level. The BAC can be thought of as behaving like a software "data diode." Its design simplicity enables cost-effective high assurance solutions.

Read More >>

Eliminate the operating system and its risks:
Haskell Lightweight Virtual Machine (HaLVM)

Run your software on HaLVM, a lightweight virtual machine that is fast, efficient, and trusted. Experience cost efficiencies, eliminate bugs, extend your security, and create a smoother experience for end users by using HaLVM.

Read More >>

Design a next-generation network protocol:
Haskell Network Stack (HaNS)

HaNS is an entirely new network stack written in Haskell that can be integrated into other systems. Being high-level, it allows quick addition of components. If you are considering designing a next generation network protocol, start by using HaNS.

Read More >>

Implement high assurance solutions with a verified microkernel:
Custom L4

The L4.verified microkernel from NICTA, being commercialized by OK Labs, is the first operating system with a complete code-level proof of correctness. For critical systems, this level of correctness provides confidence beyond that possible by testing alone. Combined with Galois' capability to build high assurance software, the L4.verified microkernel enables Galois to implement solutions with higher assurance than previously possible.

Read More >>