commit 99960bf98479bd968be3ec4c6b59690b2efd951d Author: Canopy bot Date: Mon Nov 7 09:55:10 2022 +0000 updated from master (commit 34d1c80e5ca98bffb5eb7c87fce292750b1a1ca1) diff --git a/About Us/Funding b/About Us/Funding new file mode 100644 index 0000000..adc9c3c --- /dev/null +++ b/About Us/Funding @@ -0,0 +1,16 @@ + +Funding

Funding

Published: 2019-09-10 (last updated: 2019-10-22)

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:

83% on salaries +
7% on necessary travel +
10% on inevitable administrative costs +

If you are considering donating to us, hiring us, or giving us a grant 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.

\ No newline at end of file diff --git a/About Us/Network b/About Us/Network new file mode 100644 index 0000000..ee9dae5 --- /dev/null +++ b/About Us/Network @@ -0,0 +1,21 @@ + +Network

Network

Published: 2019-09-10 (last updated: 2020-02-18)

Collaborations

The Center for the Cultivation of Technology
+The Center for the Cultivation of Technology 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 +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
+MirageOS is a library operating system that constructs unikernels for secure and high-performing applications. Most Robur projects are designed to be compatible with MirageOS, as well as native operating systems, like Linux or FreeBSD. We work closely with the MirageOS community to help develop its ecosystem and increase the availability of secure applications offered within it.

OCaml Labs
+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
+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.

+
+

Grant Funders

NLnet Foundation
+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
+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.

\ No newline at end of file diff --git a/About Us/Retreats b/About Us/Retreats new file mode 100644 index 0000000..ecd20b6 --- /dev/null +++ b/About Us/Retreats @@ -0,0 +1,7 @@ + +Retreats

Retreats

Published: 2019-09-10 (last updated: 2019-09-10)

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!

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 for more details and sign-up method.

\ No newline at end of file diff --git a/About Us/Team b/About Us/Team new file mode 100644 index 0000000..2cd6691 --- /dev/null +++ b/About Us/Team @@ -0,0 +1,30 @@ + +Team

Team

Published: 2019-09-10 (last updated: 2021-11-16)

Robur is a software development cooperative specializing in robust and secure digital infrastructure written in OCaml.

Current members

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 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.

Reynir

here some text is missing

Former members

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.

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).

\ No newline at end of file diff --git a/About Us/index.html b/About Us/index.html new file mode 100644 index 0000000..389d294 --- /dev/null +++ b/About Us/index.html @@ -0,0 +1,4 @@ + +robur

Team

Retreats

Network

Funding

\ No newline at end of file diff --git a/Contact b/Contact new file mode 100644 index 0000000..95db894 --- /dev/null +++ b/Contact @@ -0,0 +1,6 @@ + +robur

Published: 2017-11-05 (last updated: 2021-11-16)

You can reach us by mail at team@robur.coop.

If you wish, you may encrypt your email with our OpenPGP key 0CBFC7AA, fingerprint: 27EB8C7B 7BC95BDC 9B4B63CD 599270C7 0CBFC7AA.

\ No newline at end of file diff --git a/Donate b/Donate new file mode 100644 index 0000000..c3a62a1 --- /dev/null +++ b/Donate @@ -0,0 +1,22 @@ + +robur

Published: 2018-04-15 (last updated: 2021-07-05)

We are passionate about creating secure and reliable open source infrastructure. We have worked on secure implementations of important applications such as 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.

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).

As Robur is a project of the nonprofit The Center For Technical Cultivation we are tax deductible in Europe.

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
+

Tax Deductibility

For Germany, you can download a general donation receipt 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.

\ No newline at end of file diff --git a/Home b/Home new file mode 100644 index 0000000..25dec7d --- /dev/null +++ b/Home @@ -0,0 +1,14 @@ + +robur

Published: 2017-09-16 (last updated: 2019-09-10)

+
+
+

R obust Infrastructure

O pen Source Projects

B ottom-up Approach

U nderscoring Security

R eliable Technology

+
+
+

\ No newline at end of file diff --git a/Our Work/Our-Approach b/Our Work/Our-Approach new file mode 100644 index 0000000..ea8e283 --- /dev/null +++ b/Our Work/Our-Approach @@ -0,0 +1,28 @@ + +Our Approach

Our Approach

Published: 2019-09-10 (last updated: 2019-09-10)

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. In addition each piece of software leverages 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, partners and 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.

If you like our approach to open source software and want to support our work please consider a donation.

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.

\ No newline at end of file diff --git a/Our Work/Projects b/Our Work/Projects new file mode 100644 index 0000000..614ae45 --- /dev/null +++ b/Our Work/Projects @@ -0,0 +1,106 @@ + +Projects

Projects

Published: 2019-09-10 (last updated: 2022-03-01)

Robur Reproducible Builds

In 2021 we in Robur have been working towards easing deployment of reproducible mirage applications. The work has been funded by the Eurepean Union under the Next Generation Internet (NGI Pointer) initiative. The result is online.

The overall goal is to push MirageOS into production in a trustworthy way. We worked on reproducible builds for Opam packages and MirageOS - with the infrastructure being reproducible itself. Reproducible builds are crucial for supply chain security - everyone can reproduce the exact same binary (by using the same sources and environment), without reproducible builds we would not publish binaries.

Reproducible builds are also great for fleet management: by inspecting the hash of the binary that is executed, we can figure out which versions of which libraries are in the unikernel - and suggest updates if newer builds are available or if a used library has a security flaw -- albatross-client-local update my-unikernel is everything needed for an update.

Several ready-to-use MirageOS unikernels are built on a daily basis - ranging from authoritative DNS servers (secondary, let's encrypt DNS solver), DNS-and-DHCP service (similar to dnsmasq), TLS reverse proxy, Unipi - a web server that delivers content from a git repository, DNS resolver, CalDAV server, and of course your own MirageOS unikernel.

Bitcoin Piñata

The Bitcoin Piñata is a transparent bug bounty: it holds the private key for a bitcoin wallet. It is a MirageOS unikernel designed to test our TLS and all underlying transport implementations.

Its open communication channels are HTTP and HTTPS, and a TLS client and TLS server endpoint, all written in OCaml. The cryptographic material for TLS is generated on startup in the Piñata and is supposed to never leave it. However, if an attacker manages to establish a mutually authenticated (using certificates) TLS channel, the private key to the bitcoin wallet is transmitted over this channel, and the attacker gains access to the bait (the bitcoins).

The project was launched on February 10th 2015. At this time friends from the IPredator project lent us 10 bitcoins (back then worth ~2000 EUR) for the bait. By 2018 no one had successfully cracked the Piñata and the bitcoins, by this point worth ~200 000 EUR, were repurposed for other projects, however the project remains live, with a small amount of bitcoins in it, for anyone wishing to try to crack it.

Hannes Mehnert and David Kaloper-Meršinjak designed the Bitcoin Piñata to attract security professionals to look into our TLS stack, developed purely in OCaml since early 2014.

More technical information:

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.

The codebase is thousands of lines of code smaller than equivalent implementations and we did not use many external libraries, and those we had to use we read carefully to avoid security issues.

The attack surface is any part of the unikernel (or deployment) - anything allowing you to get a valid certificate (signed by the cryptographic material which shouldn't leave the Piñata), or reading the memory location where the private key to the bitcoin wallet is stored, an exploitable flaw in any software layer (OCaml runtime, virtual network device, TCP/IP stack, TLS library, X.509 validation, or elsewhere), or anything else.

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.

The source code of the Piñata is open source and even the running binary (without the private bitcoin wallet key) is published in the git repository.

Further links about the Bitcoin Piñata:

CalDAV Server

The CalDAV server is a protocol for synchronizing calendars. Our goal was to develop a calendar server that is robust and less complex to configure and maintain than other services, allowing more people to run their own digital infrastructure.

The CalDAV server project began in 2017 when Stefanie Schirmer and Hannes Mehnert got a grant from The Prototype Fund for developing a CalDAV server (RFC 4791) over a period of 6 months. After that funding period, Tarides sponsored us further, allowing us to achieve the current status of the CalDAV server.

Currently all basic features of a calendar are implemented, for example "please add this event to the calendar", and "modify the weekly meeting from now on to start half an hour later", and it is tested with a variety of CalDAV clients.

calendar.robur.coop is a live test server with the calDavZAP web user interface, try it with any user and any password (first come first serve), it persists to a remote git repository.

Our CalDAV server has a very small codebase which provides a number of security benefits and it stores all the data in git so there is a history of changes, it can easily be exported and converted to and from other formats, and if a client behaves badly (by removing entries they cannot deal with), this can be tracked and reverted.

We would like to develop the CalDAV server further, adding notifications about updates and invitations sent via Mail (as described in RFC 6638). We also aim to integrate the related protocol CardDAV (address book), which could be integrated into the same unikernel.

If you are interested in supporting further work on the CalDAV server through a donation, with a grant, or require additional features to be implemented to accommodate your project’s needs please get in touch with us!

More technical information:

Based on existing HTTP and REST libraries, we developed a WebDAV library adequate for CalDAV (e.g. no locks, but ACLs, reports). The REST library needed some extensions to support more HTTP verbs that are used in WebDAV. We also developed an iCalendar (.ics, RFC 5545) decoder and encoder.

The CalDAV unikernel uses the developed libraries to serve requests from clients, which may be "what is the last update to the calendar?", or adding events or changing times of events. Access control is done by the attached metadata to the resource (i.e. only user Tim may access Tim's calendar, groups are possible). User and group (in WebDAV lingo principals) data are stored in the same storage as the calendars. For enrolling new users and groups, we provide HTTP endpoints. The administrator password is provided as boot argument.

The storage of our CalDAV unikernel can use any mirage-kv implementation, being it a non-persistent only in-memory (not too useful for a real calendar since it is not persistent), a UNIX file system (if the unikernel runs as a UNIX process), or a remote git repository (which we recommend).

The CalDAV server is open source, with the code available on GitHub for the server and calendar.

DNS

The Domain Name System is used like a phone book for the internet - it translates human-memoizable domain names (e.g. robur.coop) to machine-routable IP addresses (e.g. 198.167.222.215) and other records such as where eMail should be sent to. DNS is a fault-tolerant hierarchical decentralized key-value store with caching. DNS has been deployed on the Internet since 1987.

On the one side, the authoritative server, which has delegated responsibility for a domain, provides that mapping information (i.e. that a certain IP is the right one for a certain domain), and on the other side a resolver provides the functionality to figure out which server to request for each query a client has.

Since 2017 we have developed DNS, server, resolver, and client as a spare-time project. They serve different purposes in our ecosystem: the server is used by domains such as nqsb.io and robur.coop as an authoritative server; we use a caching resolver for our bi-annual hack retreats in Marrakesh; and the client is used by any MirageOS unikernel that needs to resolve domain names.

When developing this project we carefully considered which elements were strictly required and have ensured a minimal codebase, providing for better security and ease of use.

Since mid-August 2019 our DNS implementation replaced the existing, but incomplete and barely maintained OCaml implementation. It is released to the opam repository.

A specific use case for this project is to combine a DNS resolver with a local zone (where it acts as server), and a DHCP server - a protocol used for dynamic IP address configuration - into a single service. We recently received confirmation of a grant from Nlnet via the next generation internet initiative from the EU to develop such a service based on our DNS library.

If you are interested in supporting this work, or knowing more about it please get in touch with us.

More technical information:

Our DNS implementation handles extensions such as dynamic updates, notifications on changes, authentication of update requests, zone transfers (all useful for provisioning X509 certificates via letsencrypt.org).

Using expressive types in OCaml we can ensure that for a given query type the reply record has a specific shape: querying an address record (A) results in a set of IPv4 addresses. Encoding such invariants in the type system reduces the boilerplate (or unsafety) which is there in other implementations.

The DNS code is available on GitHub for the library and unikernels.

Firewall

Online security is vital and an important way to improve a network's or computer's security is a firewall that can block unwanted traffic going in and out. We are developing a lightweight firewall in the secure programming language OCaml that is specifically designed to be implemented in QubesOS, a security-orientated operating system.

The Qubes-Mirage-Firewall is based on a project by Thomas Leonard. It is implemented as a MirageOS unikernel, it is more lightweight and with a smaller codebase compared to the original Linux based firewall in QubesOS which has security and useability benefits.

In 2019, we received a grant from The Prototype Fund for 6 months work on this project. We would like to continue developing it further and if you wish to support this project with a donation, grant, or just want to hear more about the project please get in touch with us.

More technical information:

Thus far we have refactored the NAT library, made the firewall react to rule changes from the Qubes interface, and added a DNS client to the firewall. We added the ability to read rule changes from QubesDB. We added the ability to resolve domain names via a DNS client so that the rules can be written in a human-friendly way, and not just as computer-friendly IP addresses.

The smaller unikernel uses less memory, which is a rare resource in QubesOS, since Qubes runs many virtual machines. As opposed to the first prototype, it can react to rule changes without the need to rebuild and reboot the firewall VM.

The code for the firewall is on GitHub, but still on several branches since we recently reworked the DNS parts.

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 compatible platform or software that is looking for OpenPGP written in a secure language.

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. 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!

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.

OpenVPN

OpenVPN is a virtual private network protocol that started from a single implementation developed in C, without any specification document. Over time flaws were found in the implementation which lead to further revisions. Also several extensions were developed for coping with other needs.

This history meant that overall OpenVPN has a number of flaws and is overly complex due to revisions on revisions. We implemented only the most recent protocol version and require the current key derivation and authentication method.

We started from scratch developing it in OCaml using existing cryptographic libraries and parsers. This approach allowed us to take some design decisions that have security benefits and our codebase is minimal. We strive for compatibility of the configuration file, so our OCaml OpenVPN can be a drop-in replacement.

We began this work in 2018 with a grant from The Prototype Fund. Whilst the code is available on Github we have not released it yet as it needs further work (in terms of testing, performance evaluation).

If you are interested in supporting further work on our OpenVPN implementation through a donation, with a grant, or just want to hear more about the project please get in touch with us!

More technical information:

Our main goal is a client implementation as a MirageOS unikernel (either forwarding all traffic to a single IP address or NAT of a local network via the OpenVPN tunnel), but we also developed a UNIX client which configures a tap device on the host and adjusts the hosts routing table accordingly. We extended our protocol implementation with a server as well. Testing is done against existing OpenVPN servers.

Our implementation has stronger security promises since we do not implement old protocol versions that are brittle. In addition it is fail-hard when using the NAT unikernel: if the tunnel is down, all packets are dropped (instead of sent unencrypted). We do not support questionable configuration options and we have safe defaults for the configuration.

Solo5

Solo5 is a sandboxed (separated) execution environment built using unikernels (a.k.a. library operating systems), including but not limited to MirageOS unikernels. Conceptually it provides a common interface between the unikernel and various host operating systems or hypervisors.

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.

Currently Solo5 is ready for use by early adopters and we plan to continue developing it further, if you are interested in supporting this development with a donation or want to hear more about the project please get in touch with us.

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 the developer 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.

The software is available on Github.

\ No newline at end of file diff --git a/Our Work/Publications-and-Talks b/Our Work/Publications-and-Talks new file mode 100644 index 0000000..5138245 --- /dev/null +++ b/Our Work/Publications-and-Talks @@ -0,0 +1,49 @@ + +Publications and Talks

Publications and Talks

Published: 2019-09-10 (last updated: 2020-01-07)

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 to us.

Hannes Mehnert

Talks:

Chaos Communication Congress 2019 (36c3) - Leaving Legacy Behind
+Presenting the current state of MirageOS unikernels, with a focus on the reduction on resource usage (carbon footprint) of network services.

CERN Computing Seminar 2019 – MirageOS: robust and secure services for the cloud
+Presenting MirageOS and its advantages along with explaining several applications being developed within it.

BOB 2018 - Engineering TCP/IP with logic
+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?
+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 Communication Congress 2018 (35c3) - Domain Name System
+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:

Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API (JACM vol 66, January 2019), full paper. (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), video presentation (David Kaloper-Meršinjak, Hannes Mehnert, Anil Madhavapeddy, Peter Sewell)

Not-quite-so-broken TLS 1.3 Mechanized Conformance Checking - TLS 1.3 Ready or Not (TRON), workshop website (David Kaloper-Meršinjak and Hannes Mehnert)

Martin Lucina

Talks:

FOSDEM 2019 - Solo5: A sandboxed, re-targetable execution environment for unikernels
+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 (Dan Williams, Ricardo Koller, Martin Lucina, Nikhil Prakash)

Mindy Preston

Talks:

DevOpsDays MSN 2018 - FuzzOps
+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!! +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
+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:

Radical Networks 2019 - A Firewall for Your Radical Network (recording)
+Discusses how to give a general understanding and strategy plan for network security tailored to everyone's individual needs. Explains what a network protocol is and how we read it, including insecure and secure protocols. Looks at tools to analyze and learn about a network (e.g. wireshark, traceroute). The idea of QubesOS and how to structure your system into different Qubes and run them, focusing on configuring and testing a firewall and why it has been obscure in the past, using our [Qubes-Mirage-Firewall](/Our Work/Projects#Firewall).

Berlin Buzzwords 2018 - Your Search Service as a Composable Function
+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.

BOB Konferenz 2016 - Dynamic programming at ease - with grammars, algebras, products
+Discusses how dynamic programming is a technique to solve a combinatorial optimization problem by reducing complexity through reusing intermediate results that are stored in a table, instead of computing them again. Explores a formal framework for dynamic programming on sequences. Separating the problems of search space description, candidate description, candidate evaluation and tabulation helps us in thinking about dynamic programming.

QCon 2016 - API-first Architecture Transformation
+Talks about the case study of building an API-first architecture at Etsy. She talks about what problems prompted this drastic change, the new tools they had to build to be able to work with the new system and what mistakes they made along the way.

EnthusiastiCon 2016 - OMG building a shell in 10 minutes
+According to Wikipedia a shell script is a computer program designed to be run by a command line interpreter. Typical operations performed by shell scripts include file manipulation, program execution, and printing text. Sounds complicated? In this talk Stefanie Schirmer shows how to build a shell in ten minutes.

JSConf EU 2015 - Functional programming and curry cooking in JS
+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.

\ No newline at end of file diff --git a/Our Work/Services b/Our Work/Services new file mode 100644 index 0000000..6429a1d --- /dev/null +++ b/Our Work/Services @@ -0,0 +1,17 @@ + +Services

Services

Published: 2019-09-10 (last updated: 2019-09-10)

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 and 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 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.

\ No newline at end of file diff --git a/Our Work/Technology-Employed b/Our Work/Technology-Employed new file mode 100644 index 0000000..85e11d9 --- /dev/null +++ b/Our Work/Technology-Employed @@ -0,0 +1,62 @@ + +Technology Employed

Technology Employed

Published: 2019-09-10 (last updated: 2019-10-31)

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.

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:

+ + + + + + + +

	Linux	MirageOS
Kernel	1600	48
Runtime	689	25
Crypto	230	23
TLS	41	6
Total	2560	102

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 "standard" UNIX processes, Xen, Qubes, and Solo5 (which in turn supports numerous targets). With regards to hardware processors MirageOS compiles to native code on 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 declarative 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 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.

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 December 2016 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.

+
+
+
+

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. 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.

OCaml lends itself by default to a programming style with explicit error handling. 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 does supports exceptions, but they are not present in the type signatures [of functions] (unlike Java), and thus from the outside (e.g. when calling a function), it is not clear whether exceptions can be raised or not. For that reason, the coding style of exception-based error handling is avoided in MirageOS. Instead of relying on exceptions, we employ explicit error handling using result types and an error monad.

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, and more recently by the crypto-ledger Tezos.

\ No newline at end of file diff --git a/Our Work/index.html b/Our Work/index.html new file mode 100644 index 0000000..ca2280f --- /dev/null +++ b/Our Work/index.html @@ -0,0 +1,4 @@ + +robur

Technology Employed

Services

Publications and Talks

Projects

Our Approach

\ No newline at end of file diff --git a/Projects/Reproducible_builds b/Projects/Reproducible_builds new file mode 100644 index 0000000..1eb20ca --- /dev/null +++ b/Projects/Reproducible_builds @@ -0,0 +1,121 @@ + +Robur Reproducible Builds

Robur Reproducible Builds

Published: 2021-11-16 (last updated: 2022-09-08)

In 2021 we in Robur have been working towards easing deployment of reproducible mirage applications. The work has been funded by the European Union under the Next Generation Internet (NGI Pointer) initiative. The result is online.

Brief robur and MirageOS introduction

MirageOS is an operating system, developed in OCaml, which produces unikernels. A unikernel serves a single purpose and is a single process, i.e. only has the really needed dependencies. For example, an OpenVPN endpoint does neither include persistent storage (block device, file system) nor user management. MirageOS unikernels are developed in OCaml, a statically typed and type-safe programming language - which avoids common pitfalls from the grounds up (spatial and temporal memory safety issues).

Robur is a collective that develops MirageOS and OCaml software with open source license. It was started in 2017, and is part of the non-profit company center for the cultivation of technology. We received funding from several projects (prototypefund, NGI pointer), donations, and commercial contracts.

Deploying MirageOS unikernel

To run a MirageOS unikernel on your laptop or computer with virtualization extensions (VT-x - KVM/BHyve), you first have to install the solo5-hvt and albatross packages. Afterwards you need to setup a virtual network switch (a bridge interface) where your unikernels will communicate, and forwarding.

Host system package installation

For Debian and Ubuntu systems, we provide package repositories. Browse the dists folder for one matching your distribution, and add it to /etc/apt/sources.list:

$ wget -q -O /etc/apt/trusted.gpg.d/apt.robur.coop.gpg https://apt.robur.coop/gpg.pub
+$ echo "deb https://apt.robur.coop ubuntu-20.04 main" >> /etc/apt/sources.list # replace ubuntu-20.04 with e.g. debian-11 on a debian buster machine
+$ apt update
+$ apt install solo5-hvt albatross
+

On FreeBSD:

$ fetch -o /usr/local/etc/pkg/robur.pub https://pkg.robur.coop/repo.pub # download RSA public key
+$ echo 'robur: {
+  url: "https://pkg.robur.coop/${ABI}",
+  mirror_type: "srv",
+  signature_type: "pubkey",
+  pubkey: "/usr/local/etc/pkg/robur.pub",
+  enabled: yes
+}' > /usr/local/etc/pkg/repos/robur.conf # Check https://pkg.robur.coop which ABI are available
+$ pkg update
+$ pkg install solo5-hvt albatross
+

For other distributions and systems we do not (yet?) provide binary packages. You can compile and install them using opam (opam install solo5 albatross). Get in touch if you're keen on adding some other distribution to our reproducible build infrastructure.

There is no configuration needed. Start the albatross_console and the albatross_daemon service (via systemctl daemon-reload ; systemctl start albatross_daemon on Linux or service albatross_daemon start on FreeBSD). Executing albatross-client-local info should return success (exit code 0) and no running unikernel. You may need to be in the albatross group, or change the permissions of the Unix domain socket (/run/albatross/util/vmmd.sock on Linux, /var/run/albatross/util/vmmd.sock on FreeBSD).

To check that albatross works, get the latest hello world unikernel and run it:

$ wget https://builds.robur.coop/job/hello/build/latest/bin/hello.hvt
+$ albatross-client-local console my-hello-unikernel & # this is sent to the background since it waits and displays the console of the unikernel named "my-hello-unikernel"
+$ albatross-client-local create my-hello-unikernel hello.hvt # this returns once the unikernel image has been transmitted to the albatross daemon
+$ albatross-client-local create --arg='--hello="Hello,\ my\ unikernel" my-hello-unikernel hello.hvt # executes the same unikernel, but passes the boot parameter "--hello"
+$ fg # back to albatross-client-local console
+$ Ctrl-C # kill that process
+

Voila, we have a working albatross installation. Albatross also supports a remote client (using a TLS handshake) albatross-client-bistro, monitoring of unikernels (albatross_stat and albatross_influx services), and a TLS endpoint (via inetd with albatross-tls-inetd).

Network for your unikernel

Next we want to setup networking for our unikernels. We use a so-called "bridge" interface for this, which is a virtual network switch where you connect "tap" interfaces (layer 2 ethernet devices). A MirageOS unikernel uses tap interfaces for communication. We give our bridge the name "service" (and for example for monitoring and management you may want to setup another bridge "management").

If you're using a network manager that is capable of setting up bridge interfaces, use that interface.

If not, on Linux you can add the following to /etc/network/interfaces (the reason for adding a dummy interface to the bridge is that otherwise Linux uses the mac address of the first connected tap interface, and there'll be rather confusing issues):

auto service
+# Host-only bridge
+iface service inet manual
+    up ip link add service-master address 02:00:00:00:00:01 type dummy
+    up ip link set dev service-master up
+    up ip link add service type bridge
+    up ip link set dev service-master master service
+    up ip addr add 10.0.42.1/24 dev service
+    up ip link set dev service up
+    down ip link del service
+    down ip link del service-master
+

On FreeBSD, add the following to /etc/rc.conf:

cloned_interfaces="bridge0"
+ifconfig_bridge0_name="service"
+ifconfig_service="inet 10.0.42.1/24"
+

Afterwards either restart your system or re-run the service scripts to have the bridge setup in your running system.

To check that the networking works, get the latest static website unikernel and run it:

$ wget https://builds.robur.coop/job/static-website/build/latest/bin/https.hvt
+$ albatross-client-local console my-website & # this is sent to the background since it waits and displays the console of the unikernel named "my-website"
+$ albatross-client-local create --net=service --arg='--ipv4=10.0.42.2/24' my-website https.hvt # this returns once the unikernel image has been transmitted to the albatross daemon
+$ ping 10.0.42.2 # should receive answers
+$ open http://10.0.42.2 # in your browser - also https://10.0.42.2 (you'll get a certificate warning)
+$ wget http://10.0.42.2/ # should download the Hello Mirage world!
+$ wget --no-check-certificate https://10.0.42.2/ # should also download the Hello Mirage world!
+$ fg # back to albatross-client-local console
+$ Ctrl-C # kill that process
+$ albatross-client-local destroy my-website # kills the unikernel
+

When you reached this point, you have successfully launched a MirageOS unikernel, and are able to communicate from your computer with it. This uses the OCaml networking stack, and the host bridge interface.

Routing and Internet

Your unikernel may want to communicate not only with your host, but also with the Internet. The other way around is also important (the Internet wants to talk with your unikernel).

There are several options, depending on your setup:

Your unikernel will be masqueraded (using NAT) - some ports may be forwarded to the unikernel, +
Your computer has several public IP addresses (and put the ethernet device with the ethernet cable on the bridge) and there is an external router, +
Your computer acts as a router for a subnet. +

NAT

This won't allow your unikernel to be reachable from the outside.You'll need to:

enable IPv4 forwarding +
add a firewall rule +

On Linux:

$ echo "1" > /proc/sys/net/ipv4/ip_forward # enables IP forwarding
+$ iptables -t nat -A POSTROUTING -o enp0s20f0 -j MASQUERADE # replace enp0s20f0 with your network interface
+

On FreeBSD:

$ echo 'gateway_enable="YES"' >> /etc/rc.conf # enable IP forwarding
+$ echo 'pf_enable="YES"' >> /etc/rc.conf # enables the packet filter
+$ echo "nat pass on em0 inet from 10.0.42.0/24 to any -> (em0)" >> /etc/pf.conf # replace em0 with your ethernet interface)
+

Public IP addresses

To put your unikernels on the same network as your host system, add that external network interface to the bridge:

On Linux, add up ip link set dev enp0s20f0 master service in /etc/network/interfaces (replace enp0s20f0 with your ethernet interface). +On FreeBSD, add ifconfig_service="addm em0" to /etc/rc.conf (replace em0 with your ethernet interface).

Router

Enable IPv4 forwarding, and setup one IP address on the bridge (replacing the 10.0.42.1/24 above).

Unikernel execution

Let's test that your unikernels have access to the Internet by using the traceroute unikernel:

$ wget https://builds.robur.coop/job/traceroute/build/latest/bin/traceroute.hvt
+$ albatross-client-local console my-traceroute & # this is sent to the background since it waits and displays the console of the unikernel named "my-traceroute"
+$ albatross-client-local create --net=service --arg='--ipv4=10.0.42.2/24' --arg='--ipv4-gateway=10.0.42.1' my-traceroute traceroute.hvt # the IP configuration depends on your setup, use your public IP address and actual router IP if you've set it up.
+$ fg # back to albatross-client-local console
+$ Ctrl-C # kill that process
+

That's it. Albatross has more features, such as block devices, multiple bridges (for management, private networks, ...), restart if the unikernel exited with specific exit code, assignment of a unikernel to a specific CPU. It also has remote command execution and resource limits (you can allow your friends to execute a number of unikernels with limited memory and block storage accessing only some of your bridges). There is a daemon to collect metrics and report them to Grafana (via Telegraf and Influx). MirageOS unikernels also support IPv6, you're not limited to legacy IP.

\ No newline at end of file diff --git a/Projects/index.html b/Projects/index.html new file mode 100644 index 0000000..e9342f3 --- /dev/null +++ b/Projects/index.html @@ -0,0 +1,4 @@ + +robur

Robur Reproducible Builds

\ No newline at end of file diff --git a/atom b/atom new file mode 100644 index 0000000..8fee11f --- /dev/null +++ b/atom @@ -0,0 +1,418 @@ +urn:uuid:8167ecfe-9676-11e7-8dc1-68f728e7bbbcrobur2022-09-13T09:15:34-00:002021-11-16T15:06:35-00:00<p>In 2021 we in <a href="https://robur.coop/">Robur</a> have been working towards easing deployment of reproducible mirage applications. The work has been funded by the European Union under the <a href="https://pointer.ngi.eu/">Next Generation Internet (NGI Pointer) initiative</a>. The result is <a href="https://builds.robur.coop">online</a>.</p> +<p>The overall goal is to push MirageOS into production in a trustworthy way. We worked on reproducible builds for <a href="https://opam.ocaml.org">Opam</a> packages and <a href="https://mirageos.org">MirageOS</a> - with the infrastructure being reproducible itself. Reproducible builds are crucial for supply chain security - everyone can reproduce the exact same binary (by using the same sources and environment), without reproducible builds we would not publish binaries.</p> +<p>Reproducible builds are also great for fleet management: by inspecting the hash of the binary that is executed, we can figure out which versions of which libraries are in the unikernel - and suggest updates if newer builds are available or if a used library has a security flaw -- <code>albatross-client-local update my-unikernel</code> is everything needed for an update.</p> +<p>Several ready-to-use MirageOS unikernels are built on a daily basis - ranging from <a href="https://builds.robur.coop/job/dns-primary-git/">authoritative DNS servers</a> (<a href="https://builds.robur.coop/job/dns-secondary/">secondary</a>, <a href="https://builds.robur.coop/job/dns-letsencrypt-secondary/">let's encrypt DNS solver</a>), <a href="https://builds.robur.coop/job/dnsvizor/">DNS-and-DHCP service (similar to dnsmasq)</a>, <a href="https://builds.robur.coop/job/tlstunnel/">TLS reverse proxy</a>, <a href="https://builds.robur.coop/job/unipi/">Unipi - a web server that delivers content from a git repository</a>, <a href="https://builds.robur.coop/job/dns-resolver/">DNS resolver</a>, <a href="https://builds.robur.coop/job/caldav/">CalDAV server</a>, and of course your own MirageOS unikernel.</p> +<h2>Brief robur and MirageOS introduction</h2> +<p><a href="https://mirageos.org">MirageOS</a> is an operating system, developed in OCaml, which produces unikernels. A unikernel serves a single purpose and is a single process, i.e. only has the really needed dependencies. For example, an OpenVPN endpoint does neither include persistent storage (block device, file system) nor user management. MirageOS unikernels are developed in <a href="https://ocaml.org">OCaml</a>, a statically typed and type-safe programming language - which avoids common pitfalls from the grounds up (spatial and temporal memory safety issues).</p> +<p><a href="https://robur.coop">Robur</a> is a collective that develops MirageOS and OCaml software with open source license. It was started in 2017, and is part of the non-profit company <a href="https://techcultivation.org">center for the cultivation of technology</a>. We received funding from several projects (<a href="https://prototypefund.de">prototypefund</a>, <a href="https://pointer.ngi.eu">NGI pointer</a>), donations, and commercial contracts.</p> +<h2>Deploying MirageOS unikernel</h2> +<p>To run a MirageOS unikernel on your laptop or computer with virtualization extensions (VT-x - KVM/BHyve), you first have to install the <code>solo5-hvt</code> and <code>albatross</code> packages. Afterwards you need to setup a virtual network switch (a bridge interface) where your unikernels will communicate, and forwarding.</p> +<h3>Host system package installation</h3> +<p>For Debian and Ubuntu systems, we provide package repositories. Browse the <a href="https://apt.robur.coop/dists">dists</a> folder for one matching your distribution, and add it to <code>/etc/apt/sources.list</code>:</p> +<pre><code>$ wget -q -O /etc/apt/trusted.gpg.d/apt.robur.coop.gpg https://apt.robur.coop/gpg.pub +$ echo "deb https://apt.robur.coop ubuntu-20.04 main" >> /etc/apt/sources.list # replace ubuntu-20.04 with e.g. debian-11 on a debian buster machine +$ apt update +$ apt install solo5-hvt albatross +</code></pre> +<p>On FreeBSD:</p> +<pre><code>$ fetch -o /usr/local/etc/pkg/robur.pub https://pkg.robur.coop/repo.pub # download RSA public key +$ echo 'robur: { + url: "https://pkg.robur.coop/${ABI}", + mirror_type: "srv", + signature_type: "pubkey", + pubkey: "/usr/local/etc/pkg/robur.pub", + enabled: yes +}' > /usr/local/etc/pkg/repos/robur.conf # Check https://pkg.robur.coop which ABI are available +$ pkg update +$ pkg install solo5-hvt albatross +</code></pre> +<p>For other distributions and systems we do not (yet?) provide binary packages. You can compile and install them using <a href="https://opam.ocaml.org">opam</a> (<code>opam install solo5 albatross</code>). Get in touch if you're keen on adding some other distribution to our reproducible build infrastructure.</p> +<p>There is no configuration needed. Start the <code>albatross_console</code> and the <code>albatross_daemon</code> service (via <code>systemctl daemon-reload ; systemctl start albatross_daemon</code> on Linux or <code>service albatross_daemon start</code> on FreeBSD). Executing <code>albatross-client-local info </code> should return success (exit code 0) and no running unikernel. You may need to be in the albatross group, or change the permissions of the Unix domain socket (<code>/run/albatross/util/vmmd.sock</code> on Linux, <code>/var/run/albatross/util/vmmd.sock</code> on FreeBSD).</p> +<p>To check that albatross works, get the latest hello world unikernel and run it:</p> +<pre><code>$ wget https://builds.robur.coop/job/hello/build/latest/bin/hello.hvt +$ albatross-client-local console my-hello-unikernel & # this is sent to the background since it waits and displays the console of the unikernel named "my-hello-unikernel" +$ albatross-client-local create my-hello-unikernel hello.hvt # this returns once the unikernel image has been transmitted to the albatross daemon +$ albatross-client-local create --arg='--hello="Hello,\ my\ unikernel" my-hello-unikernel hello.hvt # executes the same unikernel, but passes the boot parameter "--hello" +$ fg # back to albatross-client-local console +$ Ctrl-C # kill that process +</code></pre> +<p>Voila, we have a working albatross installation. Albatross also supports a remote client (using a TLS handshake) <code>albatross-client-bistro</code>, monitoring of unikernels (<code>albatross_stat</code> and <code>albatross_influx</code> services), and a TLS endpoint (via inetd with <code>albatross-tls-inetd</code>).</p> +<h3>Network for your unikernel</h3> +<p>Next we want to setup networking for our unikernels. We use a so-called "bridge" interface for this, which is a virtual network switch where you connect "tap" interfaces (layer 2 ethernet devices). A MirageOS unikernel uses tap interfaces for communication. We give our bridge the name "service" (and for example for monitoring and management you may want to setup another bridge "management").</p> +<p>If you're using a network manager that is capable of setting up bridge interfaces, use that interface.</p> +<p>If not, on Linux you can add the following to <code>/etc/network/interfaces</code> (the reason for adding a dummy interface to the bridge is that otherwise Linux uses the mac address of the first connected tap interface, and there'll be rather confusing issues):</p> +<pre><code>auto service +# Host-only bridge +iface service inet manual + up ip link add service-master address 02:00:00:00:00:01 type dummy + up ip link set dev service-master up + up ip link add service type bridge + up ip link set dev service-master master service + up ip addr add 10.0.42.1/24 dev service + up ip link set dev service up + down ip link del service + down ip link del service-master +</code></pre> +<p>On FreeBSD, add the following to <code>/etc/rc.conf</code>:</p> +<pre><code>cloned_interfaces="bridge0" +ifconfig_bridge0_name="service" +ifconfig_service="inet 10.0.42.1/24" +</code></pre> +<p>Afterwards either restart your system or re-run the service scripts to have the bridge setup in your running system.</p> +<p>To check that the networking works, get the latest static website unikernel and run it:</p> +<pre><code>$ wget https://builds.robur.coop/job/static-website/build/latest/bin/https.hvt +$ albatross-client-local console my-website & # this is sent to the background since it waits and displays the console of the unikernel named "my-website" +$ albatross-client-local create --net=service --arg='--ipv4=10.0.42.2/24' my-website https.hvt # this returns once the unikernel image has been transmitted to the albatross daemon +$ ping 10.0.42.2 # should receive answers +$ open http://10.0.42.2 # in your browser - also https://10.0.42.2 (you'll get a certificate warning) +$ wget http://10.0.42.2/ # should download the Hello Mirage world! +$ wget --no-check-certificate https://10.0.42.2/ # should also download the Hello Mirage world! +$ fg # back to albatross-client-local console +$ Ctrl-C # kill that process +$ albatross-client-local destroy my-website # kills the unikernel +</code></pre> +<p>When you reached this point, you have successfully launched a MirageOS unikernel, and are able to communicate from your computer with it. This uses the OCaml networking stack, and the host bridge interface.</p> +<h2>Routing and Internet</h2> +<p>Your unikernel may want to communicate not only with your host, but also with the Internet. The other way around is also important (the Internet wants to talk with your unikernel).</p> +<p>There are several options, depending on your setup:</p> +<ul> +<li>Your unikernel will be masqueraded (using <a href="https://en.wikipedia.org/wiki/Network_address_translation">NAT</a>) - some ports may be forwarded to the unikernel, +</li> +<li>Your computer has several public IP addresses (and put the ethernet device with the ethernet cable on the bridge) and there is an external router, +</li> +<li>Your computer acts as a router for a subnet. +</li> +</ul> +<h3>NAT</h3> +<p>This won't allow your unikernel to be reachable from the outside.You'll need to:</p> +<ul> +<li>enable IPv4 forwarding +</li> +<li>add a firewall rule +</li> +</ul> +<p>On Linux:</p> +<pre><code>$ echo "1" > /proc/sys/net/ipv4/ip_forward # enables IP forwarding +$ iptables -t nat -A POSTROUTING -o enp0s20f0 -j MASQUERADE # replace enp0s20f0 with your network interface +</code></pre> +<p>On FreeBSD:</p> +<pre><code>$ echo 'gateway_enable="YES"' >> /etc/rc.conf # enable IP forwarding +$ echo 'pf_enable="YES"' >> /etc/rc.conf # enables the packet filter +$ echo "nat pass on em0 inet from 10.0.42.0/24 to any -> (em0)" >> /etc/pf.conf # replace em0 with your ethernet interface) +</code></pre> +<h3>Public IP addresses</h3> +<p>To put your unikernels on the same network as your host system, add that external network interface to the bridge:</p> +<p>On Linux, add <code>up ip link set dev enp0s20f0 master service</code> in <code>/etc/network/interfaces</code> (replace enp0s20f0 with your ethernet interface). +On FreeBSD, add <code>ifconfig_service="addm em0"</code> to <code>/etc/rc.conf</code> (replace em0 with your ethernet interface).</p> +<h3>Router</h3> +<p>Enable IPv4 forwarding, and setup one IP address on the bridge (replacing the 10.0.42.1/24 above).</p> +<h2>Unikernel execution</h2> +<p>Let's test that your unikernels have access to the Internet by using the <a href="https://hannes.robur.coop/Posts/Traceroute">traceroute</a> unikernel:</p> +<pre><code>$ wget https://builds.robur.coop/job/traceroute/build/latest/bin/traceroute.hvt +$ albatross-client-local console my-traceroute & # this is sent to the background since it waits and displays the console of the unikernel named "my-traceroute" +$ albatross-client-local create --net=service --arg='--ipv4=10.0.42.2/24' --arg='--ipv4-gateway=10.0.42.1' my-traceroute traceroute.hvt # the IP configuration depends on your setup, use your public IP address and actual router IP if you've set it up. +$ fg # back to albatross-client-local console +$ Ctrl-C # kill that process +</code></pre> +<p>That's it. Albatross has more features, such as block devices, multiple bridges (for management, private networks, ...), restart if the unikernel exited with specific exit code, assignment of a unikernel to a specific CPU. It also has remote command execution and resource limits (you can allow your friends to execute a number of unikernels with limited memory and block storage accessing only some of your bridges). There is a daemon to collect metrics and report them to Grafana (via Telegraf and Influx). MirageOS unikernels also support IPv6, you're not limited to legacy IP.</p> +urn:uuid:a225bf44-9230-569f-8852-1b5d2132a749Robur Reproducible Builds2022-09-08T09:17:12-00:00canopy2019-09-10T19:40:14-00:00<h1>MirageOS</h1> +<p>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 <a href="/Our%20Work/Technology-Employed#OCaml">OCaml</a>.</p> +<p>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.</p> +<p>As an example to see how lines of code compare, here are the number of lines of code needed for different elements of our <a href="/Our%20Work/Projects#Bitcoin%20Pinata">Bitcoin Pinata</a>, measured in thousands of lines of code:</p> +<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> +<p>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.</p> +<p>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.</p> +<h4>More Technical Information on MirageOS:</h4> +<p>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.</p> +<p>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.</p> +<p>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.</p> +<p>MirageOS targets "standard" UNIX processes, Xen, Qubes, and Solo5 (which in turn <a href="https://github.com/Solo5/solo5/blob/master/docs/building.md#supported-targets">supports numerous targets</a>). With regards to hardware processors MirageOS compiles to native code on ARM64, x86 and x86_64.</p> +<p>There are generally three ways to feed the virtual machine with configuration data, like network configuration or TLS certificate and key:</p> +<ul> +<li>compile the information into the virtual machine image, which requires recompilation on configuration change +</li> +<li>pass the information as boot parameters, which requires reboot on configuration change +</li> +<li>store this information in a virtual block device attached to the virtual machine. +</li> +</ul> +<p>In MirageOS we use a simple declarative 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.</p> +<p>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.</p> +<p>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.</p> +<p>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.</p> +<p>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.</p> +<p>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 December 2016 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.</p> +<br /> +<br /> +<br /> +<h1>OCaml</h1> +<p>OCaml is a mature programming language that is used both in industry (Facebook, Jane Street Capital, Docker, ahrefs, simcorp, lexifi) and academia.</p> +<p>A large reason MirageOS and Robur software have security advantages over other technical projects is the programming language used - OCaml.</p> +<p>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.</p> +<p>OCaml also helps avoid many common programming errors through automated memory management to avoid memory corruption, and type checking.</p> +<p>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.</p> +<h4>More Technical Information on OCaml:</h4> +<h3>Concepts of the Language</h3> +<p>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.</p> +<p>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.</p> +<p>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.</p> +<p>OCaml lends itself by default to a programming style with explicit error handling. 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 does supports exceptions, but they are not present in the type signatures [of functions] (unlike Java), and thus from the outside (e.g. when calling a function), it is not clear whether exceptions can be raised or not. For that reason, the coding style of exception-based error handling is avoided in MirageOS. Instead of relying on exceptions, we employ explicit error handling using result types and an error monad.</p> +<h3>Verification</h3> +<p>A large subset of the OCaml semantics has been mechanically proven sound in a proof assistant.</p> +<p>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).</p> +<h3>Compilation</h3> +<p>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.</p> +<p>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).</p> +<p>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.</p> +<h3>Further Information</h3> +<p>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 <a href="https://queue.acm.org/detail.cfm?id=2038036">OCaml for the masses</a>, and more recently by the crypto-ledger <a href="https://tezos.com/static/position_paper-841a0a56b573afb28da16f6650152fb4.pdf">Tezos</a>.</p> +urn:uuid:a4887de7-8629-5578-836f-d31b51fe75aaTechnology Employed2019-10-31T12:06:40-00:00canopy2019-09-10T19:40:14-00:00<p>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.</p> +<h3>Design</h3> +<p>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.</p> +<p>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.</p> +<p>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.</p> +<h3>Develop</h3> +<p>Working with <a href="/Our%20Work/Technology-Employed#OCaml">OCaml</a> and <a href="/Our%20Work/Technology-Employed#MirageOS">MirageOS</a> we can develop specific applications that give you high assurance of their security and functionality, which seamlessly integrate in your existing infrastructure.</p> +<p>We can also work on a full stack approach to meet your needs and help a smooth migration plan for your organization.</p> +<p>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.</p> +<h3>Audit</h3> +<p>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.</p> +<p>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.</p> +<p>Please <a href="/Contact">contact us</a> 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.</p> +urn:uuid:a4887de7-8629-5578-836f-d31b51fe75aaServices2019-09-10T22:09:34-00:00canopy2019-09-10T19:40:14-00:00<p>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 <a href="/Contact">reach out</a> to us.</p> +<h1>Hannes Mehnert</h1> +<h3>Talks:</h3> +<p>Chaos Communication Congress 2019 (36c3) - <a href="https://media.ccc.de/v/36c3-11172-leaving_legacy_behind">Leaving Legacy Behind</a><br /> +Presenting the current state of MirageOS unikernels, with a focus on the reduction on resource usage (carbon footprint) of network services.</p> +<p>CERN Computing Seminar 2019 – <a href="https://cds.cern.ch/record/2674523">MirageOS: robust and secure services for the cloud</a><br /> +Presenting MirageOS and its advantages along with explaining several applications being developed within it.</p> +<p>BOB 2018 - <a href="https://www.youtube.com/watch?v=AYDws2Nqcgs">Engineering TCP/IP with logic</a><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, re-transmission, etc.</p> +<p>BornHack 2018 - <a href="https://www.youtube.com/watch?v=QtPUCC6KaWo">MirageOS: what did we achieve in the last year?</a><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.</p> +<p>Chaos Communication Congress 2018 (35c3) - <a href="https://media.ccc.de/v/35c3-9674-domain_name_system">Domain Name System</a><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 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.</p> +<h3>Publications:</h3> +<p><a href="https://dl.acm.org/citation.cfm?id=3243650">Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API (JACM vol 66, January 2019)</a>, <a href="https://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf">full paper.</a> (Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, Keith Wansbrough)</p> +<p><a href="https://usenix15.nqsb.io">Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation (Usenix security 2015)</a>, <a href="https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/kaloper-mersinjak">video presentation</a> (David Kaloper-Meršinjak, Hannes Mehnert, Anil Madhavapeddy, Peter Sewell)</p> +<p><a href="https://tron.nqsb.io">Not-quite-so-broken TLS 1.3 Mechanized Conformance Checking - TLS 1.3 Ready or Not (TRON)</a>, <a href="https://www.ndss-symposium.org/ndss2016/tron-workshop-programme/">workshop website</a> (David Kaloper-Meršinjak and Hannes Mehnert)</p> +<h1>Martin Lucina</h1> +<h3>Talks:</h3> +<p>FOSDEM 2019 - <a href="https://archive.fosdem.org/2019/schedule/event/solo5_unikernels/">Solo5: A sandboxed, re-targetable execution environment for unikernels</a><br /> +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.</p> +<h3>Publications:</h3> +<p><a href="https://dl.acm.org/citation.cfm?id=3267845">Unikernels as Processes - ACM Symposium on Cloud Computing 2018</a> (Dan Williams, Ricardo Koller, Martin Lucina, Nikhil Prakash)</p> +<h1>Mindy Preston</h1> +<h3>Talks:</h3> +<p>DevOpsDays MSN 2018 - <a href="https://www.youtube.com/watch?v=BtJsakoXxdY">FuzzOps</a><br /> +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.</p> +<p>Confreaks 2017 - <a href="https://www.youtube.com/watch?v=enRY9jd0IJw">DHCP: IT’S MOSTLY YELLING!!</a> +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.</p> +<p>Strange Loop 2015 - <a href="https://www.youtube.com/watch?v=GNc1t6Q5Dls">Non-Imperative Network Programming</a><br /> +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.</p> +<h1>Stefanie Schirmer</h1> +<h3>Talks:</h3> +<p>Radical Networks 2019 - <a href="https://radicalnetworks.org/participants/stefanie-schirmer/">A Firewall for Your Radical Network</a> (<a href="https://livestream.com/internetsociety/radnets19/videos/197991963">recording</a>)<br /> +Discusses how to give a general understanding and strategy plan for network security tailored to everyone's individual needs. Explains what a network protocol is and how we read it, including insecure and secure protocols. Looks at tools to analyze and learn about a network (e.g. wireshark, traceroute). The idea of QubesOS and how to structure your system into different Qubes and run them, focusing on configuring and testing a firewall and why it has been obscure in the past, using our [Qubes-Mirage-Firewall](/Our Work/Projects#Firewall).</p> +<p>Berlin Buzzwords 2018 - <a href="https://www.youtube.com/watch?v=4Yag3SrAMnI">Your Search Service as a Composable Function</a><br /> +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.</p> +<p>BOB Konferenz 2016 - <a href="https://bobkonf.de/2016/schirmer.html">Dynamic programming at ease - with grammars, algebras, products</a><br /> +Discusses how dynamic programming is a technique to solve a combinatorial optimization problem by reducing complexity through reusing intermediate results that are stored in a table, instead of computing them again. Explores a formal framework for dynamic programming on sequences. Separating the problems of search space description, candidate description, candidate evaluation and tabulation helps us in thinking about dynamic programming.</p> +<p>QCon 2016 - <a href="https://www.infoq.com/presentations/etsy-api/">API-first Architecture Transformation</a><br /> +Talks about the case study of building an API-first architecture at Etsy. She talks about what problems prompted this drastic change, the new tools they had to build to be able to work with the new system and what mistakes they made along the way.</p> +<p>EnthusiastiCon 2016 - <a href="https://www.youtube.com/watch?v=k6TTj4C0LF0">OMG building a shell in 10 minutes</a><br /> +According to Wikipedia a shell script is a computer program designed to be run by a command line interpreter. Typical operations performed by shell scripts include file manipulation, program execution, and printing text. Sounds complicated? In this talk Stefanie Schirmer shows how to build a shell in ten minutes.</p> +<p>JSConf EU 2015 - <a href="https://www.youtube.com/watch?v=6Qx5ZAbfqjo">Functional programming and curry cooking in JS</a><br /> +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.</p> +urn:uuid:a4887de7-8629-5578-836f-d31b51fe75aaPublications and Talks2020-01-07T11:22:12-00:00canopy2019-09-10T19:40:14-00:00<h1>Robur Reproducible Builds</h1> +<p>In 2021 we in <a href="https://robur.coop/">Robur</a> have been working towards easing deployment of reproducible mirage applications. The work has been funded by the Eurepean Union under the <a href="https://pointer.ngi.eu/">Next Generation Internet (NGI Pointer) initiative</a>. The result is <a href="https://builds.robur.coop">online</a>.</p> +<p>The overall goal is to push MirageOS into production in a trustworthy way. We worked on reproducible builds for <a href="https://opam.ocaml.org">Opam</a> packages and <a href="https://mirageos.org">MirageOS</a> - with the infrastructure being reproducible itself. Reproducible builds are crucial for supply chain security - everyone can reproduce the exact same binary (by using the same sources and environment), without reproducible builds we would not publish binaries.</p> +<p>Reproducible builds are also great for fleet management: by inspecting the hash of the binary that is executed, we can figure out which versions of which libraries are in the unikernel - and suggest updates if newer builds are available or if a used library has a security flaw -- <code>albatross-client-local update my-unikernel</code> is everything needed for an update.</p> +<p>Several ready-to-use MirageOS unikernels are built on a daily basis - ranging from <a href="https://builds.robur.coop/job/dns-primary-git/">authoritative DNS servers</a> (<a href="https://builds.robur.coop/job/dns-secondary/">secondary</a>, <a href="https://builds.robur.coop/job/dns-letsencrypt-secondary/">let's encrypt DNS solver</a>), <a href="https://builds.robur.coop/job/dnsvizor/">DNS-and-DHCP service (similar to dnsmasq)</a>, <a href="https://builds.robur.coop/job/tlstunnel/">TLS reverse proxy</a>, <a href="https://builds.robur.coop/job/unipi/">Unipi - a web server that delivers content from a git repository</a>, <a href="https://builds.robur.coop/job/dns-resolver/">DNS resolver</a>, <a href="https://builds.robur.coop/job/caldav/">CalDAV server</a>, and of course your own MirageOS unikernel.</p> +<p><a href="/Projects/Reproducible_builds">read more</a></p> +<h1>Bitcoin Piñata</h1> +<p>The <a href="http://ownme.ipredator.se">Bitcoin Piñata</a> is a transparent <a href="https://en.wikipedia.org/wiki/Bug_bounty_program">bug bounty</a>: it holds the private key for a bitcoin wallet. It is a <a href="/Our%20Work/Technology-Employed#MirageOS">MirageOS unikernel</a> designed to test our TLS and all underlying transport implementations.</p> +<p>Its open communication channels are HTTP and HTTPS, and a TLS client and TLS server endpoint, all written in <a href="/Our%20Work/Technology-Employed#OCaml">OCaml</a>. The cryptographic material for TLS is generated on startup in the Piñata and is supposed to never leave it. However, if an attacker manages to establish a mutually authenticated (using certificates) TLS channel, the private key to the bitcoin wallet is transmitted over this channel, and the attacker gains access to the bait (the bitcoins).</p> +<p>The project was <a href="https://mirage.io/announcing-bitcoin-pinata">launched</a> on February 10th 2015. At this time friends from the IPredator project lent us 10 bitcoins (back then worth ~2000 EUR) for the bait. By 2018 no one had successfully cracked the Piñata and the bitcoins, by this point worth ~200 000 EUR, were repurposed for other projects, however the project remains live, with a small amount of bitcoins in it, for anyone wishing to try to crack it.</p> +<p><a href="/About%20Us/Team">Hannes Mehnert</a> and David Kaloper-Meršinjak designed the Bitcoin Piñata to attract security professionals to look into our <a href="https://en.wikipedia.org/wiki/Transport_Layer_Security">TLS</a> stack, developed purely in OCaml since early 2014.</p> +<h4>More technical information:</h4> +<p>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.</p> +<p>The codebase is <a href="/Our%20Work/Technology-Employed#MirageOS">thousands of lines of code smaller</a> than equivalent implementations and we did not use many external libraries, and those we had to use we read carefully to avoid security issues.</p> +<p>The attack surface is any part of the unikernel (or deployment) - anything allowing you to get a valid certificate (signed by the cryptographic material which shouldn't leave the Piñata), or reading the memory location where the private key to the bitcoin wallet is stored, an exploitable flaw in any software layer (OCaml runtime, virtual network device, TCP/IP stack, TLS library, X.509 validation, or elsewhere), or anything else.</p> +<p>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.</p> +<p>The source code of the Piñata is <a href="https://github.com/mirleft/btc-pinata">open source</a> and even the running binary (without the private bitcoin wallet key) is published in the git repository.</p> +<p>Further links about the Bitcoin Piñata:</p> +<ul> +<li><a href="https://mirage.io/blog/bitcoin-pinata-results">Statistics after 5 months</a> +</li> +<li><a href="https://somerandomidiot.com/blog/2018/04/17/whacking-the-bitcoin-pinata/">Post about whacking the pinata</a> +</li> +<li><a href="https://hannes.nqsb.io/Posts/Pinata">Evaluation 3 years later</a> +</li> +<li><a href="https://usenix15.nqsb.io">Usenix security research paper on TLS stack</a> +</li> +</ul> +<h1>CalDAV Server</h1> +<p>The CalDAV server is a protocol for synchronizing calendars. Our goal was to develop a calendar server that is robust and less complex to configure and maintain than other services, allowing more people to run their own digital infrastructure.</p> +<p>The CalDAV server project began in 2017 when <a href="/About%20Us/Team">Stefanie Schirmer and Hannes Mehnert</a> got a grant from <a href="https://prototypefund.de">The Prototype Fund</a> for developing a CalDAV server (RFC 4791) over a period of 6 months. After that funding period, <a href="https://tarides.com">Tarides</a> sponsored us further, allowing us to achieve the current status of the CalDAV server.</p> +<p>Currently all basic features of a calendar are implemented, for example "please add this event to the calendar", and "modify the weekly meeting from now on to start half an hour later", and it is tested with a variety of CalDAV clients.</p> +<p><a href="https://calendar.robur.coop">calendar.robur.coop</a> is a live test server with the <a href="https://www.inf-it.com/open-source/clients/caldavzap/">calDavZAP</a> web user interface, try it with any user and any password (first come first serve), it persists to a remote git repository.</p> +<p>Our CalDAV server has a very small codebase which provides a number of security benefits and it stores all the data in git so there is a history of changes, it can easily be exported and converted to and from other formats, and if a client behaves badly (by removing entries they cannot deal with), this can be tracked and reverted.</p> +<p>We would like to develop the CalDAV server further, adding notifications about updates and invitations sent via Mail (as described in <a href="https://tools.ietf.org/html/rfc6638">RFC 6638</a>). We also aim to integrate the related protocol CardDAV (address book), which could be integrated into the same unikernel.</p> +<p>If you are interested in supporting further work on the CalDAV server through a <a href="/Donate">donation</a>, with a grant, or require additional features to be implemented to accommodate your project’s needs please <a href="/Contact">get in touch with us</a>!</p> +<h4>More technical information:</h4> +<p>Based on existing HTTP and REST libraries, we developed a WebDAV library adequate for CalDAV (e.g. no locks, but ACLs, reports). The REST library needed some extensions to support more HTTP verbs that are used in WebDAV. We also developed an iCalendar (.ics, RFC 5545) decoder and encoder.</p> +<p>The CalDAV unikernel uses the developed libraries to serve requests from clients, which may be "what is the last update to the calendar?", or adding events or changing times of events. Access control is done by the attached metadata to the resource (i.e. only user Tim may access Tim's calendar, groups are possible). User and group (in WebDAV lingo principals) data are stored in the same storage as the calendars. For enrolling new users and groups, we provide HTTP endpoints. The administrator password is provided as boot argument.</p> +<p>The storage of our CalDAV unikernel can use any <a href="https://github.com/mirage/mirage-kv">mirage-kv</a> implementation, being it a non-persistent only in-memory (not too useful for a real calendar since it is not persistent), a UNIX file system (if the unikernel runs as a UNIX process), or a remote git repository (which we recommend).</p> +<p>The CalDAV server is open source, with the code available on GitHub for the <a href="https://github.com/roburio/caldav">server</a> and <a href="https://github.com/roburio/icalendar">calendar</a>.</p> +<h1>DNS</h1> +<p>The Domain Name System is used like a phone book for the internet - it translates human-memoizable domain names (e.g. robur.coop) to machine-routable IP addresses (e.g. 198.167.222.215) and other records such as where eMail should be sent to. DNS is a fault-tolerant hierarchical decentralized key-value store with caching. DNS has been deployed on the Internet since 1987.</p> +<p>On the one side, the authoritative server, which has delegated responsibility for a domain, provides that mapping information (i.e. that a certain IP is the right one for a certain domain), and on the other side a resolver provides the functionality to figure out which server to request for each query a client has.</p> +<p>Since 2017 we have developed DNS, server, resolver, and client as a spare-time project. They serve different purposes in our ecosystem: the server is used by domains such as nqsb.io and robur.coop as an authoritative server; we use a caching resolver for our bi-annual hack retreats in Marrakesh; and the client is used by any MirageOS unikernel that needs to resolve domain names.</p> +<p>When developing this project we carefully considered which elements were strictly required and have ensured a minimal codebase, providing for better security and ease of use.</p> +<p>Since mid-August 2019 our DNS implementation replaced the existing, but incomplete and barely maintained <a href="/Our%20Work/Technology-Employed#OCaml">OCaml</a> implementation. It is released to the opam repository.</p> +<p>A specific use case for this project is to combine a DNS resolver with a local zone (where it acts as server), and a DHCP server - a protocol used for dynamic IP address configuration - into a single service. We recently received confirmation of a grant from Nlnet via the next generation internet initiative from the EU to develop such a service based on our DNS library.</p> +<p>If you are interested in supporting this work, or knowing more about it please <a href="/Contact">get in touch with us</a>.</p> +<h4>More technical information:</h4> +<p>Our DNS implementation handles extensions such as dynamic updates, notifications on changes, authentication of update requests, zone transfers (all useful for provisioning X509 certificates via letsencrypt.org).</p> +<p>Using expressive types in OCaml we can ensure that for a given query type the reply record has a specific shape: querying an address record (A) results in a set of IPv4 addresses. Encoding such invariants in the type system reduces the boilerplate (or unsafety) which is there in other implementations.</p> +<p>The DNS code is available on GitHub for the <a href="https://github.com/mirage/ocaml-dns">library</a> and <a href="https://github.com/roburio/unikernels">unikernels</a>.</p> +<h1>Firewall</h1> +<p>Online security is vital and an important way to improve a network's or computer's security is a firewall that can block unwanted traffic going in and out. We are developing a lightweight firewall in the secure programming language <a href="/Our%20Work/Technology-Employed#OCaml">OCaml</a> that is specifically designed to be implemented in <a href="https://www.qubes-os.org/">QubesOS</a>, a security-orientated operating system.</p> +<p>The Qubes-Mirage-Firewall is based on a project by Thomas Leonard. It is implemented as a <a href="/Our%20Work/Technology-Employed#MirageOS">MirageOS unikernel</a>, it is more lightweight and with a smaller codebase compared to the original Linux based firewall in QubesOS which has security and useability benefits.</p> +<p>In 2019, we received a grant from <a href="https://prototypefund.de">The Prototype Fund</a> for 6 months work on this project. We would like to continue developing it further and if you wish to support this project with a <a href="/Donate">donation</a>, grant, or just want to hear more about the project please <a href="/Contact">get in touch with us</a>.</p> +<h4>More technical information:</h4> +<p>Thus far we have refactored the NAT library, made the firewall react to rule changes from the Qubes interface, and added a DNS client to the firewall. We added the ability to read rule changes from QubesDB. We added the ability to resolve domain names via a DNS client so that the rules can be written in a human-friendly way, and not just as computer-friendly IP addresses.</p> +<p>The smaller unikernel uses less memory, which is a rare resource in QubesOS, since Qubes runs many virtual machines. As opposed to the first prototype, it can react to rule changes without the need to rebuild and reboot the firewall VM.</p> +<p>The code for the firewall is on <a href="https://github.com/yomimono/qubes-mirage-firewall/">GitHub</a>, but still on several branches since we recently reworked the DNS parts.</p> +<h1>OpenPGP</h1> +<p>OpenPGP is a much-used standard of encryption and is widely used to encrypt text, files and emails, amongst other things.</p> +<p>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 <a href="/Our%20Work/Technology-Employed#OCaml">secure language</a>.</p> +<p>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.</p> +<p>You can assist us in implementing more of the OpenPGP protocol through a <a href="/Donate">donation</a>. 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 <a href="/Contact">get in touch with us</a>!</p> +<h4>More technical information:</h4> +<p>Robur maintains a partial, opinionated implementation of OpenPGP version 4 (RFC 4880) and the related standards, written in OCaml and compatible with MirageOS.</p> +<p>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.</p> +<p>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).</p> +<p>The software is available <a href="https://github.com/roburio/ocaml-openpgp">on Github</a>.</p> +<h1>OpenVPN</h1> +<p>OpenVPN is a virtual private network protocol that started from a single implementation developed in C, without any specification document. Over time flaws were found in the implementation which lead to further revisions. Also several extensions were developed for coping with other needs.</p> +<p>This history meant that overall OpenVPN has a number of flaws and is overly complex due to revisions on revisions. We implemented only the most recent protocol version and require the current key derivation and authentication method.</p> +<p>We started from scratch developing it in <a href="/Our%20Work/Technology-Employed#OCaml">OCaml</a> using existing cryptographic libraries and parsers. This approach allowed us to take some design decisions that have security benefits and our codebase is minimal. We strive for compatibility of the configuration file, so our OCaml OpenVPN can be a drop-in replacement.</p> +<p>We began this work in 2018 with a grant from <a href="https://prototypefund.de">The Prototype Fund</a>. Whilst the code is available on <a href="https://github.com/roburio/openvpn">Github</a> we have not released it yet as it needs further work (in terms of testing, performance evaluation).</p> +<p>If you are interested in supporting further work on our OpenVPN implementation through a <a href="/Donate">donation</a>, with a grant, or just want to hear more about the project please <a href="/Contact">get in touch with us</a>!</p> +<h4>More technical information:</h4> +<p>Our main goal is a client implementation as a MirageOS unikernel (either forwarding all traffic to a single IP address or NAT of a local network via the OpenVPN tunnel), but we also developed a UNIX client which configures a tap device on the host and adjusts the hosts routing table accordingly. We extended our protocol implementation with a server as well. Testing is done against existing OpenVPN servers.</p> +<p>Our implementation has stronger security promises since we do not implement old protocol versions that are brittle. In addition it is fail-hard when using the NAT unikernel: if the tunnel is down, all packets are dropped (instead of sent unencrypted). We do not support questionable configuration options and we have safe defaults for the configuration.</p> +<h1>Solo5</h1> +<p>Solo5 is a sandboxed (separated) execution environment built using unikernels (a.k.a. library operating systems), including but not limited to MirageOS unikernels. Conceptually it provides a common interface between the unikernel and various host operating systems or hypervisors.</p> +<p>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.</p> +<p>Currently Solo5 is ready for use by early adopters and we plan to continue developing it further, if you are interested in supporting this development with a <a href="/Donate">donation</a> or want to hear more about the project please <a href="/Contact">get in touch with us</a>.</p> +<h4>More technical information:</h4> +<p>Solo5 features include:</p> +<ul> +<li>a sandboxed environment (CPU, memory) to execute native code in +</li> +<li>clock interfaces to access system time +</li> +<li>network interfaces to allow the unikernel to communicate with the outside world +</li> +<li>block storage interfaces to allow the unikernel to store persistent data +</li> +<li>an output-only "console" interface for logging and debugging +</li> +</ul> +<p>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.</p> +<p>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.</p> +<p>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 the developer 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.</p> +<p>The software is available <a href="https://github.com/solo5">on Github</a>.</p> +urn:uuid:a4887de7-8629-5578-836f-d31b51fe75aaProjects2022-03-01T22:03:39-00:00canopy2019-09-10T19:40:14-00:00<p>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.</p> +<p>We write all our code in a high-level memory-safe (and more secure) programming language called <a href="/Our%20Work/Technology-Employed#OCaml">OCaml</a>. In addition each piece of software leverages <a href="/Our%20Work/Technology-Employed#MirageOS">MirageOS</a> (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.</p> +<p>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.</p> +<p>Our approach means our software has a number of security and ease-of-use benefits:</p> +<ul> +<li>each application is small and fast to start +</li> +<li>our software can be run on all major hypervisors and is ready for the cloud +</li> +<li>we are able to provide rapid prototyping with a seamless path from prototype to production +</li> +<li>reduced attack vectors, for example by guarding against things like memory corruption +</li> +<li>a small code base which means a smaller attack surface, and easier review and audit +</li> +<li>the complexity is reduced ensuring ease of use and helping people to understand the technology +</li> +<li>it is possible to formally verify important parts with a proof assistant (proof writing software) +</li> +</ul> +<p>We work with <a href="/Our%20Work/Services">clients</a>, <a href="/About%20Us/Network#Collaborations">partners</a> and <a href="/About%20Us/Network#Grant-Funders">funders</a> to design and develop open-source protocols and applications within this approach.</p> +<p>If you are interested in seeing how we can assist you in improving your organization's digital infrastructure please see our <a href="/Our%20Work/Services">services offered</a>.</p> +<p>If you like our approach to open source software and want to support our work please consider a <a href="/Donate">donation</a>.</p> +<p>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 <a href="/Contact">you</a>.</p> +urn:uuid:a4887de7-8629-5578-836f-d31b51fe75aaOur Approach2019-09-10T22:16:40-00:00canopy2019-09-10T19:40:14-00:00<p>Robur is a software development cooperative specializing in robust and secure digital infrastructure written in OCaml.</p> +<h2>Current members</h2> +<h3>Hannes</h3> +<p>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.</p> +<p>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 <a href="https://github.com/rems-project/netsem">netsem</a>, an executable formal model of TCP/IP which can act as a test validator.</p> +<h3>Reynir</h3> +<p>here some text is missing</p> +<h2>Former members</h2> +<h3>Stefanie</h3> +<p>Stefanie is an infrastructure software engineer and a researcher.</p> +<p>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.</p> +<p>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.</p> +<p>Her Erdős number is 4.</p> +<h3>Martin</h3> +<p>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.</p> +<p>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.</p> +<p>Martin lives with his family in Bratislava, Slovakia and in his spare time enjoys hiking, yachting and the arts.</p> +<h4>Mindy</h4> +<p>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.</p> +<p>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!</p> +<p>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.</p> +<h3>Joe</h3> +<p>Joe is an independent IT consultant located in Copenhagen.</p> +<p>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.</p> +<p>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.</p> +<p>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).</p> +urn:uuid:a4887de7-8629-5578-836f-d31b51fe75aaTeam2021-11-16T14:55:32-00:00canopy2019-09-10T19:40:14-00:00<p>Twice a year the Robur team meet with others from the OCaml and MirageOS community at a week long hack retreat in Marrakesh, Morocco.</p> +<p>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!</p> +<p>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 <a href="http://retreat.mirage.io/">see the MirageOS site</a> for more details and sign-up method.</p> +urn:uuid:a4887de7-8629-5578-836f-d31b51fe75aaRetreats2019-09-10T21:40:09-00:00canopy2019-09-10T19:40:14-00:00<h1>Collaborations</h1> +<p><a href="https://techcultivation.org">The Center for the Cultivation of Technology</a><br /> +The Center for the Cultivation of Technology is a "back-end provider" for the open source community. They work with Robur to assist us in our financial processes and administration.</p> +<p><a href="https://leastauthority.com">Least Authority</a> +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.</p> +<p><a href="https://mirage.io">MirageOS</a><br /> +MirageOS is a library operating system that constructs unikernels for secure and high-performing applications. Most Robur projects are designed to be compatible with MirageOS, as well as native operating systems, like Linux or FreeBSD. We work closely with the MirageOS community to help develop its ecosystem and increase the availability of secure applications offered within it.</p> +<p><a href="http://ocamllabs.io">OCaml Labs</a><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.</p> +<p><a href="https://tarides.com">Tarides</a><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.</p> +<br /> +<h1>Grant Funders</h1> +<p><a href="https://nlnet.nl">NLnet Foundation</a><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.</p> +<p><a href="https://prototypefund.de/en">The Prototype Fund</a><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.</p> +urn:uuid:a4887de7-8629-5578-836f-d31b51fe75aaNetwork2020-02-18T17:34:49-00:00canopy2019-09-10T19:40:14-00:00<p>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.</p> +<p>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.</p> +<p>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:</p> +<ul> +<li>83% on salaries +</li> +<li>7% on necessary travel +</li> +<li>10% on inevitable administrative costs +</li> +</ul> +<p>If you are considering <a href="/Donate">donating</a> to us, <a href="/Our%20Work/Services">hiring</a> us, or <a href="/Contact">giving us a grant</a> 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.</p> +urn:uuid:a4887de7-8629-5578-836f-d31b51fe75aaFunding2019-10-22T17:16:46-00:00canopy \ No newline at end of file diff --git a/index.html b/index.html new file mode 100644 index 0000000..c8c783c --- /dev/null +++ b/index.html @@ -0,0 +1,4 @@ + +robur

Robur Reproducible Builds

Team

Retreats

Network

Funding

Technology Employed

Services

Publications and Talks

Projects

Our Approach

\ No newline at end of file diff --git a/static/0CBFC7AA.txt b/static/0CBFC7AA.txt new file mode 100644 index 0000000..7fb4d1c --- /dev/null +++ b/static/0CBFC7AA.txt @@ -0,0 +1,43 @@ +-----BEGIN PGP PUBLIC KEY BLOCK----- + +mQGNBFoE1TcBDACabgN7/BVKD5MQANNXFEgSmFWe4rT9ccLuVkRlaVzPDn/r9k/C +lHslpb+0/1GJwsYlYEaPiOA97KyY68cTqDmHdedC+SWJG8PuZa9tbfh5h+3VlFEy +RfA9HykAFK+ZIIE2HsCitNm3evCG0U5lzrlolKLUQGl0reUhQmwEejjrI4r2lfKU +LIechYJcsQR5obMS2wrs8RQbghsGD7OgjMPa7ZGoqtXXliHAzojh7dII+7Syq1Zd +orqbDon8N8eAypBpP0HX6LVEZ3bHJPIzz4c0/v6sGBdbUFBRq3RXVAyD2M1FyqYp +hG1G84EcaoQZJenuCA7gZNu7iaSU1zJDAthljTQ+lm8bvyXYmmeAM+26ozuIM6to +U5beWW+Ev6iAgP+DE60Azg3O4mgrnHy6vZJsDffrwUSqdfGbBVQl7wrt+wFgMhoD +5KUqdZzBrnnjNKuBwWNcosLfQrjrj6VwZDFoYVvWvpJ/ufAktao8epkulhKjH6V/ +SDECuecsqiEuImkAEQEAAbQYUm9idXIuaW8gPHRlYW1Acm9idXIuaW8+iQHUBBMB +CgA+AhsDBQsJCAcCBhUKCQgLAgQWAgMBAh4BAheAFiEEJ+uMe3vJW9ybS2PNWZJw +xwy/x6oFAloE1eUFCQWjmy4ACgkQWZJwxwy/x6rOMgv7BGJI+NbV1wLyqoOwMaRA +bGFbveoU86H0diErHyHTOtZckKevc/QixIK4aXCtZ9I3OiAf5q5Gl5WSDYJ/bKha +ZJ9iPzpHgnAdw0m9MoVdo7MZz0NGaww8RR3OnUL8ciJc3+JgjFveJzvRC9WVhtXl +j4Q1N2UrtvNcTl8dffFzwH5+fCt3gh/7eWnHaDEnmTzeR0Z9kkkRKbib06VH+nls +VnSY4v5MwJtkUG8yPXqbbnvirm1WMjwXXuFaks1dDGv6J81udfA/VP95WCTw1UEv +pBV9cQFmU2w60yR2086/6/NRHYGSGeSJsBGmfErmZzNPhqm2lcyzsM39YtRTvf1l +BN6Pstu3tnCPijuzwJRNvlQQTRGM6mA5uMJ10mmYzVY0/CCMy7zohaZMhUmBT/W7 +acas7qOrG4BS8oi6dFsvjGc7oEIRnfeh0+02mT5Kg6wje46i7KeKbvkUoqgUQGJj +N0zHpppreLs0R1FoJyAuUrG11qb2M567cN7n91iiCpUuuQINBFoE1WsBEACwmUhE +h8DibQUd8lK28YYyD3HFLmXXidr/Cw8q1Cc5w/Itm+3/WMW6//L5pSd1GugibsXW +pnypvGvcbGeV1LSaudhcwAP5CSPfRVhAQBOfCf3IwGiNU2ocI7o6r8ro0kFTfgRO +lDEmIiWGGT9QZfMkxH5bg4FUH0j4ekoDFN9k2rriW/JIBsvvvIhCEKj5IO3s10j6 +3HZBwoONEJztV84ch1h9/HMRlOiArqUzlxXF7wkuRwbKsXa4a0K0yiPj55lW/Hb1 +otAeodJGIXLJA5i3X3z3x7tEb0N9zjSmwovMQAi9WVBEQP7QIMNr3NVsSctMEhKm +dS9L2Vtv4M7gHAUFmXCILkeqHc66lHOyWgqEi2oV62KUD/juZxpTh7QIsql59Z+m +Qz0FWT/2Iven4MKjThM7XZ7DaxC0rVG5cC2Di3kVTW9ZZZQ6GxHqetP2QrB7DFYe +gM5XQxps7xDlY99YYnA4J0QmywOvZ2TZKJj5dU3cKVjXFkMwD3ZxHgug6S2Qma41 +KwuLZUw5+XOUM2WJJDcQDLnbWSirDjTQdCGOUElEqE2A89Rs9vcD1M+/YK9aRcnO +xfEu6tbRIUzOzRaA5RgVhlP0RtnRODWXrCKQ6wV9pIBZCONlru3Do5MP9HPqvdnZ +4LmngH6yDWIxMwix54nbgZSh8IGpjlxl1621YQARAQABiQG8BBgBCgAmFiEEJ+uM +e3vJW9ybS2PNWZJwxwy/x6oFAloE1WsCGwwFCQHhM4AACgkQWZJwxwy/x6rs1gv+ +IGrq+89ensYwEXHFh9kcr5Qb6PkbZcrtu0k6oZsbRg9EQEwIkc94bfjOX5eOtjSU +b8jD2fSMbTByq647L5TdX21cCh8Wnobc4kg0TJVemYnpo3R0M8SMayMY+1AQwORG +0gydCgckhDYqU+Q9f5PI0G2t5A5THRCDiAy5GYIrj63ZwtKqohTTNhMxPmYB/pzG +9aAzSMadw1DM3sc8CebEZHE+Ohp481B5fowx8aNFGHyex69UK3+Wyk1ipK20Nn+v +vfakWcMMn3oSiKZHB1v4YvIaxXnGxOBMZwFrBc+mSjGUznGgUFVZYGI2H890R6I0 +n6zASXjRohiJrFPy0/IDFEofr7j+p65sq7x+4AMyuvPcJ++mLGAyokGyukh07wF/ +2ojsq7oUYThWv/pbgslsfmxcL0HQEcMqYPgvWEeJUU/XTABu3GovfMNQ7emMFQCO +W+dx5ZYWO/QFziX8YAXTFV8wOxREPFjFTOnX7maHFH0lNWL5YM7mPvVKo3/FNM6J +=5rOl +-----END PGP PUBLIC KEY BLOCK----- diff --git a/static/css/style.css b/static/css/style.css new file mode 100644 index 0000000..81212e3 --- /dev/null +++ b/static/css/style.css @@ -0,0 +1,154 @@ +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; +}