From 9118b907c85f3cfc6b4aa1d69aad5f8a1a506ca3 Mon Sep 17 00:00:00 2001 From: linse Date: Sat, 16 Sep 2017 14:01:54 -0400 Subject: [PATCH] Some changes. --- Technology | 38 +++++++++++++++++++------------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/Technology b/Technology index 4d8ccd2..18b8135 100644 --- a/Technology +++ b/Technology @@ -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.