.
This commit is contained in:
parent
2b85bfe6ed
commit
cb97397946
2 changed files with 85 additions and 4 deletions
49
About
49
About
|
|
@ -1,9 +1,52 @@
|
||||||
---
|
---
|
||||||
title: How does this work?
|
title: The concept and team
|
||||||
author: someone
|
author: someone
|
||||||
abstract: some abstract
|
abstract: some abstract
|
||||||
---
|
---
|
||||||
|
|
||||||
The concept of this endeavour.
|
# Mission
|
||||||
|
|
||||||
List of names with some background information
|
The goal of robur is to develop robust digital infrastructure. This goal is
|
||||||
|
achieved by continuous maintainence of permissively licensed (MIT/ISC/BSD) open
|
||||||
|
source libraries, which are used by various partners and supporters.
|
||||||
|
|
||||||
|
Robur is a non-profit endeavour, the ultimate goal is not to earn as much as
|
||||||
|
possible, but instead to enable more people to run their own digital
|
||||||
|
infrastructure. Minimising the executable size of services and cutting down
|
||||||
|
complexity is crucial to help people to understand the technology.
|
||||||
|
|
||||||
|
Rewards (in terms of shirts, money, stickers, retreat attendance) will be given
|
||||||
|
to contributors from the open source community.
|
||||||
|
|
||||||
|
Experience in developing and deploying the technology itself will be reflected
|
||||||
|
on in academic papers, and talks at workshops and conferences.
|
||||||
|
|
||||||
|
Transparency is another goal of robur, the annual balance will be accessible to
|
||||||
|
the public.
|
||||||
|
|
||||||
|
# Non-profit company
|
||||||
|
|
||||||
|
Supporters can make charitable donations to robur, which will be used for
|
||||||
|
further development and maintainence of software and community infrastructure.
|
||||||
|
|
||||||
|
Partners can contract robur to develop prototypes (see example
|
||||||
|
[projects](/Projects)). Developed libraries will be open sourced, and are
|
||||||
|
reusable by other interested parties. The application code itself will be
|
||||||
|
exclusively copyrighted by the partner. Some terms are negotiable, e.g.
|
||||||
|
whether the library code will be exclusively licensed to the partner for some
|
||||||
|
time (maximum 6 months), influence on the development roadmap, service level
|
||||||
|
agreements (on-call debugging, running infrastructure).
|
||||||
|
|
||||||
|
# Team
|
||||||
|
|
||||||
|
## Alfred
|
||||||
|
|
||||||
|
Alfred is a hacker. He enjoys to write code since more than 15 years, but also
|
||||||
|
travelling and repairing his recumbent bicycle, and being a barista.
|
||||||
|
|
||||||
|
In 2013, Alfred did his PhD in computer science about formal verification of
|
||||||
|
imperative code (using a higher-order separation logic and the theorem prover
|
||||||
|
Coq). At the moment he is busy with reanimating an executable formal model of
|
||||||
|
TCP/IP which can act as a test validator.
|
||||||
|
|
||||||
|
Alfred co-authored a TLS implementation from the grounds up in OCaml.
|
||||||
|
|
|
||||||
40
Technology
40
Technology
|
|
@ -4,4 +4,42 @@ author: someone
|
||||||
abstract: some abstract
|
abstract: some abstract
|
||||||
---
|
---
|
||||||
|
|
||||||
This is the site about our technology
|
We develop digital infrastructure with a small footprint. This is in stark
|
||||||
|
contrast with other approaches that try to patch general purpose operating
|
||||||
|
systems by adding more layers of indirection.
|
||||||
|
|
||||||
|
Each piece of digital infrastructure (or service) is (a) written in a high-level
|
||||||
|
memory-safe programming language and (b) specialised to only contain the
|
||||||
|
required functionality at compilation time. This (a) reduces the attack vectors
|
||||||
|
and (b) drastically reduces the attack surface.
|
||||||
|
|
||||||
|
The resulting service is executed as a virtual machine on any modern hypervisor.
|
||||||
|
Its size is usually two orders of magnitude smaller (ranging from kilobytes to
|
||||||
|
16 megabytes) than a UNIX, it boots within milliseconds.
|
||||||
|
|
||||||
|
As programming language we use [OCaml](https://ocaml.org), a multi-paradigm
|
||||||
|
programming language, which unifies functional, imperative, and object-oriented
|
||||||
|
programming. OCaml has an expressive static type system, and type inference. A
|
||||||
|
developer can specify complex invariants in the type system, which are
|
||||||
|
checked at compile time, and violations are caught early.
|
||||||
|
|
||||||
|
We discuss more reasons why we use OCaml [further down](#WhyOCaml).
|
||||||
|
|
||||||
|
## MirageOS
|
||||||
|
|
||||||
|
[MirageOS](https://mirage.io) started as a research project at the University
|
||||||
|
of Cambridge in 2009.
|
||||||
|
|
||||||
|
## Why OCaml
|
||||||
|
|
||||||
|
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
|
||||||
|
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).
|
||||||
|
|
||||||
|
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
|
||||||
|
application, since the same compiler is used.
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue