Some changes.

This commit is contained in:
linse 2017-09-16 14:01:54 -04:00
parent becd9cddd3
commit 9118b907c8

View file

@ -1,35 +1,35 @@
---
title: Technology behind robur
title: Technology
author: someone
abstract: some abstract
---
We develop digital infrastructure with a small footprint. This is in stark
contrast with other approaches that try to patch general purpose operating
systems by adding more layers of indirection.
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 (a) written in a high-level
Each piece of digital infrastructure or service is (a) written in a high-level
memory-safe programming language and (b) specialised to only contain the
required functionality at compilation time. This (a) reduces the attack vectors
and (b) drastically reduces the attack surface.
and (b) also reduces the attack surface.
The resulting service is executed as a virtual machine on any modern hypervisor.
The resulting service is executed as a virtual machine on a modern hypervisor.
Its size is usually two orders of magnitude smaller (ranging from kilobytes to
16 megabytes) than a UNIX, it boots within milliseconds.
16 megabytes) than a UNIX / Linux system, and boots within milliseconds.
As programming language we use [OCaml](https://ocaml.org), a multi-paradigm
We program in [OCaml](https://ocaml.org), a multi-paradigm
programming language, which unifies functional, imperative, and object-oriented
programming. OCaml has an expressive static type system, and type inference. A
developer can specify complex invariants in the type system, which are
programming. OCaml has an expressive static type system with type inference.
Developers can specify complex invariants in the type system, which are
checked at compile time, and violations are caught early.
We discuss more reasons why we use OCaml [further down](#Why-OCaml).
## MirageOS
## MirageOS - bespoke operating systems
Our work is based on MirageOS, a suite to develop operating systems (developed
since 2009 at University of Cambridge, UK) written in the programming language
OCaml (developed since 1996 at INRIA in Paris, France). Most libraries are
Our work is based on MirageOS, a suite to develop operating systems. It has been developed
since 2009 at University of Cambridge, UK and is written in the programming language
OCaml, developed since 1996 at INRIA in Paris, France. Most libraries are
developed under permissive licenses (MIT/ISC/BSD2/Apache2). The OCaml compiler
is dual-licensed: LGPLv2 or BSD for consortium members (3000 EUR/year).
@ -69,11 +69,11 @@ AES128-CBC). The TLS handshake performance is equal with OpenSSL.
TODO: OBWOHL AUF BESTIMMTE KONTEXTE BESCHRAENKT/NICHT ALLERWELTSPRACHE DA LERNINTENSIV?
OCaml is known as a mature and safe programming language that is used in both
industry (facebook for compilers, jane street for trading, docker, ahrefs,
simcorp, lexifi) and academia (coq, compcert, ...).
simcorp, lexifi) and academia (coq, compcert).
### Module system & Compilation
OCaml has a unique module system, in which a module specifies abstract datatypes
OCaml has a unique module system. A module specifies abstract datatypes
and functions, and each module can have multiple implementations. Modules can
take other modules as parameters, the module system is a complete programming
language, evaluated at compile time. MirageOS uses this module system as a
@ -196,10 +196,10 @@ support for capabilities).
OCaml can be compiled to JavaScript, which means projects can developed in a
single language to ensure consistency and avoid errors, but code can be executed
on the client, or on the server.
on the client or on the server.
The idea of unikernels is not limited to MirageOS, other projects apply the same
methodology in different programming languages. HalVM - the Haskell ligthweight
concept in different programming languages. HalVM - the Haskell ligthweight
virtual machine - was developed by Galois Inc., and is based on Haskell. It is
used for network services such as honeypots and secure IPSec gateways.