updated current text with answers from specific list

This commit is contained in:
Sol 2019-10-22 19:16:46 +02:00
parent 3a5780ab47
commit 45c94d360e
6 changed files with 16 additions and 15 deletions

View file

@ -7,8 +7,8 @@ At Robur our focus is on the software we develop. We are passionate about our wo
We get our funding through three avenues: grants for particular open-source projects, contracts for specific work including development and auditing, and public donations that help allow us to continue the work that isn't otherwise funded. We get our funding through three avenues: grants for particular open-source projects, contracts for specific work including development and auditing, and public donations that help allow us to continue the work that isn't otherwise funded.
We spend most of our funding on salaries, ensuring Robur keeps developing the software we think is important. We do not spend money on fancy parties or first class business trips. Our general breakdown of spending per year is: We spend most of our funding on salaries, ensuring Robur keeps developing the software we think is important. We do not spend money on fancy parties or first class business trips. Our general breakdown of spending per year is:
* 88% on salaries * 83% on salaries
* 2% on necessary travel * 7% on necessary travel
* 10% on inevitable administrative costs * 10% on inevitable administrative costs
If you are considering [donating](/Donate) to us, [hiring](/Our%20Work/Services) us, or [giving us a grant](/Contact) you can be assured your money will be well spent on the actual end result of delivering the robust and secure digital infrastructure we strive for. If you are considering [donating](/Donate) to us, [hiring](/Our%20Work/Services) us, or [giving us a grant](/Contact) you can be assured your money will be well spent on the actual end result of delivering the robust and secure digital infrastructure we strive for.

View file

@ -7,8 +7,11 @@ title: Network
[The Center For Technical Cultivation](https://techcultivation.org)<br /> [The Center For Technical Cultivation](https://techcultivation.org)<br />
The Center For Technical Cultivation is a "back-end provider" for the open source community. They work with Robur to assist us in our financial processes and administration. The Center For Technical Cultivation is a "back-end provider" for the open source community. They work with Robur to assist us in our financial processes and administration.
[Least Authority](https://leastauthority.com)
Least Authority is a Berlin-based group building technology that is open source and focused on allowing user freedom and privacy protection in online services. Robur has worked with Least Authority to make security audits of OCaml applications.
[MirageOS](https://mirage.io)<br /> [MirageOS](https://mirage.io)<br />
MirageOS is a library operating system that constructs unikernels for secure and high-performing applications. Most Robur projects are designed to be implemented in MirageOS, as well as other operating systems. We work closely with the MirageOS community to help develop its ecosystem and increase the availability of secure applications offered within it. MirageOS is a library operating system that constructs unikernels for secure and high-performing applications. Most Robur projects are designed to be compatible with MirageOS, as well as native operating systems, like Linux or FreeBSD. We work closely with the MirageOS community to help develop its ecosystem and increase the availability of secure applications offered within it.
[OCaml Labs](http://ocamllabs.io)<br /> [OCaml Labs](http://ocamllabs.io)<br />
OCaml Labs is an initiative within the Cambridge Computer Laboratory started by Anil Madhavapeddy in 2011 to promote research, growth and collaboration within the wider OCaml community. Robur has had a working relationship with OCaml Labs since our inception to help widen the base of OCaml users and applications. OCaml Labs is an initiative within the Cambridge Computer Laboratory started by Anil Madhavapeddy in 2011 to promote research, growth and collaboration within the wider OCaml community. Robur has had a working relationship with OCaml Labs since our inception to help widen the base of OCaml users and applications.

View file

@ -2,6 +2,7 @@
title: Team title: Team
--- ---
Robur is a software development cooperative specializing in robust and secure digital infrastructure written in OCaml.
### Stefanie ### Stefanie

View file

@ -28,14 +28,11 @@ The software is available [on Github](https://github.com/cfcs/ocaml-openpgp).
# Solo5 # Solo5
Solo5 is a sandboxed (separated) execution environment built using unikernels (a.k.a. library operating systems), including but not limited to MirageOS unikernels. It provides the interface between software and the operating system it runs on. Solo5 is a sandboxed (separated) execution environment built using unikernels (a.k.a. library operating systems), including but not limited to MirageOS unikernels. Conceptually it provides a common interface between the unikernel and various host operating systems or hypervisors.
Conceptually, Solo5 provides the minimal set of "low level" building blocks and interfaces that a unikernel hosted on an operating system or hypervisor requires to be able to perform useful work.
Solo5's interfaces are designed in a way that allows us to easily port them to run on different host operating systems or hypervisors. Implementations of Solo5 run on Linux, FreeBSD, OpenBSD, the Muen Separation Kernel and the Genode Operating System Framework. Solo5's interfaces are designed in a way that allows us to easily port them to run on different host operating systems or hypervisors. Implementations of Solo5 run on Linux, FreeBSD, OpenBSD, the Muen Separation Kernel and the Genode Operating System Framework.
Currently Solo5 is ready for use by early adopters and we plan to continue developing it further, if you are interested in supporting this development with a [donation](/Donate) or want to hear more about the project please [get in touch with us](/Contact).
@ -54,7 +51,7 @@ Solo5 has been designed to isolate the unikernel as much as possible from its ho
Compared to existing technologies, such as traditional virtualization using KVM/QEMU, VMWare, crosvm and so on, Solo5 is several orders of magnitude smaller (around 10,000 lines of C) and is tailored to running unikernels in a legacy-free and minimalist fashion. Compared to existing technologies, such as traditional virtualization using KVM/QEMU, VMWare, crosvm and so on, Solo5 is several orders of magnitude smaller (around 10,000 lines of C) and is tailored to running unikernels in a legacy-free and minimalist fashion.
Our goal for Solo5 is to enable the use of unikernel technology to build hybrid, disaggregated systems where the designer/developer can choose which components are untrusted or security-sensitive and "split them out" from the monolithic host system. At the same time she can continue to use existing, familiar, technology as the base or "control plane" for the overall system design/deployment, or mix and match traditional applications and unikernels as appropriate. Our goal for Solo5 is to enable the use of unikernel technology to build hybrid, disaggregated systems where the designer/developer can choose which components are untrusted or security-sensitive and "split them out" from the monolithic host system. At the same time the developer can continue to use existing, familiar, technology as the base or "control plane" for the overall system design/deployment, or mix and match traditional applications and unikernels as appropriate.

View file

@ -16,7 +16,7 @@ BOB 2018 - [Engineering TCP/IP with logic](https://www.youtube.com/watch?v=AYDws
Presents a formal model of TCP/IP (developed 2000-2009 and refurbished since 2016), how it can be used to validate the FreeBSD TCP/IP stack, and what was learned while writing it. It is modeled as a label transition system, including timers, re-transmission, etc. Presents a formal model of TCP/IP (developed 2000-2009 and refurbished since 2016), how it can be used to validate the FreeBSD TCP/IP stack, and what was learned while writing it. It is modeled as a label transition system, including timers, re-transmission, etc.
BornHack 2018 - [MirageOS: what did we achieve in the last year?](https://www.youtube.com/watch?v=QtPUCC6KaWo)<br /> BornHack 2018 - [MirageOS: what did we achieve in the last year?](https://www.youtube.com/watch?v=QtPUCC6KaWo)<br />
This is a continuation of earlier talks at Bornhack (2016, 2017), and goes into detail of some active projects, such as: community repository signing (for secure updates), DNS infrastructure, our Prototype Fund sponsored CalDAV-server. This is a continuation of earlier talks at BornHack (2016, 2017), and goes into detail of some active projects, such as: community repository signing (for secure updates), DNS infrastructure, our Prototype Fund sponsored CalDAV-server.
Chaos Computer Club Congress 2018 - [Domain Name System](https://www.youtube.com/watch?v=I7060fqa-B8)<br /> Chaos Computer Club Congress 2018 - [Domain Name System](https://www.youtube.com/watch?v=I7060fqa-B8)<br />
Discusses the basic usage of DNS, including stub and recursive resolver, server; various protocol extensions including zone transfer, dynamic updates, authentication, notifications; privacy extensions (query path minimization, DNS-over-TLS); provisioning let's encrypt certificates; and attacks (poisoning, amplification). Explains the Robur implementation of DNS with above mentioned extensions as minimized MirageOS unikernels. Discusses the basic usage of DNS, including stub and recursive resolver, server; various protocol extensions including zone transfer, dynamic updates, authentication, notifications; privacy extensions (query path minimization, DNS-over-TLS); provisioning let's encrypt certificates; and attacks (poisoning, amplification). Explains the Robur implementation of DNS with above mentioned extensions as minimized MirageOS unikernels.
@ -34,7 +34,7 @@ Discusses the basic usage of DNS, including stub and recursive resolver, server;
### Talks: ### Talks:
FOSDEM 2019 - [Solo5: A sandboxed, re-targetable execution environment for unikernels](https://www.youtube.com/watch?v=VO6f7uSs3-I)<br /> FOSDEM 2019 - [Solo5: A sandboxed, re-targetable execution environment for unikernels](https://archive.fosdem.org/2019/schedule/event/solo5_unikernels/)<br />
Explains Solo5 which is a microkernel-friendly, sandboxed, re-targetable execution environment for unikernels, with a taste for minimalism. Presents the interfaces it offers to the unikernel/library operating system/application developer. Using existing library operating systems, such as MirageOS, demonstrates the developer experience for various Solo5 targets, going on to show how rigorously applying minimalist principles to interface design is used to our advantage, blurring traditional lines between unikernels, processes, kernels and hypervisors. Explains Solo5 which is a microkernel-friendly, sandboxed, re-targetable execution environment for unikernels, with a taste for minimalism. Presents the interfaces it offers to the unikernel/library operating system/application developer. Using existing library operating systems, such as MirageOS, demonstrates the developer experience for various Solo5 targets, going on to show how rigorously applying minimalist principles to interface design is used to our advantage, blurring traditional lines between unikernels, processes, kernels and hypervisors.
### Publications: ### Publications:

View file

@ -31,7 +31,7 @@ MirageOS unikernels are clean slate operating systems, not POSIX compatible, tha
These unikernels can be a compiled natively as UNIX processes (with a size of about 4% of a UNIX based system), allowing for testing and debugging in a UNIX environment, and can then be deployed as a standalone virtual machine on a cloud service or hypervisor. On top of the hypervisor, a small layer of C code unifies the interface on which OCaml runs but there is no need to carry the whole C library. These unikernels can be a compiled natively as UNIX processes (with a size of about 4% of a UNIX based system), allowing for testing and debugging in a UNIX environment, and can then be deployed as a standalone virtual machine on a cloud service or hypervisor. On top of the hypervisor, a small layer of C code unifies the interface on which OCaml runs but there is no need to carry the whole C library.
MirageOS targets several platforms: Xen, KVM on linux, Bhyve on FreeBSD, VMM on OpenBSD, VKM via Solo5, UNIX, macosx, virtio, ukvm, the Muen Separation Kernel and Qubes. With regards to hardware processors MirageOS compiles to native code on ARM32, ARM64, x86 and x86_64. MirageOS targets "standard" UNIX processes, Xen, Qubes, and Solo5 (which in turn [supports numerous targets](https://github.com/Solo5/solo5/blob/master/docs/building.md#supported-targets)). With regards to hardware processors MirageOS compiles to native code on ARM64, x86 and x86_64.
There are generally three ways to feed the virtual machine with configuration data, like network configuration or TLS certificate and key: There are generally three ways to feed the virtual machine with configuration data, like network configuration or TLS certificate and key:
@ -39,7 +39,7 @@ There are generally three ways to feed the virtual machine with configuration da
* pass the information as boot parameters, which requires reboot on configuration change * pass the information as boot parameters, which requires reboot on configuration change
* store this information in a virtual block device attached to the virtual machine. * store this information in a virtual block device attached to the virtual machine.
In MirageOS we use a simple configuration management model with localized reasoning. 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. We use unified logging throughout via syslog. In MirageOS we use a simple declarative configuration management model with localized reasoning. 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. We use unified logging throughout via syslog.
A task yields the CPU once at regular intervals throughout its execution, for example when waiting for I/O, or for other tasks to perform work upon which the task depends. This concurrency model leads to a cooperative multitasking programming style, rather than the error prone preemptive multitasking, where each code block needs to make sure to use appropriate locking strategies to avoid re-entrant execution errors. A task yields the CPU once at regular intervals throughout its execution, for example when waiting for I/O, or for other tasks to perform work upon which the task depends. This concurrency model leads to a cooperative multitasking programming style, rather than the error prone preemptive multitasking, where each code block needs to make sure to use appropriate locking strategies to avoid re-entrant execution errors.
@ -49,7 +49,7 @@ A number of protocols have already been implemented in MirageOS, with more each
Currently supported protocols, all written from scratch in OCaml, include: HTTP, DNS, DHCP (server and client), BGP, TCP/IP, IPv4, git, TLS, Lets Encrypt, OpenPGP, Prometheus, SNMP, SSH, OTR and syslog. We also have some visualizations including some terminal based UIs, a firewall, VPN and a crypto library. Currently supported protocols, all written from scratch in OCaml, include: HTTP, DNS, DHCP (server and client), BGP, TCP/IP, IPv4, git, TLS, Lets Encrypt, OpenPGP, Prometheus, SNMP, SSH, OTR and syslog. We also have some visualizations including some terminal based UIs, a firewall, VPN and a crypto library.
As some examples of the comparable code base sizes of these protocol implementations and applications our TLS library, which is inter-operable with most stacks, has a code base of roughly 4% of other implementations. We have had an authoritative name service running consistently since XX which is only a 2MB VM image, and our firewall has been used in Qubes and instead of a 200MB VM it is max 50MB. As some examples of the comparable code base sizes of these protocol implementations and applications our TLS library, which is inter-operable with most stacks, has a code base of roughly 4% of other implementations. We have had an authoritative name service running consistently since December 2016 which is only a 2MB VM image, and our firewall has been used in Qubes and instead of a 200MB VM it is max 50MB.
<br /> <br />
@ -80,7 +80,7 @@ It is a memory safe language so the behavior of our core protocol logic is only
A major advantage of functional programming is localized reasoning about program code. All inputs, outputs and effects of a function are known. Immutable data structures and cooperative multitasking allow us to reason about the state of the entire system, even if we use parallelism and complex distributed systems. A major advantage of functional programming is localized reasoning about program code. All inputs, outputs and effects of a function are known. Immutable data structures and cooperative multitasking allow us to reason about the state of the entire system, even if we use parallelism and complex distributed systems.
OCaml lends itself by default to a programming style with explicit error handling, like using an error monad, result type, and no exceptions. OCaml provides for isolated side effects like timers, IO and mutable state which is then giving an effectful layer on top of the pure protocol logic for the side effects. OCaml lends itself by default to a programming style with explicit error handling. OCaml provides for isolated side effects like timers, IO and mutable state which is then giving an effectful layer on top of the pure protocol logic for the side effects. OCaml does supports exceptions, but they are not present in the type signatures \[of functions] (unlike Java), and thus from the outside (e.g. when calling a function), it is not clear whether exceptions can be raised or not. For that reason, the coding style of exception-based error handling is avoided in MirageOS. Instead of relying on exceptions, we employ explicit error handling using result types and an error monad.
### Verification ### Verification