From 432f97470cddc23f7c3353ca4febd362d8a17eec Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 11 Sep 2019 00:08:49 +0200 Subject: [PATCH 01/13] + in urls --- About Us/Funding | 2 +- Donate | 4 ++-- Our Work/Our-Approach | 6 +++--- Our Work/Projects | 2 +- Our Work/Services | 2 +- Our Work/Technology-Employed | 2 +- 6 files changed, 9 insertions(+), 9 deletions(-) diff --git a/About Us/Funding b/About Us/Funding index 78ba9c5..9bbbb81 100644 --- a/About Us/Funding +++ b/About Us/Funding @@ -11,4 +11,4 @@ We spend most of our funding on salaries, ensuring Robur keeps developing the so * 2% on necessary travel * 10% on inevitable administrative costs -If you are considering [donating](/Donate) to us, [hiring](/Our%20Work/Services) us, or [giving us a grant](/Contact) you can be assured your money will be well spent on the actual end result of delivering the robust and secure digital infrastructure we strive for. +If you are considering [donating](/Donate) to us, [hiring](/Our+Work/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. diff --git a/Donate b/Donate index 410ecbe..21b3deb 100644 --- a/Donate +++ b/Donate @@ -1,11 +1,11 @@ --- --- -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 [PGP](/Our+Work/Projects#PGP) and DNS. Unfortunately such projects aren't always easy to get full grants for, and public donations really help us in completing such work. -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](/About%20Us/Funding)). +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](/About+Us/Funding)). 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). diff --git a/Our Work/Our-Approach b/Our Work/Our-Approach index 835a890..0d32897 100644 --- a/Our Work/Our-Approach +++ b/Our Work/Our-Approach @@ -4,7 +4,7 @@ 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](/Our%20Work/Technology-Employed#Ocaml). In addition each piece of software leverages [MirageOS](/Our%20Work/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. +We write all our code in a high-level memory-safe (and more secure) programming language called [OCaml](/Our+Work/Technology-Employed#Ocaml). In addition each piece of software leverages [MirageOS](/Our+Work/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. @@ -18,9 +18,9 @@ Our approach means our software has a number of security and ease-of-use benefit - it is possible to formally verify important parts with a proof assistant (proof writing software) -We work with [clients](/Our%20Work/Services), [partners](/About%20Us/Network#Collaborations) and [funders](/About%20Us/Network#Grant-Funders) to design and develop open-source protocols and applications within this approach. +We work with [clients](/Our+Work/Services), [partners](/About+Us/Network#Collaborations) and [funders](/About+Us/Network#Grant-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](/Our%20Work/Services). +If you are interested in seeing how we can assist you in improving your organization's digital infrastructure please see our [services offered](/Our+Work/Services). If you like our approach to open source software and want to support our work please consider a [donation](/Donate). diff --git a/Our Work/Projects b/Our Work/Projects index f2878ed..af9c0a3 100644 --- a/Our Work/Projects +++ b/Our Work/Projects @@ -6,7 +6,7 @@ title: Projects 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 compaitble platform or software that is looking for PGP written in a [secure language](/Our+Work/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. diff --git a/Our Work/Services b/Our Work/Services index d8ca023..aeec1c6 100644 --- a/Our Work/Services +++ b/Our Work/Services @@ -14,7 +14,7 @@ We’re experienced in designing and reviewing serialization frameworks, network ### Develop -Working with [OCaml](/Our%20Work/Technology-Employed#OCaml) and [MirageOS](/Our%20Work/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. +Working with [OCaml](/Our+Work/Technology-Employed#OCaml) and [MirageOS](/Our+Work/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. diff --git a/Our Work/Technology-Employed b/Our Work/Technology-Employed index 80e7683..fbf9f03 100644 --- a/Our Work/Technology-Employed +++ b/Our Work/Technology-Employed @@ -4,7 +4,7 @@ title: Technology Employed # 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](/Our%20Work/Technology-Employed#OCaml). +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](/Our+Work/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. From 5af3009835c990752832c392294ad1b119afd8aa Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 11 Sep 2019 00:09:34 +0200 Subject: [PATCH 02/13] Revert "+ in urls" since our ghetto http server is not actually working correctly This reverts commit 432f97470cddc23f7c3353ca4febd362d8a17eec. --- About Us/Funding | 2 +- Donate | 4 ++-- Our Work/Our-Approach | 6 +++--- Our Work/Projects | 2 +- Our Work/Services | 2 +- Our Work/Technology-Employed | 2 +- 6 files changed, 9 insertions(+), 9 deletions(-) diff --git a/About Us/Funding b/About Us/Funding index 9bbbb81..78ba9c5 100644 --- a/About Us/Funding +++ b/About Us/Funding @@ -11,4 +11,4 @@ We spend most of our funding on salaries, ensuring Robur keeps developing the so * 2% on necessary travel * 10% on inevitable administrative costs -If you are considering [donating](/Donate) to us, [hiring](/Our+Work/Services) us, or [giving us a grant](/Contact) you can be assured your money will be well spent on the actual end result of delivering the robust and secure digital infrastructure we strive for. +If you are considering [donating](/Donate) to us, [hiring](/Our%20Work/Services) us, or [giving us a grant](/Contact) you can be assured your money will be well spent on the actual end result of delivering the robust and secure digital infrastructure we strive for. diff --git a/Donate b/Donate index 21b3deb..410ecbe 100644 --- a/Donate +++ b/Donate @@ -1,11 +1,11 @@ --- --- -We are passionate about creating secure and reliable open source infrastructure. We have worked on secure implementations of important applications such as [PGP](/Our+Work/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 [PGP](/Our%20Work/Projects#PGP) and DNS. Unfortunately such projects aren't always easy to get full grants for, and public donations really help us in completing such work. -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](/About+Us/Funding)). +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](/About%20Us/Funding)). 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). diff --git a/Our Work/Our-Approach b/Our Work/Our-Approach index 0d32897..835a890 100644 --- a/Our Work/Our-Approach +++ b/Our Work/Our-Approach @@ -4,7 +4,7 @@ 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](/Our+Work/Technology-Employed#Ocaml). In addition each piece of software leverages [MirageOS](/Our+Work/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. +We write all our code in a high-level memory-safe (and more secure) programming language called [OCaml](/Our%20Work/Technology-Employed#Ocaml). In addition each piece of software leverages [MirageOS](/Our%20Work/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. @@ -18,9 +18,9 @@ Our approach means our software has a number of security and ease-of-use benefit - it is possible to formally verify important parts with a proof assistant (proof writing software) -We work with [clients](/Our+Work/Services), [partners](/About+Us/Network#Collaborations) and [funders](/About+Us/Network#Grant-Funders) to design and develop open-source protocols and applications within this approach. +We work with [clients](/Our%20Work/Services), [partners](/About%20Us/Network#Collaborations) and [funders](/About%20Us/Network#Grant-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](/Our+Work/Services). +If you are interested in seeing how we can assist you in improving your organization's digital infrastructure please see our [services offered](/Our%20Work/Services). If you like our approach to open source software and want to support our work please consider a [donation](/Donate). diff --git a/Our Work/Projects b/Our Work/Projects index af9c0a3..f2878ed 100644 --- a/Our Work/Projects +++ b/Our Work/Projects @@ -6,7 +6,7 @@ title: Projects 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+Work/Technology-Employed#OCaml). +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). 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. diff --git a/Our Work/Services b/Our Work/Services index aeec1c6..d8ca023 100644 --- a/Our Work/Services +++ b/Our Work/Services @@ -14,7 +14,7 @@ We’re experienced in designing and reviewing serialization frameworks, network ### Develop -Working with [OCaml](/Our+Work/Technology-Employed#OCaml) and [MirageOS](/Our+Work/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. +Working with [OCaml](/Our%20Work/Technology-Employed#OCaml) and [MirageOS](/Our%20Work/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. diff --git a/Our Work/Technology-Employed b/Our Work/Technology-Employed index fbf9f03..80e7683 100644 --- a/Our Work/Technology-Employed +++ b/Our Work/Technology-Employed @@ -4,7 +4,7 @@ title: Technology Employed # 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](/Our+Work/Technology-Employed#OCaml). +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](/Our%20Work/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. From 309ffb61d0d8645161f35921eec320137bd99645 Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 11 Sep 2019 00:12:14 +0200 Subject: [PATCH 03/13] no trailing spaces --- Our Work/Our-Approach | 2 +- Our Work/Publications-and-Talks | 2 +- static/css/style.css | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Our Work/Our-Approach b/Our Work/Our-Approach index 835a890..b8eab24 100644 --- a/Our Work/Our-Approach +++ b/Our Work/Our-Approach @@ -14,7 +14,7 @@ Our approach means our software has a number of security and ease-of-use benefit - 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 +- 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) diff --git a/Our Work/Publications-and-Talks b/Our Work/Publications-and-Talks index 2438ff3..74233b0 100644 --- a/Our Work/Publications-and-Talks +++ b/Our Work/Publications-and-Talks @@ -52,7 +52,7 @@ Explains Solo5 which is a microkernel-friendly, sandboxed, re-targetable executi 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) +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)
diff --git a/static/css/style.css b/static/css/style.css index c5b59ff..81212e3 100644 --- a/static/css/style.css +++ b/static/css/style.css @@ -142,7 +142,7 @@ a.list-group-item { float: right; } -body { +body { margin: 0px; } From f1739fca4783ea0d1c0e1e73d10bc9d059447229 Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 11 Sep 2019 00:16:40 +0200 Subject: [PATCH 04/13] #Ocaml -> #OCaml fixup --- Our Work/Our-Approach | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Our Work/Our-Approach b/Our Work/Our-Approach index b8eab24..bed0b19 100644 --- a/Our Work/Our-Approach +++ b/Our Work/Our-Approach @@ -4,7 +4,7 @@ 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](/Our%20Work/Technology-Employed#Ocaml). In addition each piece of software leverages [MirageOS](/Our%20Work/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. +We write all our code in a high-level memory-safe (and more secure) programming language called [OCaml](/Our%20Work/Technology-Employed#OCaml). In addition each piece of software leverages [MirageOS](/Our%20Work/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. From 62514c6b7ffcbff89186792ecdedd719cd62506d Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 11 Sep 2019 00:19:03 +0200 Subject: [PATCH 05/13] woops leave LA out for now --- About Us/Network | 3 --- 1 file changed, 3 deletions(-) diff --git a/About Us/Network b/About Us/Network index 313cdc7..1b0a299 100644 --- a/About Us/Network +++ b/About Us/Network @@ -7,9 +7,6 @@ title: Network [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. From 3c87741524f60c8bceb0faa41ca645c87ba41309 Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 11 Sep 2019 00:22:36 +0200 Subject: [PATCH 06/13] try underlining stuff on frontpage --- Home | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/Home b/Home index 8b0cfce..c6347e9 100644 --- a/Home +++ b/Home @@ -4,13 +4,12 @@


-
-# *R*obust Infrastructure -# *O*pen Source Projects -# *B*ottom-up Approach -# *U*nderscoring Security -# *R*eliable Technology +# __R__obust Infrastructure +# __O__pen Source Projects +# __B__ottom-up Approach +# __U__nderscoring Security +# __R__eliable Technology

From 91ec4da4bd19d2490885c7b8a935365500ecf7aa Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 11 Sep 2019 00:23:27 +0200 Subject: [PATCH 07/13] infix underlining in markdown, how to --- Home | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Home b/Home index c6347e9..3881a20 100644 --- a/Home +++ b/Home @@ -5,11 +5,11 @@

-# __R__obust Infrastructure -# __O__pen Source Projects -# __B__ottom-up Approach -# __U__nderscoring Security -# __R__eliable Technology +# _R_obust Infrastructure +# _O_pen Source Projects +# _B_ottom-up Approach +# _U_nderscoring Security +# _R_eliable Technology

From 3f7af35cce0843f809c646471ffda4246f6bbd8b Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 11 Sep 2019 00:23:45 +0200 Subject: [PATCH 08/13] infix underlining in markdown, how to --- Home | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Home b/Home index 3881a20..b25eb9d 100644 --- a/Home +++ b/Home @@ -5,11 +5,11 @@

-# _R_obust Infrastructure -# _O_pen Source Projects -# _B_ottom-up Approach -# _U_nderscoring Security -# _R_eliable Technology +# __R_obust Infrastructure +# __O_pen Source Projects +# __B_ottom-up Approach +# __U_nderscoring Security +# __R_eliable Technology

From 214529c271caf9843c055e386da10d5dd7b050ed Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 11 Sep 2019 00:25:38 +0200 Subject: [PATCH 09/13] frontpage placeholder with maybe --- Home | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Home b/Home index b25eb9d..37b3c56 100644 --- a/Home +++ b/Home @@ -5,11 +5,11 @@

-# __R_obust Infrastructure -# __O_pen Source Projects -# __B_ottom-up Approach -# __U_nderscoring Security -# __R_eliable Technology +# Robust Infrastructure +# Open Source Projects +# Bottom-up Approach +# Underscoring Security +# Reliable Technology

From 6fcb28629dc5df90ca0bce303455f954e9052b13 Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 11 Sep 2019 00:26:26 +0200 Subject: [PATCH 10/13] damn, aesthetics --- Home | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Home b/Home index 37b3c56..7fd3414 100644 --- a/Home +++ b/Home @@ -5,11 +5,11 @@

-# Robust Infrastructure -# Open Source Projects -# Bottom-up Approach -# Underscoring Security -# Reliable Technology +# R obust Infrastructure +# O pen Source Projects +# B ottom-up Approach +# U nderscoring Security +# R eliable Technology

From dcc0a42c70454ca909f896756ed0cedd738550be Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 11 Sep 2019 00:36:12 +0200 Subject: [PATCH 11/13] PGP + typo --- Donate | 2 +- Our Work/Projects | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Donate b/Donate index 410ecbe..7e71d08 100644 --- a/Donate +++ b/Donate @@ -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. diff --git a/Our Work/Projects b/Our Work/Projects index f2878ed..3380d80 100644 --- a/Our Work/Projects +++ b/Our Work/Projects @@ -2,11 +2,11 @@ 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. -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. From ca364d504c3c13b7eed8093459248ad9010f66a7 Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 11 Sep 2019 00:49:41 +0200 Subject: [PATCH 12/13] make aspell happy --- About Us/Network | 2 +- About Us/Team | 2 +- Our Work/Publications-and-Talks | 6 +++--- Our Work/Technology-Employed | 6 +++--- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/About Us/Network b/About Us/Network index 1b0a299..82d7bc1 100644 --- a/About Us/Network +++ b/About Us/Network @@ -24,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. [The Prototype Fund](https://prototypefund.de/en)
-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. diff --git a/About Us/Team b/About Us/Team index 966e216..6802606 100644 --- a/About Us/Team +++ b/About Us/Team @@ -15,7 +15,7 @@ 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 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. diff --git a/Our Work/Publications-and-Talks b/Our Work/Publications-and-Talks index 74233b0..ea7bb48 100644 --- a/Our Work/Publications-and-Talks +++ b/Our Work/Publications-and-Talks @@ -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. 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. +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)
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. +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: @@ -27,7 +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 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) diff --git a/Our Work/Technology-Employed b/Our Work/Technology-Employed index 80e7683..8bd00b4 100644 --- a/Our Work/Technology-Employed +++ b/Our Work/Technology-Employed @@ -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. -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. @@ -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. -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.
@@ -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. -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. From 4de6d5b0f935eb15c397736435896b0af8a4bd68 Mon Sep 17 00:00:00 2001 From: Hannes Mehnert Date: Thu, 12 Sep 2019 11:53:19 +0200 Subject: [PATCH 13/13] unikernels as processes is mato's paper, not mine ;) (no need to list it twice) --- Our Work/Publications-and-Talks | 3 --- 1 file changed, 3 deletions(-) diff --git a/Our Work/Publications-and-Talks b/Our Work/Publications-and-Talks index ea7bb48..b314401 100644 --- a/Our Work/Publications-and-Talks +++ b/Our Work/Publications-and-Talks @@ -30,9 +30,6 @@ Discusses the basic usage of DNS, including stub and recursive resolver, server; [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 ### Talks: