diff --git a/About b/About index 5e113eb..026e56f 100644 --- a/About +++ b/About @@ -1,9 +1,52 @@ --- -title: How does this work? +title: The concept and team author: someone 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. diff --git a/Technology b/Technology index 7d57d73..c714191 100644 --- a/Technology +++ b/Technology @@ -4,4 +4,42 @@ author: someone 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.