fixing more urls and trailing whitespaces
This commit is contained in:
Sol
parent
892dcd8008
commit
e8b0c31bb3
4 changed files with 34 additions and 31 deletions
|
|
@ -2,13 +2,13 @@
|
|||
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.
|
||||
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 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
|
||||
* 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.
|
||||
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.
|
||||
|
|
|
|||
|
|
@ -4,30 +4,30 @@ title: Network
|
|||
|
||||
# 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.
|
||||
[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.
|
||||
|
||||
[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.
|
||||
[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)
|
||||
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](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.
|
||||
|
||||
[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.
|
||||
[OCaml Labs](http://ocamllabs.io)<br />
|
||||
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.
|
||||
[Tarides](https://tarides.com)<br />
|
||||
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
|
||||
|
||||
[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.
|
||||
[NLnet Foundation](https://nlnet.nl)<br />
|
||||
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.
|
||||
[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.
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -2,10 +2,9 @@
|
|||
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.
|
||||
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.
|
||||
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.
|
||||
|
|
|
|||
|
|
@ -1,8 +1,12 @@
|
|||
---
|
||||
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).
|
||||
|
||||
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.
|
||||
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:
|
||||
|
||||
|
|
@ -21,7 +25,7 @@ A recent example for code which is not safe that used multitasking is in Ethereu
|
|||
|
||||
#### 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 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.
|
||||
|
||||
|
|
@ -35,7 +39,7 @@ There are generally three ways to feed the virtual machine with configuration da
|
|||
* 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.
|
||||
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.
|
||||
|
||||
|
|
@ -43,7 +47,7 @@ The virtual memory subsystem in contemporary operating systems provides an addre
|
|||
|
||||
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.
|
||||
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.
|
||||
|
||||
|
|
@ -57,32 +61,32 @@ As some examples of the comparable code base sizes of these protocol implementat
|
|||
|
||||
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.
|
||||
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 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.
|
||||
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.
|
||||
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
|
||||
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).
|
||||
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
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue