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

new text for website!

Browse source
This commit is contained in:
Sol 2019-09-10 21:40:14 +02:00
parent 8959855424
commit ef125dbfe4
24 changed files with 450 additions and 680 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

0
static/0CBFC7AA.txt → 0CBFC7AA.txt
View file

130
About
View file

@ -1,130 +0,0 @@
---
title: Concept and team
---
Our mission is to develop robust digital infrastructure. We achieve this goal
by continuous maintenance of permissively licensed (MIT/ISC/BSD) open
source libraries, which are used by various partners and supporters.
We strive 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, hardware, retreats) for contributors of the open source community are part of the funding plan. Academic papers and talks at workshops and technical conferences will be written to document the development and deployment of the technology. The annual balance will be opened for the public to satisfy transparency what donations and funding is used for.)
### Non-profit company
Robur, a programmer cooperative, is part of the [Center for the Cultivation of
Technology](https://techcultivation.org), a German charitable non-profit company.
Our budget stems from three pillars: donations from supporters, grants, and
commercial contracts (features or products). For our mission, it is crucial
that all our developed libraries are permissively licensed and open source.
Supporters can make [donations](/Donate) to robur, which will be used for further
development and maintainence of software and community infrastructure.
Various foundations, research councils, countries, have grants for open source
projects which improve the current state of digital technology. We keep an eye
on these, and apply where appropriate. If you want to partner up with a
specific proposal, let us know.
Companies can contract robur to develop prototypes (see example
[projects](/Projects)). Developed libraries are open sourced under a
permissive license, to be reusable by other interested parties.
The application code itself can be exclusively owned by the funding partner.
Examples include branding, configuration and the concrete composition of libraries.
Negotiable terms include time-limited exclusively licenses, service level
agreements (on-call troubleshooting, running infrastructure, updates), early
access on new development, influencing on the development roadmap.
#### 2018
We start our endeavour in 2018. Our budget consists at the moment of 6 bitcoin
converted to € and [prototypefund](https://prototypefund.de/project/robur-io/).
We are still looking for funding. 2018 will be our first year, starting with a
team of three, hopefully five at the end of the year.
### Team
#### Eva
Eva is an infrastructure software engineer and a researcher.
She studied Applied Computer Science in the Natural Sciences, and developed a typechecker for a compiler of a language for optimization problems. In her PhD project she developed metrics to compare forest data structures, with an application in molecular structure comparison. Working as a postdoc in cancer research on molecular structure prediction, she found her way to Brooklyn and Berlin.
In the US tech industry, she works on infrastructure problems with distributed systems on a large scale with millions of users, developing API infrastructure and search infrastructure, with a focus on stateless systems.
Her Erdős number is 4.
#### Hannes
Hannes enjoys living in Berlin, Germany. Until end of 2017, he used to be a research
associate at the University of Cambridge in the [rems](https://rems.io) project.
He enjoys to write code, and also travelling and repairing his recumbent
bicycle, and being a barista.
Hannes did his PhD in computer science about [formal verification of imperative
code](https://itu.dk/research/tomeso/) (using a higher-order separation logic
and the theorem prover Coq). Hannes co-authored [not-quite-so-broken
TLS](https://nqsb.io), a TLS implementation from the grounds up in OCaml, and
contributes to the MirageOS project as a core team member. He is working on
various projects, including opam signing and
[netsem](https://www.cl.cam.ac.uk/~pes20/Netsem/), an executable formal model of
TCP/IP which can act as a test validator.
#### Martin
[Martin](https://lucina.net/) has been programming since before programming was
trendy, eating [Sharp SC61860A](https://en.wikipedia.org/wiki/Sharp_PC-1350)
machine code for breakfast since before it was healthy, and using Linux way
back when it was just Linus Torvalds’ glorified terminal emulator.
A founding member of Unikernel Systems (later acquired by Docker), Martin has
been involved in a number of library operating system projects since 2014,
including the [rumprun](http://repo.rumpkernel.org/rumprun) unikernel and
[MirageOS](https://mirage.io/). He is a co-author of
[Solo5](https://github.com/Solo5/solo5), a secure execution environment for
unikernels, and joins robur in 2018 to continue his work towards creating
secure software that “just works” and other ambitious projects.
Martin lives with his family in Bratislava, Slovakia and in his spare time
enjoys hiking, yachting and the arts.
#### Mindy
[Mindy](https://somerandomidiot.com) ran the first MirageOS unikernel in the
public cloud in 2014. Mindy has worked extensively on the MirageOS TCP/IP
network stack and various protocol implementations, and is a member of the
project's core team. She managed the release of MirageOS's
[latest major version](https://mirage.io/blog/announcing-mirage-30-release).
Mindy is interested in freeing software from unnecessary dependencies, including
monolithic kernels. While she finds testing and bug-fixing rewarding, her true
goal is to apply techniques that remove entire bug classes to broader classes of
computation. Memory safety isn't just for application code!
In her free time, Mindy enjoys bothering cats, playing board games, riding
bicycles, and embroidery. She lives in beautiful Madison, Wisconsin
in the United States.
#### Paul
Paul is an independent IT consultant located in Copenhagen.
Paul has a background in penetration testing, protocol design, applied
cryptography, and architectural IT security system design for customers in
especially the banking, insurance, and pension fund sectors. He has been
consulting on [BPAY integration](https://en.wikipedia.org/wiki/BPAY) in
Australia, and conducting web and network security assessments for customers
throughout the world.
Lately he has spent the last three years writing OCaml and has been working with
IT security, dev-ops and automated deployment for customers specializing in
Enterprise Resource Planning, Internet of Things, and medical technology.
In his spare time he dabbles in research into similar topics and serialization
frameworks, in addition to the enjoyable pursuit of tabletop roleplaying and
social interactions in smokey pubs - two disciplines that he excels in, but that
have somehow not been of particular interest to paying customers (yet).

14
About Us/Funding Normal file
View file

@ -0,0 +1,14 @@
---
title: Funding
---
At Robur our focus is on the software we develop. We are passionate about our work and believe in the importance of creating and maintaining secure digital infrastructure.
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:
* 88% on salaries
* 2% on necessary travel
* 10% on inevitable administrative costs
If you are considering [donating](/Donate) to us, [hiring](/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.

33
About Us/Network Normal file
View file

@ -0,0 +1,33 @@
---
title: Network
---
# Collaborations {#Collaborations}
[The Center For Technical Cultivation](https://techcultivation.org)
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)
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.
[OCaml Labs](http://ocamllabs.io)
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.
[Tarides](https://tarides.com)
Is a for-profit distributed engineering team based in Paris and Cambridge that makes software for MirageOS. Robur works alongside Tarides to expand the MirageOS ecosystem and collaborate on some projects.
<br>
# Grant Funders {#Grant-Funders}
[NLnet Foundation](https://nlnet.nl)
In 2019 NLnet Foundation granted Robur funding to develop a secure DNS resolver in OCaml. NLnet is a Dutch foundation that receives money from donations, legacies and collaborative funding and sub-granting mechanisms after starting with substantial capital established by pioneers of the European internet in 1997. It grants money to organizations and people that contribute to an open information society and secure internet projects.
[The Prototype Fund](https://prototypefund.de/en)
The Prototype Fund has awarded Robur several grants for various projects such as the [CalDAV Server](/Projects#CalDAV), the [Mirage Firewall](/Projects#Mirage-Firewall) and our OCaml implementation of an [OpenVPN Client](/Projects#OpenVPN). The Prototype Fund is a funding program of the Federal Ministry of Education and Research (BMBF) that is supported and evaluated by the Open Knowledge Foundation Germany. It funds individuals and small organizations to develop open source applications designed for the common good.

11
About Us/Retreats Normal file
View file

@ -0,0 +1,11 @@
---
title: Retreats
---
Twice a year the Robur team meet with others from the OCaml and MirageOS community at a week long hack retreat in Marrakesh, Morocco.
We use these times to discuss and learn about new developments in the MirageOS ecosystem and meet in person about our Robur projects. And of course we have fun whilst we are at it!
Whilst there are limited places for each retreat we are always open to new people with an interest in OCaml and MirageOS joining us. It doesn't matter if you haven't coded in OCaml before, if you come with an enthusiasm to learn we have an enthusiasm to share.
The retreats are held in a hostel in the center of the city, which we wholly rent out for the period, with food provided. If you are interested in participating in the next retreat please [see the MirageOS site](http://retreat.mirage.io/) for more details and sign-up method.

46
About Us/Team Normal file
View file

@ -0,0 +1,46 @@
---
title: Team
---
### Stefanie
Stefanie is an infrastructure software engineer and a researcher.
She studied Applied Computer Science in the Natural Sciences, and developed a typechecker for a compiler of a language for optimization problems. In her PhD project she developed metrics to compare forest data structures, with an application in molecular structure comparison. Working as a postdoc in cancer research on molecular structure prediction, she found her way to Brooklyn and Berlin.
In the US tech industry, she works on infrastructure problems with distributed systems at a large scale with millions of users, developing API infrastructure and search infrastructure, with a focus on stateless systems.
Her Erdős number is 4.
### Hannes
Hannes enjoys living in Berlin, Germany. Until end of 2017, he used to be a research associate at the University of Cambridge in the rems project. He enjoys to write code, and also travelling and repairing his recumbent bicycle, and being a barista.
Hannes did his PhD in computer science about formal verification of imperative code (using a higher-order separation logic and the theorem prover Coq). Hannes co-authored not-quite-so-broken TLS, a TLS implementation from the ground up in OCaml, and contributes to the MirageOS project as a core team member. He is working on various projects, including opam signing and netsem, an executable formal model of TCP/IP which can act as a test validator.
### Martin
Martin has been programming since before programming was trendy, eating Sharp SC61860A machine code for breakfast since before it was healthy, and using Linux way back when it was just Linus Torvalds’ glorified terminal emulator.
A founding member of Unikernel Systems (later acquired by Docker), Martin has been involved in a number of library operating system projects since 2014, including the Rumprun unikernel and MirageOS. He is a co-author of Solo5, a secure execution environment for unikernels, and joins Robur in 2018 to continue his work towards creating secure software that “just works” and other ambitious projects.
Martin lives with his family in Bratislava, Slovakia and in his spare time enjoys hiking, yachting and the arts.
#### Mindy
Mindy ran the first MirageOS unikernel in the public cloud in 2014. Mindy has worked extensively on the MirageOS TCP/IP network stack and various protocol implementations, and is a member of the project's core team. She managed the release of MirageOS's latest major version.
Mindy is interested in freeing software from unnecessary dependencies, including monolithic kernels. While she finds testing and bug-fixing rewarding, her true goal is to apply techniques that remove entire bug classes to broader classes of computation. Memory safety isn't just for application code!
In her free time, Mindy enjoys bothering cats, playing board games, riding bicycles, and embroidery. She lives in beautiful Madison, Wisconsin in the United States.
### Joe
Joe is an independent IT consultant located in Copenhagen.
Joe has a background in penetration testing, protocol design, applied cryptography, and architectural IT security system design for customers, especially in the banking, insurance, and pension fund sectors. He has been consulting on BPAY integration in Australia, and conducting web and network security assessments for customers throughout the world.
Lately he has spent the last couple of years writing OCaml and has been working with IT security, dev-ops and automated deployment for customers specializing in Enterprise Resource Planning, Internet of Things, and medical technology.
In his spare time he dabbles in research into similar topics and serialization frameworks, in addition to the enjoyable pursuit of tabletop roleplaying and social interactions in smoky pubs - two disciplines that he excels in, but that have somehow not been of particular interest to paying customers (yet).

7
Contact
View file

@ -2,10 +2,7 @@
title: Contact
---
If you want to fund our work, we [are happy to receive donations](/Donate).
You can reach us by mail at `team@robur.io`.
If you wish, you may encrypt your email with the OpenPGP key
[0CBFC7AA](/static/0CBFC7AA.txt), fingerprint: `27EB8C7B 7BC95BDC 9B4B63CD
599270C7 0CBFC7AA`.
If you wish, you may encrypt your email with our [OpenPGP key 0CBFC7AA](/static/0CBFC7AA.txt), fingerprint: 27EB8C7B 7BC95BDC 9B4B63CD 599270C7 0CBFC7AA.

39
Donate
View file

@ -2,46 +2,37 @@
title: Donate
---
Robur is a project of the [Center for the Cultivation of
Technology](https://techcultivation.org), a charity registered in Germany.
Donations to robur are tax-deductible in Europe.
We are passionate about creating secure and reliable open source infrastructure. We have worked on secure implementations of important applications such as [PGP](/Projects#PGP) and [DNS](/Projects#DNS).
Wir sind eine gemeinnützige Organisation, somit können Spenden an uns europaweit
von der Steuer abgesetzt werden. Für Spenden bis 200€ reicht der Kontoauszug
zusammen mit [unserem vereinfachten
Spendennachweis](https://techcultivation.org/documents/cct-vereinfachter-spendennachweis.pdf),
für größere Spenden schicke uns bitte deine Postanschrift und das Datum der
Spende an `donate@techcultivation.org`.
Unfortunately such projects aren't always easy to get full grants for, and public donations really help us in completing such work.
For Germany, you can [download a general donation
receipt](https://techcultivation.org/documents/cct-vereinfachter-spendennachweis.pdf)
that together with your bank statement is sufficient to claim taxes on donations
up to 200€.
If you want to assist us continue these projects we would be grateful for a donation and promise to spend your money well (for more information on how we spend the funds we get please see our [funding page](/Funding).
For other European countries and larger donations, we're happy to provide
individual donation receipts and work with you on their recognition. For that,
please send us your full name and postal address and the date of your
transaction to `donate@techcultivation.org`.
As Robur is a project of the nonprofit [The Center For Technical Cultivation](https://techcultivation.org) we are [tax deductible in Europe](/Donate#Tax-Deductibility).
To donate via SEPA wire transfer, use:
### How To Donate
- To donate via SEPA wire transfer, use:
```
Account holder: Center for the Cultivation of Technology
Subject: robur JSR9DAHD
IBAN: DE65 4306 0967 4111 9411 01
BIC: GENODEM1GLS
Bank: GLS Gemeinschaftsbank, Christstrasse 9, 44789 Bochum, Germany
```
For US ACH wire transfers, use:
- For US ACH wire transfers, use:
```
Account holder: Center for the Cultivation of Technology
Subject: robur JSR9DAHD
Account number: 8310006087
ACH Routing number: 026073150
Wire routing number: 026073008
Bank: Transferwise, 19 W 24th Street, New York 10010, USA
```
You can also donate to our bitcoin wallet `1EP21qxHyzvAp3aufLBhnGZepTh7n3SS6S`.
- You can also donate to our bitcoin wallet 1EP21qxHyzvAp3aufLBhnGZepTh7n3SS6S.
### Tax Deductibility {#Tax-Deductibility}
For Germany, you can [download a general donation receipt](https://techcultivation.org/documents/cct-vereinfachter-spendennachweis.pdf) that together with your bank statement is sufficient to claim taxes on donations up to 200€.
For other European countries and larger donations, we're happy to provide individual donation receipts and work with you on their recognition. For that, please send your full name and postal address and the date of your transaction to `donate@techcultivation.org`.

41
Home
View file

@ -1,34 +1,19 @@
---
---
[//]: # (Computers on the Internet get compromised mostly to gain or block access to data: User data is being downloaded, leaked and sold, or ransomware blocks access to user data until a fee is paid. Other common attacks target compute resources, to use them in denial of service attacks or to manipulate opinion with chatbots.)
[//]: # (Common software stacks often include legacy parts at runtime that provide unnecessary attack surface. Critical security updates are rarely deployed on time, because they result in unforeseen behaviour. Also, lots of embedded devices are missing a secure update channel.)
Robur is a open source software cooperative.
We build performant bespoke minimal operating systems for high-assurance services.
With our approach to systems development we provide the following advantages for you:
* cutting-edge systems programming and security research
* systems based on the unikernel pioneer [MirageOS](https://mirage.io)
* secure implementation guarded against memory corruption, type-level problems, leaky abstraction and unforeseen state
* ready for the cloud, runs on all major hypervisors
* instant boot (milliseconds)
* competitive performance to C implementations
* can target embedded devices, small size (~4% of UNIX based system), compilation to native code
* minimal codebase without mutable state allows to reason about entire systems and adherence to specification
* extensive library ecosystem, yet minimal trusted code base at runtime
* rapid prototyping with a seamless path from prototype to production
* possibility to formally verify important parts with a proof assistant
<sub><sup>robust open source software design</sup></sub>
<sub><sup>prioritising security all of the time</sup></sub>
Our team is eager to develop applications for high assurance, which seamlessly
integrate in your existing infrastructure. Contact us and we'll collaboratively
develop a more secure architecture and a smooth migration plan for your
organization. And we'll implement and deploy this together at your organization.
We bring a variety of solutions, including basic network services, DNS, DHCP,
TLS, persistent storage (like git), and are happy to expand these to your needs.
<br>
<br>
<br>
<br>
>>>>>>>># *R*obust Infrastructure
>>>>>>>># *O*pen Source Projects
>>>>>>>># *B*ottom-up Approach
>>>>>>>># *U*nderscoring Security
>>>>>>>># *R*eliable Technology
Take a look at our [technology](/Technology), learn about our [concept and
team](/About) or browse some [projects](/Projects). You can reach us by mail at
team@robur.io.

39
Our Work/Our-Approach Normal file
View file

@ -0,0 +1,39 @@
---
title: Our Approach
---
We are a nonprofit open source software cooperative whose mission is to develop robust and secure digital infrastructure. We strive to enable more people to reliably run their own infrastructure by producing correct, surprise-free software to be deployed in real environments. Our software aims to meet the needs of anyone working in an environment where security and dependability is vital.
We write all our code in a high-level memory-safe (and more secure) programming language called [OCaml](/Technology-Employed#Ocaml). In addition each piece of software leverages [MirageOS](/Technology-Employed#MirageOS) (a minimal operating system) to produce bespoke applications tailored to only contain their required functionality. Each service is executed on virtual machines with a size usually around 1-10 MB, much smaller than a UNIX / Linux system, and it boots within milliseconds.
Where other approaches try to patch general purpose operating systems by adding more layers, we strive to build a secure system from the ground up.
Our approach means our software has a number of security and ease-of-use benefits:
- each application is small and fast to start
- our software can be run on all major hypervisors and is ready for the cloud
- we are able to provide rapid prototyping with a seamless path from prototype to production
- reduced attack vectors, for example by guarding against things like memory corruption
- a small code base which means a smaller attack surface, and easier review and audit
- the complexity is reduced ensuring ease of use and helping people to understand the technology
- it is possible to formally verify important parts with a proof assistant (proof writing software)
We work with [clients](/Funding), [partners](/Network#Collaborations) and [funders](/Network#Funders) to design and develop open-source protocols and applications within this approach.
If you are interested in seeing how we can assist you in improving your organization's digital infrastructure please see our [services offered](/Services-Offered).
If you like our approach to open source software and want to support our work please consider a [donation](/Donate).
Or if you are a funder of open source projects focused on security and reliability and like our approach we would love to hear from [you](/Contact).

64
Our Work/Projects Normal file
View file

@ -0,0 +1,64 @@
---
title: Projects
---
# PGP {#PGP}
OpenPGP is a much-used standard of encryption and is widely used to encrypt text, files and emails, amongst other things.
Robur is implementing OpenPGP in OCaml, for use in MirageOS and any other compaitble platform or software that is looking for PGP written in a [secure language](/Technology-Employed#Ocaml).
This work is funded through donations and is still an ongoing project, which means that it may not currently possess all the features required for various use-cases. Currently our implementation can sign, verify, compress, encrypt and decrypt.
You can assist us in implementing more of the OpenPGP protocol through a [donation](/Donate). If you are interested hearing more about the project, require additional features to be implemented to accommodate your project’s needs, or are able to assist with a grant please [get in touch with us](/Contact)!
#### More technical information:
Robur maintains a partial, opinionated implementation of OpenPGP version 4 (RFC 4880) and the related standards, written in OCaml and compatible with MirageOS.
The software consists of a library, and various UNIX tools that make use of the library, and can be used to interact with systems that are currently using GnuPG or other OpenPGP implementations for file encryption or verification using OpenPGP signatures. Notably it can be used from within MirageOS applications without having to bundle a C implementation, and the UNIX binaries are separated from the library so that your applications can use the library directly, unlike GnuPG or libgpgme whose API translates to repeated executions of the gpg2 binary and parsing of the textual output from that.
Currently we have implemented signing/verification and encryption/decryption, but there is no support for elliptic curve cryptography. Decompression of ZLIB streams is supported through the use of a pure OCaml library called decompress. While some things are implemented with a streaming API, many operations make use of an in-memory buffer, which introduces memory constraints on the file handled (this is an area where there is definitely room for improvement).
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.
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.
#### More technical information:
Solo5 features include:
* a sandboxed environment (CPU, memory) to execute native code in
* clock interfaces to access system time
* network interfaces to allow the unikernel to communicate with the outside world
* block storage interfaces to allow the unikernel to store persistent data
* an output-only "console" interface for logging and debugging
Solo5 has been designed to isolate the unikernel as much as possible from its host, while making the best of the available isolation technologies that the host hardware, operating system or hypervisor provide, such as hardware-assisted virtualization, system call filtering and so on. Interfaces are intentionally designed to treat the unikernel as a "static system". In other words, the unikernel must declare its intent to make use of host resources (such as memory, network or storage) up front, and can not gain access to further host resources at run time.
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.

70
Our Work/Publications-and-Talks Normal file
View file

@ -0,0 +1,70 @@
---
title: Publications and Talks
---
We regularly give talks and write publications about our work, OCaml and MirageOS and other aspects of coding, security and computer science that we have expertise in. Below are some examples of these, if you are interested in having a Robur member speak at your event please [reach out](/Contact) to us.
# Hannes Mehnert
### Talks:
CERN Computing Seminar 2019 – [MirageOS: robust and secure services for the cloud](https://cds.cern.ch/record/2674523)
Presenting MirageOS and its advantages along with explaining several applications being developed within it.
BOB 2018 - [Engineering TCP/IP with logic](https://www.youtube.com/watch?v=AYDws2Nqcgs)
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, retransmission, etc.
BornHack 2018 - [MirageOS: what did we achieve in the last year?](https://www.youtube.com/watch?v=QtPUCC6KaWo)
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)
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 minimisation, DNS-over-TLS); provisioning let's encrypt certificates; and attachs (poisoning, amplification). Explains the Robur implementation of DNS with above mentioned extensions as minimized MirageOS unikernels.
### Publications:
[Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API (JACM vol 66, January 2019)](https://dl.acm.org/citation.cfm?id=3243650), [full paper.](https://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf) (Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, Keith Wansbrough)
[Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation (Usenix security 2015)](https://usenix15.nqsb.io), [video presentation](https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/kaloper-mersinjak) (David Kaloper-Meršinjak, Hannes Mehnert, Anil Madhavapeddy, Peter Sewell)
[Not-quite-so-broken TLS 1.3 Mechanised Conformance Checking - TLS 1.3 Ready or Not (TRON)](https://tron.nqsb.io), [workshop website](https://www.ndss-symposium.org/ndss2016/tron-workshop-programme/) (David Kaloper-Meršinjak and Hannes Mehnert)
[Unikernels as Processes - ACM Symposium on Cloud Computing 2018](https://dl.acm.org/citation.cfm?id=3267845) (Dan Williams, Ricardo Koller, Martin Lucina, Nikhil Prakash)
# Martin Lucina
### Talks:
FOSDEM 2019 - [Solo5: A sandboxed, re-targetable execution environment for unikernels](https://www.youtube.com/watch?v=VO6f7uSs3-I)
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:
[Unikernels as Processes - ACM Symposium on Cloud Computing 2018](https://dl.acm.org/citation.cfm?id=3267845) (Dan Williams, Ricardo Koller, Martin Lucina, Nikhil Prakash)
# Mindy Preston
### Talks:
DevOpsDays MSN 2018 - [FuzzOps](https://www.youtube.com/watch?v=BtJsakoXxdY)
Discusses testing software to find bugs before deploying software, including continuous integration solutions and property-based testing. Looks at issues of testing frameworks, including common human errors. Explains fuzzers - a solution to this important problem in which computers generate inputs and find counter examples to enable more complete code testing and bug finding.
Confreaks 2017 - [DHCP: IT’S MOSTLY YELLING!!](https://www.youtube.com/watch?v=enRY9jd0IJw)
Discusses how the Dynamic Host Configuration Protocol (DHCP) is structured and how it is used in a network. Explains how addressing and packet structure (or yelling) in DHCP works to establish a connection, and what can go wrong. Looks at tcpdump as a way to examine this yelling along with DHCP options to help establish a quieter and more secure connection.
Strange Loop 2015 - [Non-Imperative Network Programming](https://www.youtube.com/watch?v=GNc1t6Q5Dls)
Discusses how network programming is often taught and practiced in C, but it doesn't have to be. We can build better network stacks -- ones more expressive, intuitive, and robust -- in other languages! There are many non-C network stacks in the world, and we can learn a lot from the diversity of solutions for common problems.
# Stefanie Schirmer
### Talks:
Berlin Buzzwords 2018 - [Your Search Service as a Composable Function](https://www.youtube.com/watch?v=4Yag3SrAMnI)
Discusses the real-time processing pipeline of modern search systems. Speaking from her previous experience at Etsy Stefanie explains how several different backends power Etsy's search, among them Solr, Elasticsearch, our own key-value-store Arizona, and services for machine learning and inference. How do all these systems work together, present a common interface to Etsy's developers and a coherent search experience to our users? She talks about their learnings along the way of building this proxy, and trying to find the right abstraction for the search problem.
JSConf EU 2015 - [Functional programming and curry cooking in JS](https://www.youtube.com/watch?v=6Qx5ZAbfqjo)
This talk explores functional programming concepts, which help us create powerful abstractions to master complex problems and create more simple and elegant programs. JavaScript allows us to ease into the functional programming style, letting us focus just on the concepts, without the distraction of learning a specific functional programming language. To make the dry functional programming concepts more digestible, we use cooking as an analogy. And since the logician Haskell Curry invented functional programming, we combine our journey in JavaScript with examples and recipes for tasty curry dishes.

32
Our Work/Services Normal file
View file

@ -0,0 +1,32 @@
---
title: Services
---
We can work with you to design, develop and audit software and infrastructure to assist you in enhancing your technical security and reliability. Whilst we are not a service provider, and so can not offer to host applications, we can assist you in deploying MirageOS and OCaml services.
### Design
Working with you to understand the needs of your organization, and how your software infrastructure is currently setup and used, we can assist you in working out any improvements you might require.
We can consult on design for specific products to ensure you plan the best solution for a single application, or take a more holistic view of your infrastructure and protocols to improve speed, security and ease of use.
We’re experienced in designing and reviewing serialization frameworks, network protocols, cryptographic protocols, and system architectures, and with solutions built on the FreeBSD and Linux operating systems, including sandboxing, hardening and exploit mitigations.
### Develop
Working with [Ocaml](/Technology-Employed#OCaml) and [MirageOS](/Technology-Employed#MirageOS) we can develop specific applications that give you high assurance of their security and functionality, which seamlessly integrate in your existing infrastructure.
We can also work on a full stack approach to meet your needs and help a smooth migration plan for your organization.
We can bring a variety of solutions, including basic network services, DNS, DHCP, TLS, persistent storage (like git), and are happy to expand these to your needs.
### Audit
We can provide code auditing services, particularly focusing on security and reducing code base. We have team members who have thorough experience working with OCaml, C (embedded, kernel and userspace), x86 assembly, Scala, Java, Android, Haskell, PHP and Python.
Our audits can help ensure your environment is secure whilst also working with you to reduce attack service and increase speed. While we generally prefer “white-box” audits because we believe they yield the best results for the time invested, we also have experience with “black-box” penetration testing.
Please [contact us](/Contact) if you are interested in any of the above and we can discuss how we can assist you in developing a more secure architecture and for your organization.

101
Our Work/Technology-Employed Normal file
View file

@ -0,0 +1,101 @@
---
title: Technology Employed
---
# MirageOS {#MirageOS}
MirageOS is a software suite to build custom-tailored operating systems from (mostly open source) small individual libraries. It has been developed since 2009 at the University of Cambridge, UK and is written in the programming language [OCaml](/Technology-Employed#Ocaml).
It compiles the necessary OCaml libraries into a unikernel - a small operating system, each built for a certain purpose. For each unikernel we can pick from hundreds of permissively licensed open source libraries which implement network protocols, storage on block devices, or interfaces to network devices via the hypervisor or host operating system. As we only put into each one exactly what is needed, each unikernel is fast; instantly booting and, as there is less code base, it is easier to maintain and keep secure.
As an example to see how lines of code compare, here are the number of lines of code needed for different elements of our Bitcoin Pinata, measured in thousands of lines of code:
<table>
<tr><th></th><th>Linux</th><th>MirageOS</th></tr>
<tr><td>Kernel</td><td>1600</td><td>48</td></tr>
<tr><td>Runtime</td><td>689</td><td>25</td></tr>
<tr><td>Crypto</td><td>230</td><td>23</td></tr>
<tr><td>TLS</td><td>41</td><td>6</td></tr>
<tr><td>Total</td><td>2560</td><td>102</td></tr>
</table>
MirageOS is an event-based operating system - it can manage tasks asynchronously. A task gives up the CPU it was using once its execution is finished, or if it has to wait for input. This model leads to a cooperative multitasking programming style, which is much less error prone to one that multi-tasks.
A recent example for code which is not safe that used multitasking is in Ethereum, which lead to a huge amount of the cryptocurrency ether being stolen. Even established software like the Firefox JavaScript engine, or PHP shows similar problems on a regular basis.
#### More Technical Information on MirageOS:
MirageOS is a library operating system where specialization of the running image is done at compile-time. It contains only the runtime system and application code, rendering all of the usual operating system kernel services obsolete, for example our DNS unikernel only needs OCaml runtime and UDP stack, not a full TCP/IP stack. Time and other resources from the OS are explicit instead of implicit, so if a random number generator, console, network interface or file system are needed they are explicitly configured. The simple design of the runtime, with smaller images, create a very fast runtime and MirageOS can boot in just milliseconds.
MirageOS unikernels are clean slate operating systems, not POSIX compatible, that are written in a high level functional language, OCaml. The minimal code base, with minimal use of mutable state, allows us to reason about entire systems with adherence to specification. This leads to single-purpose systems with a minimal attack surface, where lots of layers of complexity (file system, scheduler, process management, virtual memory subsystem) are avoided.
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.
There are generally three ways to feed the virtual machine with configuration data, like network configuration or TLS certificate and key:
* compile the information into the virtual machine image, which requires recompilation 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.
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.
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 reentrant execution errors.
The virtual memory subsystem in contemporary operating systems provides an address mapping for each process. MirageOS unikernels consist of a single CPU execution context and so use a single address space. This severely limits overhead from context switching that is prevalent in traditional operating systems. Spatial memory safety between tasks is achieved statically through leveraging the OCaml type system at compile-time, instead of at run-time using virtual memory as done in traditional operating system.
A number of protocols have already been implemented in MirageOS, with more each year. We focus on fast, secure and robust implementations so we only implement the sensible features for each protocol. OCaml supports exceptions, but writing interfaces that throw exceptions requires rigorous discipline on behalf of the caller in terms of exception handling, and it requires the library author to be disciplined about documenting them. We have a policy of limiting the use of exceptions in MirageOS code and instead relying on explicit return types that encode errors explicitly, meaning the user is confronted with failure modes while writing their application code, and encouraged to handle them.
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.
<br>
<br>
<br>
# OCaml {#OCaml}
OCaml is a mature programming language that is used both in industry (Facebook, Jane Street Capital, Docker, ahrefs, simcorp, lexifi) and academia.
A large reason MirageOS and Robur software have security advantages over other technical projects is the programming language used - OCaml.
OCaml is a functional programming language - the way in which one is forced to construct code minimizes potential bugs in the code, for example by remembering what events have taken place already in the code and not allowing these states to change unless specifically changed. All inputs, outputs and effects of a function are known.
OCaml also helps avoid many common programming errors through automated memory management to avoid memory corruption, and type checking.
OCaml's speed once complied is comparable to C code, one of the fastest languages. OCaml can also be compiled to JavaScript, so both client and server side of a web application can be developed in the same language, allowing for easier understanding of the full application and enhancing security.
#### More Technical Information on OCaml:
### Concepts of the Language
OCaml is a functional programming language with declarative code that minimizes side effects and mutable state. Its functional programming concepts give us a list of security advantages for MirageOS. OCaml avoids the root causes of common flaws in computer security and exploits in a number of ways.
It is a memory safe language so the behavior of our core protocol logic is only dependent on arguments not arbitrary memory, avoiding memory corruption. OCamls strings are immutable by default and type checking allows us to avoid many common programming errors, including guarding against leaky abstraction.
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
### Verification
A large subset of the OCaml semantics has been mechanically proven sound in a proof assistant.
OCaml is the implementation language of the well-known proof assistant Coq. Development in Coq can be extracted to OCaml code, as demonstrated by CompCert, a formally verified optimizing C compiler, in order to be compiled and executed. The opposite direction is also possible: OCaml code can be translated into Coq definitions (using Coq of OCaml).
### Compilation
OCaml code compiles to native code, which is competitive, and comparable to compiled C code. As an example, our TLS library has up to 85% of the bulk throughput of OpenSSL (using AES128-CBC). The TLS handshake performance is comparable with OpenSSL.
The OCaml compiler generates native code for x86, arm, etc., and has a bytecode backend, which can target microcontrollers (PIC18 family in the OcaPIC project). OCaml can also be compiled to JavaScript, so both client and server side of a web application can be developed in the same language with shared interface code (more details at the Ocsigen project).
In 2016, Facebook developed ReasonML, a dialect of OCaml which syntax is closer to JavaScript, and easier to comprehend for beginners coming from that family of programming languages. ReasonML and OCaml code can be easily combined into a single application, since they use the same compiler.
### Further Information
There is active work on OCaml language development and its runtime system. More literature on why OCaml is a good choice has been written by Yaron Minsky (Jane Street) in the article [OCaml for the masses](https://queue.acm.org/detail.cfm?id=2038036), and more recently by the crypto-ledger [Tezos](https://tezos.com/static/position_paper-841a0a56b573afb28da16f6650152fb4.pdf).

46
Projects/CalDAV
View file

@ -1,46 +0,0 @@
---
title: CalDAV server
abstract: ![calendar](/static/img/calendar.png)
---
![calendar](/static/img/calendar.png)
Calendaring software provides users with an
electronic version of a calendar. Additionally, the software may provide an
appointment book, address book, or contact list.
We implemented a CalDAV server based on MirageOS.
[CalDAV](https://en.wikipedia.org/wiki/CalDAV) is a calendaring extension to
WebDAV, an HTTP-based protocol that allows to read, write and alter files, directories and file properties.
The calendar data can be stored in memory, on disk, or in a
git repository using [irmin](https://github.com/mirage/irmin).
We tested interoperability with most common CalDAV clients (DAVdroid on Android, Thunderbird Lightning on Linux/Unix/Windows, Apple
calendar app on MacOS and iOS).
## How to try the calendar server
There is a live instance for testing available at `calendar.robur.io`.
There is a test user called `test` with password `password` for your convenience.
If you use MacOS, you need add a new CalDAV account in the calendar app, set it to manual, and enter the above URL, username and password.
For iOS you need to add an account in the calendar app, select "other" and then CalDAV.
Discovery of calendars happens automatically.
If you use Thunderbird Lightning, you need to create a new calendar on the network, select CalDAV as remote calendar format, and enter a full calendar URL, e.g.
`https://calendar.robur.io/calendars/<username>/calendar`.
If you use DAVdroid, you can enter the short URL like for MacOS, but you need to append `/calendars`.
Discovery of calendars happens automatically.
## How to host the calendar server yourself
See the [installation instructions on the project home on github](https://github.com/roburio/caldav/blob/master/README.md).
Time to add some calendars and fun meetups!
## Funding
This project was funded via the [prototype
fund](https://prototypefund.de/project/robur-io/). Thanks a lot!

46
Projects/HomeRouter
View file

@ -1,46 +0,0 @@
---
title: Home router
abstract: ![home router](/static/img/homerouter.png)
---
![home router](/static/img/homerouter.png)
This is just a project idea, not (yet) a finished project.
A home router is a computer which manages the Internet uplink for a client, and
provides local connectivity. It is accessible via the Internet, and the
software running on a router needs to be hardened against attackers. Attackers
are searching for flaws in popular routers, because if they can breach their
security, they get access to a large amount of computing and bandwidth
resources.
The home router provides basic network services for the local network, such as a
domain name service (DNS) caching resolver, dynamic host configuration (DHCP),
wireless (using WPA2 and WPS) networks, wired network connectivity,
communication with the service provider (e.g. using PPP and PPPoE) including
authentication, a web server for configuration.
Clients are demanding increasing feature sets, including network storage, voice
over IP (VoIP) endpoint, virtual private network (VPN) integration, data
collector and broker for the Internet of things.
Lots of home routers are currently based on a small Linux distribution, and if a
security issue is discovered in any subsystem, this likely leads to a compromise
of the entire router. Secure update channels may not be available, and even if
so, the fear that updating may introduce unforeseen behaviour keeps people away
from updating their routers.
We would base a router on top of an off-the-shelf arm64 board, where MirageOS is
already running, using kvm as hypervisor. Each network service would run as a
separate virtual machine. Several services are already available as MirageOS
unikernels, such as a caching DNS resolver, a DHCP server, a firewall with NAT, an MQTT implementation,
a web server, ... A secure update channel, based on TUF, is currently under
development.
The infrastructure for distributing binary updates would be some Linux host
which compiles the above mentioned unikernels whenever a dependent library is
updated or changes are rolled out to the unikernel code themselves.
Other required network services which are not yet implemented in OCaml, such as
WPA2 or VoIP, would initially be based on a Linux virtual machine. MirageOS
unikernels and Linux virtual machines can coexist.

34
Projects/Pinata
View file

@ -1,34 +0,0 @@
---
title: The Bitcoin Piñata
abstract: ![Piñata](/static/img/pinata.png)
---
![Piñata](/static/img/pinata.png)
The [Bitcoin Piñata](http://ownme.ipredator.se) is a unikernel which serves as
bug bounty system to test TLS and the underlying implementations. Its
communication endpoints are a website describing the setup, and both a TLS
client and a TLS server listening on a port. The total size, including TLS,
X.509, TCP/IP, of the virtual machine image is 4MB, which is less than 4% of a
comparable system using a Linux kernel and OpenSSL.
When a TLS handshake with the Piñata is successful including mutual
authentication, the Piñata transmits the private key to a Bitcoin wallet which
initially contained 10BTC. The project started on February 10th 2015. Our
lender transferred on March 18th 2018 the 10BTC and repurposed them for other
projects.
On startup, the Piñata generates its certificate authority on the fly, including
certificates and private keys. This means that only the Piñata itself contains
private keys which can authenticate successfully, and an attacker has to find
an exploitable flaw in any software layer (OCaml runtime, virtual network
device, TCP/IP stack, TLS library, X.509 validation, or elsewhere) to complete the challenge.
The Piñata is online since February 10th 2015, and even though hundreds of
thousands of connections and initiated TLS handshakes, no Bitcoins were taken.
By using a Bitcoin wallet, the Piñata is a transparent bug bounty. Everybody
can observe (by looking into the blockchain) whether it has been compromised and
the money has been transferred to another wallet. It is also self-serving: when
an attacker discovers a flaw, they don't need to fill out any forms to retrieve
the bounty, instead they can take the wallet, without any questions asked.

21
Projects/TLStunnel
View file

@ -1,21 +0,0 @@
---
title: TLS reverse proxy
abstract: ![TLS reverse proxy](/static/img/reverse.png)
---
![TLStunnel](/static/img/reverse.png)
The [tlstunnel](https://github.com/hannesm/tlstunnel) is a reverse proxy unikernel which
listens for TLS connections, and forwards requests to backends, such as a
web server. The backend is chosen by inspecting the Server Name
Indication, a widely deployed extension of the TLS protocol, where a client
requests the server name to talk with during the TLS handshake.
The project is similar to others, such as stunnel or stud, but uses our TLS
implementation written in the memory-safe language OCaml, instead of one written
in C. The backend web servers don't need TLS support,
which lowers the maintenance burden. Most security problems in TLS
implementations are caused by unsafe memory handling and support for weak cryptographic primitives.
This TLS reverse proxy is deployed on various websites, including [Real World
OCaml](https://realworldocaml.org) since 2015.

182
Technology
View file

@ -1,182 +0,0 @@
---
title: Technology
---
We develop digital infrastructure with a minimal footprint. Where other approaches
try to patch general purpose operating systems by adding more layers of indirection,
we strive to build a secure system from the ground up.
Each piece of digital infrastructure or service is written in a high-level
memory-safe programming language and tailored to only contain the
required functionality at compilation time. This reduces the attack vectors
and the attack surface.
The resulting service is executed as a virtual machine on a modern hypervisor.
Its size is usually around 1-10 MB, much smaller than a UNIX / Linux system, and boots within milliseconds.
## MirageOS - bespoke operating systems
Our work is based on MirageOS, a suite to build operating systems. It has been developed
since 2009 at University of Cambridge, UK and is written in the programming language
OCaml (see [Why OCaml](#Why-OCaml)).
Most libraries are developed as open source (MIT/ISC/BSD2/Apache2).
MirageOS is a library operating system. It composes OCaml libraries into a
bespoke operating system, called a unikernel. A unikernel can be a compiled as a
UNIX binary, or a standalone virtual machine image. To build the right
unikernel for your custom business logic, we can pick from hundreds of libraries which
implement network protocols, storage on block devices, or interfaces to network devices
via the hypervisor.
On top of the hypervisor, a small layer of C code unifies
the interface on which OCaml runs.
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.
## Running unikernel, system security
Aside from automated memory management to avoid memory corruption, and type checking to avoid many common
programming errors, the major advantage of functional programming is localized reasoning about program code.
All inputs, outputs and effects of a function are known.
Immutable datastructures and cooperative multitasking allow us to reason about the state of the entire system,
even if we use parallelism and complex distributed systems.
### Simple config management model with localized reasoning
There are three ways to feed a virtual machine with configuration data like
network configuration or TLS certificate and key:
- compile the information into the virtual machine image, which requires
recompilation 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.
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.
### Simple concurrency model with localized reasoning
MirageOS is an event based operating system with asynchronous tasks. A task
yields the CPU once its execution is finished, or if it has to wait for IO.
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 reentrant execution errors.
A recent example for code which is not safe under reentrant execution
[in Ethereum](http://hackingdistributed.com/2016/06/18/analysis-of-the-dao-exploit/)
lead to a huge amount of ether being stolen.
Established software like the [Firefox JavaScript engine](http://www.nist.org/news.php?extend.175),
or [PHP](https://bugs.php.net/bug.php?id=74308) shows similar problems on a regular basis.
### Simple process memory model with localized reasoning
The virtual memory subsystem in contemporary operating systems provides an
address mapping for each process. Since a unikernel is only a single service, it
uses a single address space, avoiding the need for complex address mapping code
altogether.
[//]: # (I think we should explain the context for mentioning Xen here)
An example for corrupting the page table is [Xen's XSA-182](http://xenbits.xen.org/xsa/advisory-182.html).
### Simple library model with localized reasoning
A MirageOS unikernel is much smaller than a comparable UNIX
virtual machine. By avoiding superfluous code we decrease the attack surface
immensely.
Consider the breakdown of the code of the example system [Bitcoin Piñata](/Projects/Pinata) compared
to a virtual machine using Linux and OpenSSL, measured in thousands of lines of code:
<table>
<tr><th></th><th>Linux</th><th>MirageOS</th></tr>
<tr><td>Kernel</td><td>1600</td><td>48</td></tr>
<tr><td>Runtime</td><td>689</td><td>25</td></tr>
<tr><td>Crypto</td><td>230</td><td>23</td></tr>
<tr><td>TLS</td><td>41</td><td>6</td></tr>
<tr><td>Total</td><td>2560</td><td>102</td></tr>
</table>
### Secure updates
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](https://opam.ocaml.org).
It resolves dependencies and lets [authors sign their releases](https://github.com/hannesm/conex),
so there is no need for a central package repository server.
Central repository servers are known targets for attackers and have been breached in the past, amongst them
the [Linux kernel](https://lwn.net/Articles/57135/), [FreeBSD
infrastructure](https://www.freebsd.org/news/2012-compromise.html),
[Debian](https://www.debian.org/News/2003/20031202) and
[PHP](http://php.net/archive/2013.php#id2013-10-24-2).
## Why OCaml
### Functional programming style
As discussed in the system security paragraph, many security advantages of MirageOS are
based on the choice of a programming language in which problems can be solved in a functional style.
This style allows us to reason about the possible states of a system.
### Performance
OCaml code compiles to native code, which is
competitive, and comparable to compiled C code. As
an example, our [TLS library](https://usenix15.nqsb.io) has up to 85% of the bulk throughput of OpenSSL (using
AES128-CBC). The TLS handshake performance is comparable with OpenSSL.
### Dependency management
MirageOS leverages OCaml's module system to adapt the unikernel to the compilation target.
Each operating system service in MirageOS is a module, for example the console, the
network stack, the random number generator.
Each of the services has multiple implementations that are chosen based on the target.
On UNIX, the sockets API of the host is used as networking stack. On a
unikernel, the TCP/IP stack natively implemented in OCaml is being used.
A MirageOS developer does not need to reason about compilation targets, just about the
module interface.
### Verification
A large subset of the OCaml semantics has been [mechanically proven
sound](http://www.cl.cam.ac.uk/~so294/ocaml/) in a proof assistant.
OCaml is the implementation language of the well-known proof assistant
[Coq](https://coq.inria.fr). Development in Coq can be extracted to OCaml code,
as demonstrated by [compcert](http://compcert.inria.fr/), a formally verified
optimizing C compiler, in order to be compiled and executed. The other
direction is also possible: OCaml code can be translated into Coq definitions
(using [Coq of OCaml](https://github.com/clarus/coq-of-ocaml/)).
[CFML](http://www.chargueraud.org/softs/cfml/) is an ongoing research project
which enables us to prove properties about OCaml programs using the
[Coq](https://coq.inria.fr) proof assistant.
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/)
prompted some language modifications, such as that strings are no longer mutable.
### Modern dialects and compile targets
OCaml is a mature programming language that is used both in
industry (Facebook, Jane Street Capital, Docker, ahrefs,
simcorp, lexifi) and academia.
The OCaml compiler generates native code for x86, arm, etc., and has a bytecode
backend, which can target microcontrollers (PIC18 family in the [OcaPIC project](http://www.algo-prog.info/ocapic/web/?id=OCAPIC:OCAPIC)).
OCaml can also be compiled to JavaScript, so both client
and server side of a web application can be developed in the same language with shared interface code (more details at the [ocsigen project](http://ocsigen.org/)).
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 into a single
application, since they use the same compiler.
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).

154
static/css/style.css
View file

@ -1,154 +0,0 @@
html {
background-color: #fafafa;
font-family: medium-content-serif-font,Georgia,Cambria,"Times New Roman",Times,serif;
font-size: 21px;
}
html a {
text-decoration: none;
color: black;
text-decoration: underline;
}
html a:visited {
color: black;
text-decoration: underline;
}
.navbar {
box-sizing: border-box;
box-shadow: 0 2px 2px -2px rgba(0,0,0,.15);
position: fixed;
top: 0;
right: 0;
left: 0;
z-index: 1030;
background-color: rgba(255,255,128,1);
text-decoration: none;
}
.container {
margin: 0 auto;
max-width: 800px;
}
blockquote {
font-style: italic;
padding: 0px 20px;
margin: 0 0 20px;
border-left: 5px solid #eee;
}
main {
margin-top: 100px;
}
.flex-container {
display: flex;
width: 100%;
justify-content: center;
}
article {
margin-top: 30px;
}
footer {
margin-top: 20px;
}
pre {
padding: 0px;
}
body h2 {
margin-bottom: 3px;
font-weight: 700;
font-size: 40px;
line-height: 1.04;
letter-spacing: -.028em;
font-family: medium-content-sans-serif-font,"Lucida Grande","Lucida Sans Unicode","Lucida Sans",Geneva,Arial,sans-serif;
}
.post-title {
}
.author {
font-size: 13px;
}
.date {
display: none;
}
time {
font-size: 13px;
}
footer {
font-size: 13px;
}
.tags {
font-size: 13px;
}
.post,
.listing {
width: 90%;
max-width: 800px;
}
a.list-group-item {
border: 0;
}
.extract {
margin-top: 10px;
}
.tag {
font-size: 13px;
margin-right: 4px;
}
.navbar-nav {
clear:both;
margin-left: 0px;
padding-left: 0px;
font-family: medium-content-sans-serif-font,"Lucida Grande","Lucida Sans Unicode","Lucida Sans",Geneva,Arial,sans-serif;
font-size: 15px;
padding: 0 0 0 0;
}
.navbar-default li a, .navbar-default li a:visited {
color: #777;
}
.navbar-default li a:hover {
color: black;
}
.navbar-default li {
list-style-type: none;
font-family: medium-content-sans-serif-font,"Lucida Grande","Lucida Sans Unicode","Lucida Sans",Geneva,Arial,sans-serif;
font-size: 21px;
color: #777;
float: right;
padding: 10px 10px 10px 10px;
}
.navbar-header {
float: left;
background-color: rgba(255,255,128,1);
padding: 10px 10px 10px 10px;
}
.navbar-brand {
font-family: "Helvetica Neue",Helvetica,Arial,sans-serif;
font-weight: 700;
font-size: 40px;
}
.navbar-collapse {
float: right;
}
body {
margin: 0px;
}
.footer {
padding-top: 3px;
padding-bottom: 3px;
padding-left: 140px;
background: lightgrey;
}

BIN
static/img/calendar.png
View file

Binary file not shown.
Side by side

Before

Width:  |  Height:  |  Size: 143 KiB

BIN
static/img/homerouter.png
View file

Binary file not shown.
Side by side

Before

Width:  |  Height:  |  Size: 48 KiB

BIN
static/img/pinata.png
View file

Binary file not shown.
Side by side

Before

Width:  |  Height:  |  Size: 21 KiB

BIN
static/img/reverse.png
View file

Binary file not shown.
Side by side

Before

Width:  |  Height:  |  Size: 22 KiB