fixing even more urls and trailing whitespaces
This commit is contained in:
Sol
parent
e8b0c31bb3
commit
3f56965e6a
5 changed files with 33 additions and 33 deletions
|
|
@ -18,7 +18,7 @@ Our approach means our software has a number of security and ease-of-use benefit
|
|||
- it is possible to formally verify important parts with a proof assistant (proof writing software)
|
||||
|
||||
|
||||
We work with [clients](/About%20Us/Funding), [partners](/About%20Us/Network#Collaborations) and [funders](/About%20Us/Network#Grant-Funders) to design and develop open-source protocols and applications within this approach.
|
||||
We work with [clients](/Our%20Work/Service), [partners](/About%20Us/Network#Collaborations) and [funders](/About%20Us/Network#Grant-Funders) to design and develop open-source protocols and applications within this approach.
|
||||
|
||||
If you are interested in seeing how we can assist you in improving your organization's digital infrastructure please see our [services offered](/Our%20Work/Services).
|
||||
|
||||
|
|
|
|||
|
|
@ -4,11 +4,11 @@ title: Projects
|
|||
|
||||
# PGP
|
||||
|
||||
OpenPGP is a much-used standard of encryption and is widely used to encrypt text, files and emails, amongst other things.
|
||||
OpenPGP is a much-used standard of encryption and is widely used to encrypt text, files and emails, amongst other things.
|
||||
|
||||
Robur is implementing OpenPGP in OCaml, for use in MirageOS and any other compaitble platform or software that is looking for PGP written in a [secure language](/Technology-Employed#Ocaml).
|
||||
Robur is implementing OpenPGP in OCaml, for use in MirageOS and any other compaitble platform or software that is looking for PGP written in a [secure language](/Our%20Work/Technology-Employed#Ocaml).
|
||||
|
||||
This work is funded through donations and is still an ongoing project, which means that it may not currently possess all the features required for various use-cases. Currently our implementation can sign, verify, compress, encrypt and decrypt.
|
||||
This work is funded through donations and is still an ongoing project, which means that it may not currently possess all the features required for various use-cases. Currently our implementation can sign, verify, compress, encrypt and decrypt.
|
||||
|
||||
You can assist us in implementing more of the OpenPGP protocol through a [donation](/Donate). If you are interested hearing more about the project, require additional features to be implemented to accommodate your project’s needs, or are able to assist with a grant please [get in touch with us](/Contact)!
|
||||
|
||||
|
|
@ -28,9 +28,9 @@ The software is available [on Github](https://github.com/cfcs/ocaml-openpgp).
|
|||
|
||||
# Solo5
|
||||
|
||||
Solo5 is a sandboxed (separated) execution environment built using unikernels (a.k.a. library operating systems), including but not limited to MirageOS unikernels. It provides the interface between software and the operating system it runs on.
|
||||
Solo5 is a sandboxed (separated) execution environment built using unikernels (a.k.a. library operating systems), including but not limited to MirageOS unikernels. It provides the interface between software and the operating system it runs on.
|
||||
|
||||
Conceptually, Solo5 provides the minimal set of "low level" building blocks and interfaces that a unikernel hosted on an operating system or hypervisor requires to be able to perform useful work.
|
||||
Conceptually, Solo5 provides the minimal set of "low level" building blocks and interfaces that a unikernel hosted on an operating system or hypervisor requires to be able to perform useful work.
|
||||
|
||||
Solo5's interfaces are designed in a way that allows us to easily port them to run on different host operating systems or hypervisors. Implementations of Solo5 run on Linux, FreeBSD, OpenBSD, the Muen Separation Kernel and the Genode Operating System Framework.
|
||||
|
||||
|
|
@ -54,7 +54,7 @@ Solo5 has been designed to isolate the unikernel as much as possible from its ho
|
|||
|
||||
Compared to existing technologies, such as traditional virtualization using KVM/QEMU, VMWare, crosvm and so on, Solo5 is several orders of magnitude smaller (around 10,000 lines of C) and is tailored to running unikernels in a legacy-free and minimalist fashion.
|
||||
|
||||
Our goal for Solo5 is to enable the use of unikernel technology to build hybrid, disaggregated systems where the designer/developer can choose which components are untrusted or security-sensitive and "split them out" from the monolithic host system. At the same time she can continue to use existing, familiar, technology as the base or "control plane" for the overall system design/deployment, or mix and match traditional applications and unikernels as appropriate.
|
||||
Our goal for Solo5 is to enable the use of unikernel technology to build hybrid, disaggregated systems where the designer/developer can choose which components are untrusted or security-sensitive and "split them out" from the monolithic host system. At the same time she can continue to use existing, familiar, technology as the base or "control plane" for the overall system design/deployment, or mix and match traditional applications and unikernels as appropriate.
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -2,24 +2,24 @@
|
|||
title: Publications and Talks
|
||||
---
|
||||
|
||||
We regularly give talks and write publications about our work, OCaml and MirageOS and other aspects of coding, security and computer science that we have expertise in. Below are some examples of these, if you are interested in having a Robur member speak at your event please [reach out](/Contact) to us.
|
||||
We regularly give talks and write publications about our work, OCaml and MirageOS and other aspects of coding, security and computer science that we have expertise in. Below are some examples of these, if you are interested in having a Robur member speak at your event please [reach out](/Contact) to us.
|
||||
|
||||
|
||||
# Hannes Mehnert
|
||||
|
||||
### Talks:
|
||||
|
||||
CERN Computing Seminar 2019 – [MirageOS: robust and secure services for the cloud](https://cds.cern.ch/record/2674523)
|
||||
Presenting MirageOS and its advantages along with explaining several applications being developed within it.
|
||||
CERN Computing Seminar 2019 – [MirageOS: robust and secure services for the cloud](https://cds.cern.ch/record/2674523)<br />
|
||||
Presenting MirageOS and its advantages along with explaining several applications being developed within it.
|
||||
|
||||
BOB 2018 - [Engineering TCP/IP with logic](https://www.youtube.com/watch?v=AYDws2Nqcgs)
|
||||
Presents a formal model of TCP/IP (developed 2000-2009 and refurbished since 2016), how it can be used to validate the FreeBSD TCP/IP stack, and what was learned while writing it. It is modeled as a label transition system, including timers, retransmission, etc.
|
||||
BOB 2018 - [Engineering TCP/IP with logic](https://www.youtube.com/watch?v=AYDws2Nqcgs)<br />
|
||||
Presents a formal model of TCP/IP (developed 2000-2009 and refurbished since 2016), how it can be used to validate the FreeBSD TCP/IP stack, and what was learned while writing it. It is modeled as a label transition system, including timers, retransmission, etc.
|
||||
|
||||
BornHack 2018 - [MirageOS: what did we achieve in the last year?](https://www.youtube.com/watch?v=QtPUCC6KaWo)
|
||||
BornHack 2018 - [MirageOS: what did we achieve in the last year?](https://www.youtube.com/watch?v=QtPUCC6KaWo)<br />
|
||||
This is a continuation of earlier talks at Bornhack (2016, 2017), and goes into detail of some active projects, such as: community repository signing (for secure updates), DNS infrastructure, our Prototype Fund sponsored CalDAV-server.
|
||||
|
||||
Chaos Computer Club Congress 2018 - [Domain Name System](https://www.youtube.com/watch?v=I7060fqa-B8)
|
||||
Discusses the basic usage of DNS, including stub and recursive resolver, server; various protocol extensions including zone transfer, dynamic updates, authentication, notifications; privacy extensions (query path minimisation, DNS-over-TLS); provisioning let's encrypt certificates; and attachs (poisoning, amplification). Explains the Robur implementation of DNS with above mentioned extensions as minimized MirageOS unikernels.
|
||||
Chaos Computer Club Congress 2018 - [Domain Name System](https://www.youtube.com/watch?v=I7060fqa-B8)<br />
|
||||
Discusses the basic usage of DNS, including stub and recursive resolver, server; various protocol extensions including zone transfer, dynamic updates, authentication, notifications; privacy extensions (query path minimisation, DNS-over-TLS); provisioning let's encrypt certificates; and attachs (poisoning, amplification). Explains the Robur implementation of DNS with above mentioned extensions as minimized MirageOS unikernels.
|
||||
|
||||
### Publications:
|
||||
|
||||
|
|
@ -27,7 +27,7 @@ Discusses the basic usage of DNS, including stub and recursive resolver, server;
|
|||
|
||||
[Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation (Usenix security 2015)](https://usenix15.nqsb.io), [video presentation](https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/kaloper-mersinjak) (David Kaloper-Meršinjak, Hannes Mehnert, Anil Madhavapeddy, Peter Sewell)
|
||||
|
||||
[Not-quite-so-broken TLS 1.3 Mechanised Conformance Checking - TLS 1.3 Ready or Not (TRON)](https://tron.nqsb.io), [workshop website](https://www.ndss-symposium.org/ndss2016/tron-workshop-programme/) (David Kaloper-Meršinjak and Hannes Mehnert)
|
||||
[Not-quite-so-broken TLS 1.3 Mechanised Conformance Checking - TLS 1.3 Ready or Not (TRON)](https://tron.nqsb.io), [workshop website](https://www.ndss-symposium.org/ndss2016/tron-workshop-programme/) (David Kaloper-Meršinjak and Hannes Mehnert)
|
||||
|
||||
|
||||
[Unikernels as Processes - ACM Symposium on Cloud Computing 2018](https://dl.acm.org/citation.cfm?id=3267845) (Dan Williams, Ricardo Koller, Martin Lucina, Nikhil Prakash)
|
||||
|
|
@ -37,8 +37,8 @@ Discusses the basic usage of DNS, including stub and recursive resolver, server;
|
|||
|
||||
### Talks:
|
||||
|
||||
FOSDEM 2019 - [Solo5: A sandboxed, re-targetable execution environment for unikernels](https://www.youtube.com/watch?v=VO6f7uSs3-I)
|
||||
Explains Solo5 which is a microkernel-friendly, sandboxed, re-targetable execution environment for unikernels, with a taste for minimalism. Presents the interfaces it offers to the unikernel/library operating system/application developer. Using existing library operating systems, such as MirageOS, demonstrates the developer experience for various Solo5 targets, going on to show how rigorously applying minimalist principles to interface design is used to our advantage, blurring traditional lines between unikernels, processes, kernels and hypervisors.
|
||||
FOSDEM 2019 - [Solo5: A sandboxed, re-targetable execution environment for unikernels](https://www.youtube.com/watch?v=VO6f7uSs3-I)<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.
|
||||
|
||||
### Publications:
|
||||
|
||||
|
|
@ -49,13 +49,13 @@ Explains Solo5 which is a microkernel-friendly, sandboxed, re-targetable executi
|
|||
|
||||
### Talks:
|
||||
|
||||
DevOpsDays MSN 2018 - [FuzzOps](https://www.youtube.com/watch?v=BtJsakoXxdY)
|
||||
Discusses testing software to find bugs before deploying software, including continuous integration solutions and property-based testing. Looks at issues of testing frameworks, including common human errors. Explains fuzzers - a solution to this important problem in which computers generate inputs and find counter examples to enable more complete code testing and bug finding.
|
||||
DevOpsDays MSN 2018 - [FuzzOps](https://www.youtube.com/watch?v=BtJsakoXxdY)<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.
|
||||
|
||||
Confreaks 2017 - [DHCP: IT’S MOSTLY YELLING!!](https://www.youtube.com/watch?v=enRY9jd0IJw)
|
||||
Discusses how the Dynamic Host Configuration Protocol (DHCP) is structured and how it is used in a network. Explains how addressing and packet structure (or yelling) in DHCP works to establish a connection, and what can go wrong. Looks at tcpdump as a way to examine this yelling along with DHCP options to help establish a quieter and more secure connection.
|
||||
Discusses how the Dynamic Host Configuration Protocol (DHCP) is structured and how it is used in a network. Explains how addressing and packet structure (or yelling) in DHCP works to establish a connection, and what can go wrong. Looks at tcpdump as a way to examine this yelling along with DHCP options to help establish a quieter and more secure connection.
|
||||
|
||||
Strange Loop 2015 - [Non-Imperative Network Programming](https://www.youtube.com/watch?v=GNc1t6Q5Dls)
|
||||
Strange Loop 2015 - [Non-Imperative Network Programming](https://www.youtube.com/watch?v=GNc1t6Q5Dls)<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.
|
||||
|
||||
|
||||
|
|
@ -63,8 +63,8 @@ Discusses how network programming is often taught and practiced in C, but it doe
|
|||
|
||||
### Talks:
|
||||
|
||||
Berlin Buzzwords 2018 - [Your Search Service as a Composable Function](https://www.youtube.com/watch?v=4Yag3SrAMnI)
|
||||
Berlin Buzzwords 2018 - [Your Search Service as a Composable Function](https://www.youtube.com/watch?v=4Yag3SrAMnI)<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.
|
||||
|
||||
JSConf EU 2015 - [Functional programming and curry cooking in JS](https://www.youtube.com/watch?v=6Qx5ZAbfqjo)
|
||||
This talk explores functional programming concepts, which help us create powerful abstractions to master complex problems and create more simple and elegant programs. JavaScript allows us to ease into the functional programming style, letting us focus just on the concepts, without the distraction of learning a specific functional programming language. To make the dry functional programming concepts more digestible, we use cooking as an analogy. And since the logician Haskell Curry invented functional programming, we combine our journey in JavaScript with examples and recipes for tasty curry dishes.
|
||||
JSConf EU 2015 - [Functional programming and curry cooking in JS](https://www.youtube.com/watch?v=6Qx5ZAbfqjo)<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.
|
||||
|
|
|
|||
|
|
@ -2,31 +2,31 @@
|
|||
title: Services
|
||||
---
|
||||
|
||||
We can work with you to design, develop and audit software and infrastructure to assist you in enhancing your technical security and reliability. Whilst we are not a service provider, and so can not offer to host applications, we can assist you in deploying MirageOS and OCaml services.
|
||||
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.
|
||||
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 can consult on design for specific products to ensure you plan the best solution for a single application, or take a more holistic view of your infrastructure and protocols to improve speed, security and ease of use.
|
||||
|
||||
We’re experienced in designing and reviewing serialization frameworks, network protocols, cryptographic protocols, and system architectures, and with solutions built on the FreeBSD and Linux operating systems, including sandboxing, hardening and exploit mitigations.
|
||||
|
||||
|
||||
### Develop
|
||||
Working with [Ocaml](/Technology-Employed#OCaml) and [MirageOS](/Technology-Employed#MirageOS) we can develop specific applications that give you high assurance of their security and functionality, which seamlessly integrate in your existing infrastructure.
|
||||
Working with [Ocaml](/Our%20Work/Technology-Employed#Ocaml) and [MirageOS](/Our%20Work/Technology-Employed#MirageOS) we can develop specific applications that give you high assurance of their security and functionality, which seamlessly integrate in your existing infrastructure.
|
||||
|
||||
We can also work on a full stack approach to meet your needs and help a smooth migration plan for your organization.
|
||||
|
||||
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.
|
||||
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.
|
||||
We can provide code auditing services, particularly focusing on security and reducing code base. We have team members who have thorough experience working with OCaml, C (embedded, kernel and userspace), x86 assembly, Scala, Java, Android, Haskell, PHP and Python.
|
||||
|
||||
Our audits can help ensure your environment is secure whilst also working with you to reduce attack service and increase speed. While we generally prefer “white-box” audits because we believe they yield the best results for the time invested, we also have experience with “black-box” penetration testing.
|
||||
|
||||
|
||||
Please [contact us](/Contact) if you are interested in any of the above and we can discuss how we can assist you in developing a more secure architecture and for your organization.
|
||||
Please [contact us](/Contact) if you are interested in any of the above and we can discuss how we can assist you in developing a more secure architecture and for your organization.
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@ title: Technology Employed
|
|||
|
||||
# MirageOS
|
||||
|
||||
MirageOS is a software suite to build custom-tailored operating systems from (mostly open source) small individual libraries. It has been developed since 2009 at the University of Cambridge, UK and is written in the programming language [OCaml](/Our%20Work/Technology-Employed#Ocaml).
|
||||
MirageOS is a software suite to build custom-tailored operating systems from (mostly open source) small individual libraries. It has been developed since 2009 at the University of Cambridge, UK and is written in the programming language [OCaml](/Our%20Work/Technology-Employed#OCaml).
|
||||
|
||||
It compiles the necessary OCaml libraries into a unikernel - a small operating system, each built for a certain purpose. For each unikernel we can pick from hundreds of permissively licensed open source libraries which implement network protocols, storage on block devices, or interfaces to network devices via the hypervisor or host operating system. As we only put into each one exactly what is needed, each unikernel is fast; instantly booting and, as there is less code base, it is easier to maintain and keep secure.
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue