diff --git a/Technology b/Technology index da01a16..6829aa2 100644 --- a/Technology +++ b/Technology @@ -36,7 +36,13 @@ 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. -## MirageOS: Running a unikernel & system security +## Running a 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 @@ -49,10 +55,10 @@ network configuration or TLS certificate and key. - Store this information in a virtual block device which is attached to the virtual machine. -For example, logs can be exfiltrated using syslog with UDP, TCP, or TLS as -transport. The transport to use has to be chosen at compile time because TLS -requires the TLS library to be linked in, but the log destination can be passed -as boot parameter to the unikernel. +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 @@ -60,7 +66,7 @@ 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 be hardened to allow reentrant execution. +to make sure to use appropriate locking strategies, to avoid reentrant execution errors. TODO: For example ..