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

Technology: Move Ocaml down.

Browse source
This commit is contained in:
linse 2017-09-16 15:06:49 -04:00
parent 022be8cf94
commit f723ab2f59
1 changed files with 48 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

95
Technology
View file

@ -33,53 +33,8 @@ via the hypervisor.
On top of the hypervisor, a small layer of C code unifies On top of the hypervisor, a small layer of C code unifies
the interface on which OCaml runs. the interface on which OCaml runs.
## OCaml 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.
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.
## MirageOS: Running a unikernel & system security ## MirageOS: Running a unikernel & system security
@ -143,6 +98,52 @@ TODO: For example ..
## Why OCaml ## 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 TODO: OCaml runtime vom franz. BSI reviewed, solo5 noch kein wirkliches review
OCaml code can be very fast (our TLS implementation reaches up to OCaml code can be very fast (our TLS implementation reaches up to