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

Loeschdiskussion.

Browse source
This commit is contained in:
linse 2017-09-16 19:29:53 -04:00
parent fb7e820e4d
commit ebc2dff0b6
1 changed files with 3 additions and 72 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

75
Technology
View file

@ -104,7 +104,7 @@ to a virtual machine using Linux and OpenSSL, measured in thousands of lines of
### Secure updates
If a security flaw is discovered in a library, and the library gets a security update,
If a security flaw is discovered in a library, and there is 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,
@ -154,7 +154,7 @@ direction is also possible: OCaml code can be translated into Coq definitions
The National Cybersecurity Agency of France reviewed the implementation of the
OCaml runtime system, [their
report](http://www.ssi.gouv.fr/agence/publication/lafosec-securite-et-langages-fonctionnels/)
altered some language modifications, such as that strings are no longer mutable.
prompted some language modifications, such as that strings are no longer mutable.
### Modern dialects and compile targets
@ -167,74 +167,5 @@ OCaml which syntax is closer to JavaScript, and easier to comprehend for
beginners. Reason and OCaml code can be easily combined in a single
application, since the same compiler is used.
More literature on why OCaml is a good choice in the modern world has been
More literature on why OCaml is a good choice has been
written by Yaron Minsky (Jane Street) in the article [OCaml for the masses](http://queue.acm.org/detail.cfm?id=2038036), and more recently by the crypto-ledger [tezos](https://www.tezos.com/static/papers/position_paper.pdf).
## Current state and future directions
Many libraries developed in the MirageOS project are deployed by Docker for Mac
and Docker for Windows, which have more than 100000 active users.
Available libraries include an IPv4 stack (TCP, UDP, ARP), DHCP client and
server, DNS server and resolver (both recursive and forwarding), HTTP (including
webmachine for request routing, and sessions), syslog, git (both client and
server, with mutliple storage backends: block device, in-memory), prometheus
integration. A TLS library, including random number generator (Fortuna),
cryptographic primitives (RSA, DSA, DH, AES), X.509 (using ASN.1), was developed
3 years ago and is in production serving websites, plus some applications using
the client side. A prototype implementation for managing unikernels on the host
system is already deployed and actively used, similar to libvirt, but with a
minimised code base, and written in OCaml. Monitoring is done with
prometheus. <- TODO: das bedeutet structured data und cloud ready / scalable /
funktioniert in distributed system?
More libraries are under active development, this includes an OpenPGP
implementation, an ssh implementation, structured syslog, Cap'n proto (RPC with
support for capabilities).
OCaml can be compiled to JavaScript, which means projects can developed in a
single language to ensure consistency and avoid errors, but code can be executed
on the client or on the server.
The idea of unikernels is not limited to MirageOS, other projects apply the same
concept in different programming languages. HalVM - the Haskell ligthweight
virtual machine - was developed by Galois Inc., and is based on Haskell. It is
used for network services such as honeypots and secure IPSec gateways.
IncludeOS is a C++ based unikernel which was initially developed at University
of Oslo, and now further developed in a startup.
Other unikernels are listed on
[Wikipedia](https://en.wikipedia.org/wiki/Unikernel) and there is an exchange of
ideas between different approaches. Among all unikernels, MirageOS has been
around the longest, has the most libraries available and deployed to production,
has an active developer community, and the safe programming language makes it
suitable for secure systems.
MirageOS has a small trusted code base compared to other operating systems.
Apart from the CPU (and its virtualisation extensions, VT-x, VT-d, EPT), and the
hypervisor implementation.Dieser satzkein verb On top of the hypervisor in the
host system a tiny virtual machine monitor (solo5) is executed. It does not rely
on qemu or other emulation code, but only contains drivers needed for the actual
unikernel (block and network devices). The unikernel itself consists of roughly
2000 lines of C code with basic functions such as malloc, memcopy, memcmp, on
which the vanilla OCaml runtime is executed. On top of that, only OCaml code is
executed, which includes an asynchronous task engine, the mentioned TCP/IP
stack, and the concrete services.
TODO: vllt bullet points rausnehmen, eher das formal verification argument detailliert erklaeren?
The security of MirageOS unikernels is planned to be improved even more in
several areas:
- data segments will be be mapped read/write, code segments execute-only
- private key material will be zeroed before destruction
- the address space layout will be randomised to make exploitation harder
- MirageOS will be ported to (se)L4 as hypervisor to minimize the trusted code
running on the host system
- once open hardware (RISC-V) is widely available, MirageOS will use this as
target. There is already a RISC-V backend for OCaml
- OCaml will be compilable to Coq (an interactive theorem prover) definitions,
within which theorems about the code can be proven
- Coq code will also be extractable to OCaml.