diff --git a/Technology b/Technology index 074529b..33f082b 100644 --- a/Technology +++ b/Technology @@ -102,43 +102,25 @@ to a virtual machine using Linux and OpenSSL, measured in thousands of lines of Total2560102 -By minimising each unikernel to its minimal footprint, -security breaches are contained to the information the unikernel contains. - ### Secure updates -If a security flaw is found in a library, and the library gets a security update, +If a security flaw is discovered in a library, and the library gets a security update, all unikernels depending on this library need to be updated as well. This can be done with the OCaml package manager. It resolves dependencies and lets authors sign their releases, so there is no need for a central package repository server. -These servers are known targets for attackers. -Various servers hosting open source software have been breached, amongst them -are [Linux kernel](https://lwn.net/Articles/57135/), [FreeBSD +Central repository servers are known targets for attackers and have been breached in the past, amongst them +the [Linux kernel](https://lwn.net/Articles/57135/), [FreeBSD infrastructure](https://www.freebsd.org/news/2012-compromise.html), -[Debian](https://www.debian.org/News/2003/20031202), -[php](http://php.net/archive/2013.php#id2013-10-24-2). - -TODO: For example .. +[Debian](https://www.debian.org/News/2003/20031202) and +[PHP](http://php.net/archive/2013.php#id2013-10-24-2). ## Why OCaml -OCaml is a functional programming language with automated memory management, -preventing manual memory management errors. The strong and expressive type -system of OCaml catches most programming errors already at compile time. We use -a declarative style with immutable data structures and memory to avoid side -effects that are hard to reason about. Errors are expressed as part of the type -signature. IO is contained on top of the protocol logic. An implementation of a -protocol can be used both as executable code, and as a test oracle. +### Functional programming style -Most security problems for network services arise in parsers of received network -data. OCaml allows us to write strict parsers, which return success and error -on the type system level to ensure that the caller handles all cases. If a -parser contains an error, in our system the impact is local, it cannot access -memory beyond the the network data. Errors in parsers written in unsafe -languages often lead to buffer overflows, which can lead to remote code -execution. +### Performance OCaml code is compiled to native code running in the OCaml runtime, which is very performant, on par with C++ code. The OCaml runtime is just used for @@ -146,32 +128,6 @@ memory management, and very small compared to a JVM or Python runtime. As example, our TLS library has up to 85% of the bulk throughput of OpenSSL (using 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). - -### Module system & Compilation - -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 -powerful abstraction mechanism to adapt the unikernel to the compilation target. -It defines modules for all operating system services, such as the console, the -network stack, the random number generator. For each service, an implementation -can be provided depending on the compilation target (UNIX process or virtual -machine). On UNIX, the sockets API is used as the networking stack. On a -virtual machine, the TCP/IP stack in OCaml is being used. - -By leveraging the module system of OCaml for MirageOS, we get module separation -and dependency analysis from the well-tested module system of OCaml and avoid -reimplementing these error-prone and important parts. A MirageOS unikernel -developer does not need to reason about compilation targets, just about the -module interface. - -TODO: OCaml runtime vom franz. BSI reviewed, solo5 noch kein wirkliches review - OCaml code can be very fast (our TLS implementation reaches up to 85% of the throughput of OpenSSL), and compiles either to native code on various architectures or to bytecode. It can even compile to JavaScript. OCaml is @@ -179,6 +135,33 @@ memory managed, individual developers don't have to manually allocate and release memory (which is a common source of security issues in other operating systems). + +### Dependency management + +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 to adapt the unikernel to the compilation target. +It defines modules for all operating system services, such as the console, the +network stack, the random number generator. For each service, an implementation +can be provided depending on the compilation target (UNIX process or virtual +machine). On UNIX, the sockets API is used as the networking stack. On a +virtual machine, the TCP/IP stack in OCaml is being used. + +A MirageOS developer does not need to reason about compilation targets, just about the +module interface. + +### Security reviews + +TODO: OCaml runtime vom franz. BSI reviewed, solo5 noch kein wirkliches review + +### Modern dialects and compile targets + +OCaml is known as a mature programming language that is used in both +industry (facebook for compilers, jane street for trading, docker, ahrefs, +simcorp, lexifi) and academia (coq, compcert). + In 2016, Facebook developed [reason](https://reasonml.github.io/), a dialect of OCaml which syntax is closer to JavaScript, and easier to comprehend for beginners. Reason and OCaml code can be easily combined in a single