--- title: Technology --- We develop digital infrastructure with a minimal footprint. Where other approaches try to patch general purpose operating systems by adding more layers of indirection, we strive to build a secure system from the ground up. Each piece of digital infrastructure or service is written in a high-level memory-safe programming language and tailored to only contain the required functionality at compilation time. This reduces the attack vectors and the attack surface. The resulting service is executed as a virtual machine on a modern hypervisor. Its size is usually around 1-10 MB, much smaller than a UNIX / Linux system, and boots within milliseconds. ## MirageOS - bespoke operating systems Our work is based on MirageOS, a suite to build operating systems. It has been developed since 2009 at University of Cambridge, UK and is written in the programming language OCaml (see [Why OCaml](#Why-OCaml)). Most libraries are developed as open source (MIT/ISC/BSD2/Apache2). MirageOS is a library operating system. It composes OCaml libraries into a bespoke operating system, called a unikernel. A unikernel can be a compiled as a UNIX binary, or a standalone virtual machine image. To build the right unikernel for your custom business logic, we can pick from hundreds of libraries which implement network protocols, storage on block devices, or interfaces to network devices via the hypervisor. On top of the hypervisor, a small layer of C code unifies the interface on which OCaml runs. OCaml is a functional programming language that minimizes side effects and mutable state. Its functional programming concepts give us a list of security advantages for MirageOS. ## Running unikernel, system security Aside from automated memory management to avoid memory corruption, and type checking to avoid many common programming errors, the major advantage of functional programming is localized reasoning about program code. All inputs, outputs and effects of a function are known. Immutable datastructures and cooperative multitasking allow us to reason about the state of the entire system, even if we use parallelism and complex distributed systems. ### Simple config management model with localized reasoning There are three ways to feed a virtual machine with configuration data like network configuration or TLS certificate and key: - compile the information into the virtual machine image, which requires recompilation on configuration change - pass the information as boot parameters, which requires reboot on configuration change - store this information in a virtual block device attached to the virtual machine. For example, logs can be written from the unikernel to a syslog collector with UDP, TCP, or TLS as transport. The transport needs to be chosen at compile time because TLS requires the TLS library to be linked into the kernel image, but the log destination is passed as boot parameter. ### Simple concurrency model with localized reasoning MirageOS is an event based operating system with asynchronous tasks. A task yields the CPU once its execution is finished, or if it has to wait for IO. This concurrency model leads to a cooperative multitasking programming style, rather than the error prone preemptive multitasking, where each code block needs to make sure to use appropriate locking strategies to avoid reentrant execution errors. A recent example for code which is not safe under reentrant execution [in Ethereum](http://hackingdistributed.com/2016/06/18/analysis-of-the-dao-exploit/) lead to a huge amount of ether being stolen. Established software like the [Firefox JavaScript engine](http://www.nist.org/news.php?extend.175), or [PHP](https://bugs.php.net/bug.php?id=74308) shows similar problems on a regular basis. ### Simple process memory model with localized reasoning The virtual memory subsystem in contemporary operating systems provides an address mapping for each process. Since a unikernel is only a single service, it uses a single address space, avoiding the need for complex address mapping code altogether. [//]: # (I think we should explain the context for mentioning Xen here) An example for corrupting the page table is [Xen's XSA-182](http://xenbits.xen.org/xsa/advisory-182.html). ### Simple library model with localized reasoning A MirageOS unikernel is much smaller than a comparable UNIX virtual machine. By avoiding superfluous code we decrease the attack surface immensely. Consider the breakdown of the code of the example system [Bitcoin PiƱata](/Projects/Pinata) compared to a virtual machine using Linux and OpenSSL, measured in thousands of lines of code:
Linux | MirageOS | |
---|---|---|
Kernel | 1600 | 48 |
Runtime | 689 | 25 |
Crypto | 230 | 23 |
TLS | 41 | 6 |
Total | 2560 | 102 |