diff --git a/Technology b/Technology index e3cc206..da01a16 100644 --- a/Technology +++ b/Technology @@ -33,53 +33,8 @@ via the hypervisor. On top of the hypervisor, a small layer of C code unifies the interface on which OCaml runs. -## 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. - -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. - -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 -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. +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. ## MirageOS: Running a unikernel & system security @@ -143,6 +98,52 @@ TODO: For example .. ## 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. + +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. + +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 +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