robur/homepage-data
4
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

rearrange ocaml.

Browse source
This commit is contained in:
linse 2017-09-16 18:47:55 -04:00
parent 86930814e0
commit d898c14694
1 changed files with 34 additions and 51 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

85
Technology
View file

@ -102,43 +102,25 @@ to a virtual machine using Linux and OpenSSL, measured in thousands of lines of
<tr><td>Total</td><td>2560</td><td>102</td></tr>
</table>
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