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

Merge branch 'master' of git+ssh://git.robur.io/robur.io

Browse source
This commit is contained in:
Sol 2019-10-22 17:35:13 +02:00
commit 3a5780ab47
9 changed files with 19 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
About Us/Network
View file

@ -7,9 +7,6 @@ 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)<br />
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 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.
@ -27,7 +24,7 @@ Is a for-profit distributed engineering team based in Paris and Cambridge that m
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. 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)<br /> [The Prototype Fund](https://prototypefund.de/en)<br />
The Prototype Fund has awarded Robur several grants for various projects such as the CalDAV Server, the Mirage Firewall and our OCaml implementation of an OpenVPN Client. 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. The Prototype Fund has awarded Robur several grants for various projects such as the CalDAV Server, the Mirage Firewall and our OCaml implementation of an OpenVPN client. 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.

2
About Us/Team
View file

@ -15,7 +15,7 @@ Her Erdős number is 4.
### Hannes ### 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 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 traveling 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. 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.

2
Donate
View file

@ -1,7 +1,7 @@
--- ---
--- ---
We are passionate about creating secure and reliable open source infrastructure. We have worked on secure implementations of important applications such as [PGP](/Our%20Work/Projects#PGP) and DNS. We are passionate about creating secure and reliable open source infrastructure. We have worked on secure implementations of important applications such as [OpenPGP](/Our%20Work/Projects#OpenPGP) and DNS.
Unfortunately such projects aren't always easy to get full grants for, and public donations really help us in completing such work. Unfortunately such projects aren't always easy to get full grants for, and public donations really help us in completing such work.

11
Home
View file

@ -4,13 +4,12 @@
<br /> <br />
<br /> <br />
<br /> <br />
<br />
# *R*obust Infrastructure # <u>R</u> obust Infrastructure
# *O*pen Source Projects # <u>O</u> pen Source Projects
# *B*ottom-up Approach # <u>B</u> ottom-up Approach
# *U*nderscoring Security # <u>U</u> nderscoring Security
# *R*eliable Technology # <u>R</u> eliable Technology
<br /> <br />
<br /> <br />

4
Our Work/Projects
View file

@ -2,11 +2,11 @@
title: Projects title: Projects
--- ---
# PGP # OpenPGP
OpenPGP is a much-used standard of encryption and is widely used to encrypt text, files and emails, amongst other things. 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](/Our%20Work/Technology-Employed#OCaml). Robur is implementing OpenPGP in OCaml, for use in MirageOS and any other compatible platform or software that is looking for OpenPGP written in a [secure language](/Our%20Work/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. 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.

9
Our Work/Publications-and-Talks
View file

@ -13,13 +13,13 @@ CERN Computing Seminar 2019 – [MirageOS: robust and secure services for the cl
Presenting MirageOS and its advantages along with explaining several applications being developed within it. 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)<br /> BOB 2018 - [Engineering TCP/IP with logic](https://www.youtube.com/watch?v=AYDws2Nqcgs)<br />
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. 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 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. 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.
### Publications: ### Publications:
@ -27,10 +27,7 @@ Discusses the basic usage of DNS, including stub and recursive resolver, server;
[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: 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) [Not-quite-so-broken TLS 1.3 Mechanized 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 # Martin Lucina

6
Our Work/Technology-Employed
View file

@ -41,7 +41,7 @@ There are generally three ways to feed the virtual machine with configuration da
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 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. 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.
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. 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.
@ -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 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 />
@ -76,7 +76,7 @@ OCaml's speed once complied is comparable to C code, one of the fastest 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. 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. 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. OCaml's 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. 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.