Introduction

MirageOS development focus has been a lot on tooling and the developer experience, but to accomplish our goal to "get MirageOS into production", we need to lower the barrier. This means for us to release binary unikernels. As described earlier, we received a grant for "Deploying MirageOS" from NGI Pointer to work on the required infrastructure. This is joint work with Reynir.

We provide at builds.robur.coop binary unikernel images (and supplementary software). Do…

Introduction

MirageOS development focus has been a lot on tooling and the developer experience, but to accomplish our goal to "get MirageOS into production", we need to lower the barrier. This means for us to release binary unikernels. As described earlier, we received a grant for "Deploying MirageOS" from NGI Pointer to work on the required infrastructure. This is joint work with Reynir.

We provide at builds.robur.coop binary unikernel images (and supplementary software). Doing binary releases of MirageOS unikernels is challenging in two aspects: firstly to be useful for everyone, a binary unikernel should not contain any configuration (such as private keys, certificates, etc.). Secondly, the binaries should be reproducible. This is crucial for security; everyone can reproduce the exact same binary and verify that our build service did only use the sources. No malware or backdoors included.

This post describes how you can deploy MirageOS unikernels without compiling it from source, then dives into the two issues outlined above - configuration and reproducibility - and finally describes how to setup your own reproducible build infrastructure for MirageOS, and how to bootstrap it.

Deploying MirageOS unikernels from binary

To execute a MirageOS unikernel, apart from a hypervisor (Xen/KVM/Muen), a tender (responsible for allocating host system resources and passing these to the unikernel) is needed. Using virtio, this is conventionally done with qemu on Linux, but its code size (and attack surface) is huge. For MirageOS, we develop Solo5, a minimal tender. It supports hvt - hardware virtualization (Linux KVM, FreeBSD BHyve, OpenBSD VMM), spt - sandboxed process (a tight seccomp ruleset (only a handful of system calls allowed, no hardware virtualization needed), Linux only). Apart from that, muen (a hypervisor developed in Ada), virtio (for some cloud deployments), and xen (PVHv2 or Qubes 4.0) - read more. We deploy our unikernels as hvt with FreeBSD BHyve as hypervisor.

On builds.robur.coop, next to the unikernel images, solo5-hvt packages (FreeBSD 12.2, Ubuntu 20.04) are provided - download the binary and install it. A NixOS package is already available - please note that soon packaging will be much easier (and we will work on packages merged into distributions).

When the tender is installed, download a unikernel image (e.g. the traceroute described in an earlier post), and execute it:

$ solo5-hvt --net:service=tap0 -- traceroute.hvt --ipv4=10.0.42.2/24 --ipv4-gateway=10.0.42.1

If you plan to orchestrate MirageOS unikernels, you may be interested in albatross - we provide binary packages as well for this (albatross FreeBSD and albatross Ubuntu 20.04). An upcoming post will go into further details of how to setup albatross.

MirageOS configuration

A MirageOS unikernel has a specific purpose - composed of OCaml libraries - selected at compile time, which allows to only embed the required pieces. This reduces the attack surface drastically. At the same time, to be widely useful to multiple organisations, no configuration data must be embedded into the unikernel.

Early MirageOS unikernels such as mirage-www embed content (blog posts, ..) and TLS certificates and private keys in the binary (using crunch). The Qubes firewall (read the blog post by Thomas for more information) used to include the firewall rules until v0.6 in the binary, since v0.7 the rules are read dynamically from QubesDB. This is big usability improvement.

We have several possibilities to provide configuration information in MirageOS, on the one hand via boot parameters (can be pre-filled at development time, and further refined at configuration time, but those passed at boot time take precedence). Boot parameters have a length limitation.

Another option is to use a block device - where the TLS reverse proxy stores the configuration, modifiable via a TCP control socket (authentication using a shared hmac secret).

Several other unikernels, such as this website and our CalDAV server, store the content in a remote git repository. The git URI and credentials (private key seed, host key fingerprint) are passed via boot parameter.

Finally, another option that we take advantage of is to introduce a post-link step that rewrites the binary to embed configuration. The tool caravan developed by Romain that does this rewrite is used by our openvpn router (binary).

In the future, some configuration information - such as monitoring system, syslog sink, IP addresses - may be done via DHCP on one of the private network interfaces - this would mean that the DHCP server has some global configuration option, and the unikernels no longer require that many boot parameters. Another option we want to investigate is where the tender shares a file as read-only memory-mapped region from the host system to the guest system - but this is tricky considering all targets above (especially virtio and muen).

Behind the scenes: reproducible builds

To provide a high level of assurance and trust, if you distribute binaries in 2021, you should have a recipe how they can be reproduced in a bit-by-bit identical way. This way, different organisations can run builders and rebuilders, and a user can decide to only use a binary if it has been reproduced by multiple organisations in different jurisdictions using different physical machines - to avoid malware being embedded in the binary.

For a reproduction to be successful, you need to collect the checksums of all sources that contributed to the built, together with other things (host system packages, environment variables, etc.). Of course, you can record the entire OS and sources as a tarball (or file system snapshot) and distribute that - but this may be suboptimal in terms of bandwidth requirements.

With opam, we already have precise tracking which opam packages are used, and since opam 2.1 the opam switch export includes extra-files (patches) and records the VCS version. Based on this functionality, orb, an alternative command line application using the opam-client library, can be used to collect (a) the switch export, (b) host system packages, and (c) the environment variables. Only required environment variables are kept, all others are unset while conducting a build. The only required environment variables are PATH (sanitized with an allow list, /bin, /sbin, with /usr, /usr/local, and /opt prefixes), and HOME. To enable Debian's apt to install packages, DEBIAN_FRONTEND is set to noninteractive. The SWITCH_PATH is recorded to allow orb to use the same path during a rebuild. The SOURCE_DATE_EPOCH is set to enable tools that record a timestamp to use a static one. The OS* variables are only used for recording the host OS and version.

The goal of reproducible builds can certainly be achieved in several ways, including to store all sources and used executables in a huge tarball (or docker container), which is preserved for rebuilders. The question of minimal trusted computing base and how such a container could be rebuild from sources in reproducible way are open.

The opam-repository is a community repository, where packages are released to on a daily basis by a lot of OCaml developers. Package dependencies usually only use lower bounds of other packages, and the continuous integration system of the opam repository takes care that upon API changes all reverse dependencies include the right upper bounds. Using the head commit of opam-repository usually leads to a working package universe.

For our MirageOS unikernels, we don't want to stay behind with ancient versions of libraries. That's why our automated building is done on a daily basis with the head commit of opam-repository. Since our unikernels are not part of the main opam repository (they include the configuration information which target to use, e.g. hvt), and we occasionally development versions of opam packages, we use the unikernel-repo as overlay.

If no dependent package got a new release, the resulting binary has the same checksum. If any dependency was released with a newer release, this is picked up, and eventually the checksum changes.

Each unikernel (and non-unikernel) job (e.g. dns-primary outputs some artifacts:

• the binary image (in bin/, unikernel image, OS package)
• the build-environment containing the environment variables used for this build
• the system-packages containing all packages installed on the host system
• the opam-switch that contains all opam packages, including git commit or tarball with checksum, and potentially extra patches, used for this build
• a job script and console output

To reproduce such a built, you need to get the same operating system (OS, OS_FAMILY, OS_DISTRIBUTION, OS_VERSION in build-environment), the same set of system packages, and then you can orb rebuild which sets the environment variables and installs the opam packages from the opam-switch.

You can browse the different builds, and if there are checksum changes, you can browse to a diff between the opam switches to reason whether the checksum change was intentional (e.g. here the checksum of the unikernel changed when the x509 library was updated).

The opam reproducible build infrastructure is driven by:

• orb conducting reproducible builds (packages FreeBSD, Ubuntu 20.04)
• builder scheduling builds in contained environments (packages FreeBSD, Ubuntu 20.04)
• builder-web storing builds in a database and providing a HTTP interface (packages FreeBSD)

These tools are themselves reproducible, and built on a daily basis. The infrastructure executing the build jobs installs the most recent packages of orb and builder before conducting a build. This means that our build infrastructure is reproducible as well, and uses the latest code when it is released.

Conclusion

Thanks to NGI funding we now have reproducible MirageOS binary builds available at builds.robur.coop. The underlying infrastructure is reproducible, available for multiple platforms (Ubuntu using docker, FreeBSD using jails), and can be easily bootstrapped from source (once you have OCaml and opam working, getting builder and orb should be easy). All components are open source software, mostly with permissive licenses.

We also have an index over sha-256 checksum of binaries - in the case you find a running unikernel image where you forgot which exact packages were used, you can do a reverse lookup.

We are aware that the web interface can be improved (PRs welcome). We will also work on the rebuilder setup and run some rebuilds.

Please reach out to us (at team AT robur DOT coop) if you have feedback and suggestions.

Tarides is excited to announce that our CEO, Dr. Thomas Gazagnaire, and Prof. Anil Madhavapeddy, from the University of Cambridge, will present their innovative platform OSMOSE at the Open Source Innovation Sprint (OSIS) conference on 1 July 2021. This event is organized by Systematic.

OSMOSE is a software platform made to manage digital infrastructure at scale, securely and efficiently. It uses the groundbreaking creation of unikernels to radically simplify the way applications are built and de…

Tarides is excited to announce that our CEO, Dr. Thomas Gazagnaire, and Prof. Anil Madhavapeddy, from the University of Cambridge, will present their innovative platform OSMOSE at the Open Source Innovation Sprint (OSIS) conference on 1 July 2021. This event is organized by Systematic.

OSMOSE is a software platform made to manage digital infrastructure at scale, securely and efficiently. It uses the groundbreaking creation of unikernels to radically simplify the way applications are built and deployed for the cloud.

Since digital transformation has become more and more dependent on cloud computing, it has increasing problems with high response latency, security risks, and resource inefficiencies—all which make these services ultimately unreliable. The demand for interconnected devices is ever increasing, but the security of these devices remain unchecked, making them susceptible to security vulnerabilities. This leaves consumers and businesses open to exploitation, as demonstrated in reports of tech devices violating users’ privacy, like sending audio recordings without their knowledge or consent.

Tarides addresses these issues with OSMOSE, a platform which combines hardware and software elements to invert the current cloud-centric model. OSMOSE securely connects with physical spaces to provide extremely low latency and high-bandwidth, local-area computation capabilities, which can turn a fleet of IoT devices into a local data-centre.

This innovative platform enables computer resources to be tracked efficiently and temporarily rented to users. This turns any IoT deployment into a local, private cloud, allowing a better utilization of local resources and improved security.

Major components of OSMOSE already have commercial applications. It’s been used to make existing cloud deployments more secure and efficient by companies such as Amazon, Citrix, and Docker.

Tarides applies a high-touch, mixed business strategy—using consultancy services to field test open source components under development. Tarides applies their research to real-world systems to build unikernels, a secure-by-design and resource-efficient application specialised to their run-time environments. If interested in using OSMOSE as a solution for your business, please reach out to Tarides for more information.

Register for OSIS to attend the OSMOSE presentation on 1 July 2021.

Feedback on this post is welcomed on Discuss!

The opam team has great pleasure in announcing opam 2.1.0~rc2!

The focus since beta4 has been preparing for a world with more than one released version of opam (i.e. 2.0.x and 2.1.x). The release candidate extends CLI versioning further and, under the hood, includes a big change to the opam root format which allows new versions of opam to indicate that the root may still be read by older versions of the opam libraries. A plugin compiled against the…

Feedback on this post is welcomed on Discuss!

The opam team has great pleasure in announcing opam 2.1.0~rc2!

The focus since beta4 has been preparing for a world with more than one released version of opam (i.e. 2.0.x and 2.1.x). The release candidate extends CLI versioning further and, under the hood, includes a big change to the opam root format which allows new versions of opam to indicate that the root may still be read by older versions of the opam libraries. A plugin compiled against the 2.0.9 opam libraries will therefore be able to read information about an opam 2.1 root (plugins and tools compiled against 2.0.8 are unable to load opam 2.1.0 roots).

Please do take this release candidate for a spin! It is available in the Docker images at ocaml/opam on Docker Hub as the opam-2.1 command (or you can sudo ln -f /usr/bin/opam-2.1 /usr/bin/opam in your Dockerfile to switch to it permanently). The release candidate can also be tested via our installation script (see the wiki for more information).

Thank you to anyone who noticed the unannounced first release candidate and tried it out. Between tagging and what would have been announcing it, we discovered an issue with upgrading local switches from earlier alpha/beta releases, and so fixed that for this second release candidate.

Assuming no showstoppers, we plan to release opam 2.1.0 next week. The improvements made in 2.1.0 will allow for a much faster release cycle, and we look forward to posting about the 2.2.0 plans soon!

Try it!

In case you plan a possible rollback, you may want to first backup your ~/.opam directory.

The upgrade instructions are unchanged:

1. Either from binaries: run

   sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --dev

   or download manually from the Github "Releases" page to your PATH.

2. Or from source, manually: see the instructions in the README.

You should then run:

opam init --reinit -ni

We hope there won't be any, but please report any issues to the bug-tracker. Thanks for trying it out, and hoping you enjoy!

At Ahrefs, we have been using BuckleScript and ReasonML in production for more than two years. We already have a codebase of tens of thousands of lines of code, with several web applications that are data intensive and communicate with backend services written in OCaml, using tools like atd.

Given our investment in these technologies, we have been following closely the recent changes in ReScript, with its rebrand and renaming, and the split with the ReasonML proje…

At Ahrefs, we have been using BuckleScript and ReasonML in production for more than two years. We already have a codebase of tens of thousands of lines of code, with several web applications that are data intensive and communicate with backend services written in OCaml, using tools like atd.

Given our investment in these technologies, we have been following closely the recent changes in ReScript, with its rebrand and renaming, and the split with the ReasonML project, explained in the project blog post.

ReScript: becoming its own language

We are excited about the way ReScript is unifying the experience and making it easier for developers who are getting started to find documentation in a single place, as well as continuing its strong focus on performance and readable JavaScript output.

On the other hand, we are trying to figure out the implications of this change in the mid- and long-term, especially regarding the integration with the OCaml ecosystem. And more importantly, what this evolution will mean for production users like us who rely on this integration.

ReScript integration with OCaml has historically been seamless, as BuckleScript started originally as a new backend for the OCaml compiler. However, in recent months, there have been several hints that ReScript wants to evolve towards becoming its own language:

• It has now its own parser, incompatible with OCaml native applications
• Official repository guidelines for technical writing mentions explicitly that no reference to OCaml should appear in docs
• Upgrades to the latest version of OCaml compiler, which used to be part of the roadmap, have been deprioritized recently.

So, even if officially ReScript has not announced that they will break backwards compatibility with OCaml, just the fact that it is sticking with an old version of the OCaml compiler poses some challenges for us in terms of tooling. The uncertainty about the future and the pace of changes add some risk to the high-level goals we have for our teams and codebase: we would like to share more code between frontend and backend, not less.

Melange: a fork of ReScript, focused on OCaml compatibility

When António Monteiro announced Melange, a fork of ReScript but with a strong focus on keeping compatibility with OCaml, we decided to try it out and see how it could work for us.

Ultimately, the experiment was successful. We managed to build all our frontend applications with Melange, while keeping the existing bundling setup, which currently uses Webpack.

Throughout this process, we had to modify some parts of the code. We will now go through the most relevant parts of the process:

• Upgrade to OCaml 4.12: the most relevant part was the deprecation of Pervasives module to use Stdlib.
• Use ppxlib in our ppxs: we had to upgrade the two ppxs that we use in the frontend codebase to the latest compiler version, bs-emotion-ppx and an in-house ppx for internationalization.
• Configure esy: we were already using esy to bring the editor tooling into scope of the developer environment, so we just had to make sure melange would also be included in the json configuration.
• Upgrade to Reason 3.7.0: a quite simple change too, as the whole process is automated by using refmt. As a side note, we ran into a small bug with some type annotations, that we were able to work around.
• “Lift” dune workspace to the root of our monorepo: this is probably the most intrusive change. Because we have shared code between backend and frontend, and Dune needs to have access to all sources under its workspace, we had to “lift” the Dune workspace from the backend directory to the root of monorepo.

The good

This experiment allowed us to experience what a project like Melange could offer for our use case. Here are some of the things we might be able to leverage in a codebase built with Melange:

• Recent version of the OCaml compiler: at some point, we could pin compiler version between backend and frontend teams, making upgrades more straightforward as they would happen atomically.
• Shared editor tooling: the official OCaml vscode extension works great with Melange, as well as any other OCaml editor integration. Having backend and frontend teams use similar editor setup removes a lot of maintenance work for us.
• Consuming ppxs from source: Melange allows to consume ppxs from source, which also removes issues with pre-compiled ppxs (like this issue with the recent M1 Macs).
• Melange allows to run all ppxs from a single executable file, which has some nice performance benefits.
• Use Dune for atd files generators: ReScript “generators” are unfortunately not documented anymore, but we use them extensively for atd file generation. Being able to share Dune rules in backend and frontend would make our build setup easier.
• Access to OCaml documentation tooling: Melange allows to leverage existing tooling for generating documentation, like odoc.
• Async syntax: the latest Reason version supports “let op” syntax, which is handy for client-side code.

The bad

While there are many things that are exciting about Melange, there are some other parts that can be improved.

• Build performance: We already knew that performance would be far worse than ReScript, as Melange uses Dune in a way that it was not designed for. In our tests, builds with Melange are roughly 1 order of magnitude slower than ReScript ones.
• First-class Dune support: if there was a deeper integration between Dune and Melange, we could explore features like shared libraries or shared rules between backend and frontend. As of today, Dune has no knowledge about Melange environment, so it can perform basic rules execution, but there is no access to high level stanzas like library in Melange.
• Two-headed goal: finally, we see a more strategic risk in Melange proposition. Right now it has two goals: keep compatibility with both ReScript and OCaml. But we don’t know how long these goals will be feasible. If at some point ReScript decides to move away from the OCaml compiler fully, then Melange users would not be able to consume any updates to the ReScript ecosystem anymore.

Alright, but are you migrating to Melange or ReScript?

With all the information available, the answer is: we don’t know yet. 😄 We want to keep exploring all the available options and have as much information as possible before committing further. So for now, we are upgrading the codebase to recent versions of ReScript, but we are holding up on features that only work one way. For example, we have not migrated our codebase to the ReScript syntax yet, as there is no way to translate back to Reason syntax.

In the meantime, we will keep exploring how far the limitations of Melange can be mitigated. To be continued! 🚀

Thanks to Igor and Feihong for reviewing and improving earlier versions of this post.

Building Ahrefs codebase with Melange was originally published in ahrefs on Medium, where people are continuing the conversation by highlighting and responding to this story.

A while ago, my former student Chuangjie Xu and I computed an integer using a sheaf topos. For that purpose,

1. we developed our mathematics constructively,
2. we formalized our mathematics in Martin-Löf type theory, in Agda notation,
3. we pressed a button, and
4. after a few seconds we saw the integer we expected in front of us.

Well, it was a few seconds for the computer in steps (3)-(4), but three years for us in steps (1)-(2).

Why formalize?

Most people formalize mathematics (in Automa…

A while ago, my former student Chuangjie Xu and I computed an integer using a sheaf topos. For that purpose,

1. we developed our mathematics constructively,
2. we formalized our mathematics in Martin-Löf type theory, in Agda notation,
3. we pressed a button, and
4. after a few seconds we saw the integer we expected in front of us.

Well, it was a few seconds for the computer in steps (3)-(4), but three years for us in steps (1)-(2).

Why formalize?

Most people formalize mathematics (in Automath, NuPrl, Coq, Agda, Lean, ...) to get confidence in the correctness of mathematics - or so they claim. The reality is that formalizing mathematics is intellectually fun.

Entertaining considerations aside, my initial motivation for computer formalization, about 10 years ago, was to write algorithms derived from work on game theory with Paulo Oliva. In particular, this had applications to proof theory, such as getting programs from classical proofs. Our first version of a (manually) extracted program from a classical proof was written in Haskell, in a train journey coming back from a visit to our collaborators Monika Seisenberger and Ulrich Berger in Swansea. The train journey was long enough for us to be able to complete the program. But when we ran it, it didn't work. I had been learning Agda for about one year by then, and I told Paulo that it would be easier to write the mathematics in Agda, and hence be sure it will work before we ran it, than to debug the Haskell program. And that was the case.

Before then I was the kind of person who dismissed formalization, and would say so to people who did formalization (it is probably too late to apologize now). I trusted my own mathematics, and if I wanted to derive programs from my mathematical work, I would just write them manually. Since then, my attitude has changed considerably.

I now use Agda as a "blackboard" to develop my work. For example, the following were conceived and developed directly in Agda before they were written in mathematical vernacular: Injective types in univalent mathematics, Compact, totally separated and well-ordered types in univalent mathematics, The Cantor-Schröder-Bernstein Theorem for ∞-groupoids, The Burali-Forti argument in HoTT/UF and Continuity of Gödel's system T functionals via effectful forcing.

Other people will have different reasons to formalize. For example, wouldn't it be wonderful if the whole undergraduate mathematical curriculum were formalized? Wouldn't it be wonderful to archive all mathematical knowledge not just as text but in a more structured way, so that it can be used by both people and computers? Wouldn't it be wonderful if when we submit a paper, the referee didn't need to check correctness, but only novelty, significance and so on? Did you ever woke up in the middle of the night after you submitted a paper, with doubts about the crucial lemma? Or worse, after it was published?

But for the purposes of this post, I will concentrate on only one aspect of formalization: a formalized piece of constructive mathematics is automatically a computer program that you can run in practice.

Constructive mathematics

Constructive mathematics begins by removing the principle of excluded middle, and therefore the axiom of choice, because choice implies excluded middle. But why would anybody do such an outrageous thing?

I particularly like the analogy with Euclidean geometry. If we remove the parallel postulate, we get absolute geometry, also known as neutral geometry. If after we remove the parallel postulate, we add a suitable axiom, we get hyperbolic geometry, but if we instead add a different suitable axiom we get elliptic geometry. Every theorem of neutral geometry is a theorem of these three geometries, and more geometries. So a neutral proof is more general.

When I say that I am interested in constructive mathematics, most of the time I mean that I am interested in neutral mathematics, so that we simply remove excluded middle and choice, and we don't add anything to replace them. So my constructive definitions and theorems are also definitions and theorems of classical mathematics.

Occasionally, I flirt with axioms that contradict the principle of excluded middle, such as Brouwerian intuitionistic axioms that imply that "all functions $(\mathbb{N} \to 2) → \mathbb{N}$ are uniformly continuous", when we equip the set $2$ with the discrete topology and $\mathbb{N} \to 2$ with the product topology, so that we get the Cantor space. The contradiction with classical logic, of course, is that using excluded middle we can define non-continuous functions by cases. Brouwerian intuitionistic mathematics is analogous to hyperbolic or elliptic geometry in this respect. The "constructive" mathematics I am talking about in this post is like neutral geometry, and I would rather call it "neutral mathematics", but then nobody would know what I am talking about. That's not to say that the majority of mathematicians will know what I am talking about if I just say "constructive mathematics".

But it is not (only) the generality of neutral mathematics that I find attractive. Somehow magically, constructions and proofs that don't use excluded middle or choice are automatically programs. The only way to define non-computable things is to use excluded middle or choice. There is no other way. At least not in the underlying type theories of proof assistants such as NuPrl, Coq, Agda and Lean. We don't need to consider Turing machines to establish computability. What is a computable sheaf, anyway? I don't want to pause to consider this question in order to use a sheaf topos to compute a number. We only need to consider sheaves in the usual mathematical sense.

Sometimes people ask me whether I believe in the principle of excluded middle. That would be like asking me whether I believe in the parallel postulate. It is clearly true in Euclidean geometry, clearly false in elliptic and in hyperbolic geometries, and deliberately undecided in neutral geometry. Not only that, in the same way as the parallel postulate defines Euclidean geometry, the principle of excluded middle and the axiom of choice define classical mathematics.

The undecidedness of excluded middle in my neutral mathematics allows me to prove, for example, "if excluded middle holds, then the Cantor-Schröder-Bernstein Theorem for ∞-groupoids holds". If excluded middle were false, I would be proving a counter-factual - I would be proving that an implication is true simply because its premise is false. But this is not what I am doing. What I am really proving is that the CSB theorem holds for the objects of boolean ∞-toposes. And why did I use excluded middle? Because somebody else showed that there is no other way. But also sometimes I use excluded middle or choice when I don't know whether there is another way (in fact, I believe that more than half of my publications use classical logic).

So, am I a constructivist? There is only one mathematics, of which classical and constructive mathematics are particular branches. I enjoy exploring the whole landscape. I am particularly fond of constructive mathematics, and I wouldn't practice it, however useful it may be for applications, if I didn't enjoy it. But this is probably my bad taste.

Toposes as provinces of the mathematical world

Toposes are generalized (sober) spaces. But also toposes can be considered as provinces of the mathematical world.

Hyland's effective topos is a province where "everything is computable". This is an elementary topos, which is not a Grothendieck topos, built from classical ingredients: we use excluded middle and choice, with Turing machines to talk about computability. But, as it turns out, although everybody agrees which functions $\mathbb{N} \to \mathbb{N}$ are computable and which ones aren't, there is disagreement among classical mathematicians working on computability theory about what counts as "computable" for more general mathematical objects, such as functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$. No problem. Just consider other provinces, called realizability toposes, which include the effective topos as an example.

Johnstone's topological topos is a topos of spaces. It fully embeds a large category of topological spaces, where the objects outside the image of the embedding can be considered as generalized spaces (which include the Kuratowski limit spaces and more). In this province of the mathematical world, "all functions are continuous".

There are also provinces where there are infinitesimals and "all functions are smooth".

A more boring, but important, province, is the topos of classical sets. This is where classical mathematics takes place.

These provinces of mathematics have an internal language. We use a certain subobject classifier to collect the things that count as truth values in the province, and we devise a kind of type theory whose types are interpreted as objects and whose mathematical statements are interpreted as truth values in the province. Then a mathematical statement in this type theory is true in some toposes, false in other toposes, and undecided in yet other toposes. This internal language, or type theory, is very rich. Starting from natural numbers we can construct the integers, the rationals, the real numbers, free groups etc., and then do e.g. analysis and group theory and so on. The internal language of the free topos can be considered as a type theory for neutral mathematics: whatever we prove in the free type theory is true in all mathematical provinces, including classical set theory.

In the above first three provinces, the principle of excluded middle fails, but for different reasons, with respectively computability, continuity and infinitesimals to blame.

Our topos

Now our plot has a twist: we work within neutral mathematics to build a province of "biased" constructive mathematics where Brouwerian principles hold, such as "all functions $(\mathbb{N} \to 2) → \mathbb{N}$ are uniformly continuous".

Johnstone's topological topos (1979) would do the job, except that it is built using classical ingredients. This topos has siblings by Mike Fourman (1982) and van der Hoeven and Moerdijk (1984) with aims similar to ours, as explained in our own 2013 and 2016 papers, which give a third sibling.

Johnstone's topological topos is very easy to describe: take the monoid of continuous endomaps of the one-point compactification of the discrete natural numbers, considered as a category, then take sheaves for the canonical coverage. Van der Hoeven and Moerdijk's topos is similar: this time take the monoid of continuous endomaps of the Baire space, with the "open-cover coverage". Fourman's topos is constructed from a site of formal spaces or locales, with a similar coverage.

Our topos is also similar: we take the monoid of uniformly continuous endomaps of the Cantor space. Because it is not provable in neutral mathematics that continuous functions on the Cantor space are automatically uniformly continuous, we explicitly ask for uniform continuity rather than just continuity. As for our coverage, we initially considered coverings of finitely many jointly surjective maps. But an equivalent, smaller coverage makes the mathematics (and the formalization) simpler: for each natural number $n$ we consider a cover with $2^n$ functions, namely the concatenation maps $(\mathbb{N} \to 2) \to (\mathbb{N} \to 2)$ defined by $\alpha \mapsto s \alpha$ for each finite binary sequence $s$ of length $n$. These functions are jointly surjective, and, moreover, have disjoint images, considerably simplifying the checking of the sheaf condition. Moreover, the coverage axiom is not only satisfied, but also is equivalent to the fact that the morphisms in our site are uniformly continuous functions. So this is a sort of "uniform-continuity coverage". Our slides (2014) illustrate these ideas with pictures and examples.

The details of the mathematics can be found in the above paper, and the Agda formalization can be found at Chuangjie's page. A few years later, we ported part of this formalization to Cubical Agda to deal properly with function extensionality (which we originally dealt with in ad hoc ways).

The integer we compute

After we construct the sheaf topos, we define a simple type theory and we interpret it in the topos. We define a "function" $(\mathbb{N} \to 2) \to \mathbb{N}$ in this type theory, without proving that it is uniformly continuous, and apply the interpretation map to get a morphism of the topos, which amounts to a uniformly continuous function. From this morphism we get the modulus of uniform continuity, which is the integer we are interested in. The interested reader can find the details in the above paper and Agda code for the paper or the substantially more comprehensive Agda code for Chuangjie's thesis.

Tarides is taking part in the Data Portability & Services Incubator (DAPSI), a 3-year EU funded project that empowers internet innovators to develop new solutions in the Data Portability field.

What is DAPSI?

The Data Portability and Services Incubator (DAPSI) is an EU funded project, under the European Commission’s Next Generation Internet (NGI) initiative. The aim of this initiave is to empower top internet innovators to develop human-centric solutions. DAPSI addresses the challenge of …

Tarides is taking part in the Data Portability & Services Incubator (DAPSI), a 3-year EU funded project that empowers internet innovators to develop new solutions in the Data Portability field.

What is DAPSI?

The Data Portability and Services Incubator (DAPSI) is an EU funded project, under the European Commission’s Next Generation Internet (NGI) initiative. The aim of this initiave is to empower top internet innovators to develop human-centric solutions. DAPSI addresses the challenge of personal data portability on the internet, as foreseen under the GDPR and make it significantly easier for citizens to have any data which is stored with one service provider transmitted directly to another provider.

Take a look at the DAPSI innovators portfolio to see more information about the selected projects.

What is our project?

Our project, called SCoP for Secure-by-design Communication Protocols, is taking part in the DAPSI to tackle data portability issues in communication services.

Over the past few decades, the usage of emails has been massively widespread by both individuals and companies. Billions of emails are sent every day and this number is expected to increase to reach 333 billion of emails exchanged daily in 2022. Moreover, as managing internet communication stacks have become increasingly complex, end-users have tended to entrust this task to third-party companies like Google and Microsoft. Furthermore, existing implementations of these communication services rely on ad-hoc methodologies and memory-unsafe languages, where minor developer errors can easily escalate into major security flaws. The centralization of these communication services means that a single successful attack leads to major personal data breaches.

To fix this issue, our project aims to engineer a modern basis for open messaging that supports existing protocols such as emails but is also extensible and customizable for emerging protocols such as matrix. We will be building trustable implementations of these open protocols using type-safe languages and we will deploy these implementations as specialized, secure and resource efficient unikernels. They will become the basis of the communication system of OSMOSE, Tarides’ commercial solution for secure-by-design IoT infrastructure.

Every component of that system will be carefully designed as independent libraries, using modern development techniques to avoid the common reported threats and flaws. For instance, the implementation of protocol parsers and serializers will be written in a type-safe language and will be using fuzzing, e.g state-of-the-art coverage-driven tests. The combination of these techniques will increase users’ trust to migrate their personal data to these new secure services.

Moreover, these techniques are also useful to produce a large and reusable corpus of test materials, which we plan to release separately for other implementations to use. It will give the tools to other developers to write the next generation of messaging applications by extending the existing protocols with more confidence.

Want to be part of it?

Would you like to hear more about the project? Or want to deploy our solution? This project will build on a number of existing components in MirageOS, such as MrMime and Irmin, so feel free to contribute to these existing components! Please reach out to contact@tarides.com.

The third annual meeting of the Alt-Ergo Users’ Club took place on April 1! Our annual meeting is the ideal place to review the needs of each partner regarding Alt-Ergo. We were pleased to welcome our partners to discuss the roadmap for future Alt-Ergo developments and improvements.

Alt-Ergo is an automatic prover of mathematical formulas, jointly developed by LRI and OCamlPro (since 2014). To learn more or join the Club, visit https://alt-ergo.ocamlpro.com.

Our Club has several goa…

The third annual meeting of the Alt-Ergo Users’ Club took place on April 1! Our annual meeting is the ideal place to review the needs of each partner regarding Alt-Ergo. We were pleased to welcome our partners to discuss the roadmap for future Alt-Ergo developments and improvements.

Alt-Ergo is an automatic prover of mathematical formulas, jointly developed by LRI and OCamlPro (since 2014). To learn more or join the Club, visit https://alt-ergo.ocamlpro.com.

Our Club has several goals. Its main objective is to ensure the sustainability of Alt-Ergo by fostering collaboration between Club members and by building links with users of formal methods, such as the Why3 community. One of our priorities is to define the needs of users of constraint solvers by extending Alt-Ergo to new domains such as Model Checking, while competing with other state-of-the-art solvers in international competitions. Finally, the Club aims to find new projects or contracts for the development of long term functionalities.

We would like to thank all our members for their support: Mitsubishi Electric R&D Centre Europe, AdaCore and CEA List. We would also like to acknowledge the help of the Why3 development team with whom we work to improve our tools.

This year, new points of interest were raised by our members. Firstly, model generation, which was added to Alt-Ergo in the last edition, has been useful to the majority of our club members. Firstly, we will now focus on refining the constraints and studying how to propagate them. Secondly, we presented Dolmen: the parser/typer that will allow to type only once SMT2 files and to be ready for SMT3. Its integration to Alt-Ergo is in progress. The opinion of the club members is warm about the future contributions of the Dolmen tool to the SMT solver community!

These features are now our main priorities. You can see the boards presented at the 2021 Club meeting. To follow our progress on the new features, follow the articles on our blog!

About OCamlPro:

OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users’ Club). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: contact@ocamlpro.com.

Introduction

Tl;DR: mirage-crypto-ec, with x509 0.12.0, and tls 0.13.0, provide fast and secure elliptic curve support in OCaml and MirageOS - using the verified fiat-crypto stack (Coq to OCaml to executable which generates C code that is interfaced by OCaml). In x509, a long standing issue (countryName encoding), and archive (PKCS 12) format is now supported, in addition to EC keys. In tls, ECDH key exchanges are supported, and ECDSA and EdDSA certificates.

Elliptic curve cryptography

Since May…

Introduction

Tl;DR: mirage-crypto-ec, with x509 0.12.0, and tls 0.13.0, provide fast and secure elliptic curve support in OCaml and MirageOS - using the verified fiat-crypto stack (Coq to OCaml to executable which generates C code that is interfaced by OCaml). In x509, a long standing issue (countryName encoding), and archive (PKCS 12) format is now supported, in addition to EC keys. In tls, ECDH key exchanges are supported, and ECDSA and EdDSA certificates.

Elliptic curve cryptography

Since May 2020, our OCaml-TLS stack supports TLS 1.3 (since tls version 0.12.0 on opam).

TLS 1.3 requires elliptic curve cryptography - which was not available in mirage-crypto (the maintained fork of nocrypto).

There are two major uses of elliptic curves: key exchange (ECDH) for establishing a shared secret over an insecure channel, and digital signature (ECDSA) for authentication, integrity, and non-repudiation. (Please note that the construction of digital signatures on Edwards curves (Curve25519, Ed448) is called EdDSA instead of ECDSA.)

Elliptic curve cryptoraphy is vulnerable to various timing attacks - have a read of the overview article on ECDSA. When implementing elliptic curve cryptography, it is best to avoid these known attacks. Gladly, there are some projects which address these issues by construction.

In addition, to use the code in MirageOS, it should be boring C code: no heap allocations, only using a very small amount of C library functions -- the code needs to be compiled in an environment with nolibc.

Two projects started in semantics, to solve the issue from the grounds up: fiat-crypto and hacl-star: their approach is to use a proof system (Coq or F* to verify that the code executes in constant time, not depending on data input. Both projects provide as output of their proof systems C code.

For our initial TLS 1.3 stack, Clément, Nathan and Etienne developed fiat-p256 and hacl_x5519. Both were one-shot interfaces for a narrow use case (ECDH for NIST P-256 and X25519), worked well for their purpose, and allowed to gather some experience from the development side.

Changed requirements

Revisiting our cryptography stack with the elliptic curve perspective had several reasons, on the one side the customer project NetHSM asked for feasibility of ECDSA/EdDSA for various elliptic curves, on the other side DNSSec uses elliptic curve cryptography (ECDSA), and also wireguard relies on elliptic curve cryptography. The number of X.509 certificates using elliptic curves is increasing, and we don't want to leave our TLS stack in a state where it can barely talk to a growing number of services on the Internet.

Looking at hacl-star, their support is limited to P-256 and Curve25519, any new curve requires writing F*. Another issue with hacl-star is C code quality: their C code does neither compile with older C compilers (found on Oracle Linux 7 / CentOS 7), nor when enabling all warnings (> 150 are generated). We consider the C compiler as useful resource to figure out undefined behaviour (and other problems), and when shipping C code we ensure that it compiles with -Wall -Wextra -Wpedantic --std=c99 -Werror. The hacl project ships a bunch of header files and helper functions to work on all platforms, which is a clunky ifdef desert. The hacl approach is to generate a whole algorithm solution: from arithmetic primitives, group operations, up to cryptographic protocol - everything included.

In contrast, fiat-crypto is a Coq development, which as part of compilation (proof verification) generates executables (via OCaml code extraction from Coq). These executables are used to generate modular arithmetic (as C code) given a curve description. The generated C code is highly portable, independent of platform (word size is taken as input) - it only requires a <stdint.h>, and compiles with all warnings enabled (once a minor PR got merged). Supporting a new curve is simple: generate the arithmetic code using fiat-crypto with the new curve description. The downside is that group operations and protocol needs to implemented elsewhere (and is not part of the proven code) - gladly this is pretty straightforward to do, especially in high-level languages.

Working with fiat-crypto

As mentioned, our initial fiat-p256 binding provided ECDH for the NIST P-256 curve. Also, BoringSSL uses fiat-crypto for ECDH, and developed the code for group operations and cryptographic protocol on top of it.

The work needed was (a) ECDSA support and (b) supporting more curves (let's focus on NIST curves). For ECDSA, the algorithm requires modular arithmetics in the field of the group order (in addition to the prime). We generate these primitives with fiat-crypto (named npYYY_AA) - that required a small fix in decoding hex. Fiat-crypto also provides inversion since late October 2020, paper - which allowed to reduce our code base taken from BoringSSL. The ECDSA protocol was easy to implement in OCaml using the generated arithmetics.

Addressing the issue of more curves was also easy to achieve, the C code (group operations) are macros that are instantiated for each curve - the OCaml code are functors that are applied with each curve description.

Thanks to the test vectors (as structured data) from wycheproof (and again thanks to Etienne, Nathan, and Clément for their OCaml code decodin them), I feel confident that our elliptic curve code works as desired.

What was left is X25519 and Ed25519 - dropping the hacl dependency entirely felt appealing (less C code to maintain from fewer projects). This turned out to require more C code, which we took from BoringSSL. It may be desirable to reduce the imported C code, or to wait until a project on top of fiat-crypto which provides proven cryptographic protocols is in a usable state.

To avoid performance degradation, I distilled some X25519 benchmarks, turns out the fiat-crypto and hacl performance is very similar.

Achievements

The new opam package mirage-crypto-ec is released, which includes the C code generated by fiat-crypto (including inversion), point operations from BoringSSL, and some OCaml code for invoking these functions and doing bounds checks, and whether points are on the curve. The OCaml code are some functors that take the curve description (consisting of parameters, C function names, byte length of value) and provide Diffie-Hellman (Dh) and digital signature algorithm (Dsa) modules. The nonce for ECDSA is computed deterministically, as suggested by RFC 6979, to avoid private key leakage.

The code has been developed in NIST curves, removing blinding (since we use operations that are verified to be constant-time), added missing length checks (reported by Greg), curve25519, a fix for signatures that do not span the entire byte size (discovered while adapting X.509), fix X25519 when the input has offset <> 0. It works on x86 and arm, both 32 and 64 bit (checked by CI). The development was partially sponsored by Nitrokey.

What is left to do, apart from further security reviews, is performance improvements, Ed448/X448 support, and investigating deterministic k for P521. Pull requests are welcome.

When you use the code, and encounter any issues, please report them.

Layer up - X.509 now with ECDSA / EdDSA and PKCS 12 support, and a long-standing issue fixed

With the sign and verify primitives, the next step is to interoperate with other tools that generate and use these public and private keys. This consists of serialisation to and deserialisation from common data formats (ASN.1 DER and PEM encoding), and support for handling X.509 certificates with elliptic curve keys. Since X.509 0.12.0, it supports EC private and public keys, including certificate validation and issuance.

Releasing X.509 also included to go through the issue tracker and attempt to solve the existing issues. This time, the "country name is encoded as UTF8String, while RFC demands PrintableString" filed more than 5 years ago by Reynir, re-reported by Petter in early 2017, and again by Vadim in late 2020, was fixed by Vadim.

Another long-standing pull request was support for PKCS 12, the archive format for certificate and private key bundles. This has been developed and merged. PKCS 12 is a widely used and old format (e.g. when importing / exporting cryptographic material in your browser, used by OpenVPN, ...). Its specification uses RC2 and 3DES (see this nice article), which are the default algorithms used by openssl pkcs12.

One more layer up - TLS

In TLS we are finally able to use ECDSA (and EdDSA) certificates and private keys, this resulted in slightly more complex configuration - the constraints between supported groups, signature algorithms, ciphersuite, and certificates are intricate:

The ciphersuite (in TLS before 1.3) specifies which key exchange mechanism to use, but also which signature algorithm to use (RSA/ECDSA). The supported groups client hello extension specifies which elliptic curves are supported by the client. The signature algorithm hello extension (TLS 1.2 and above) specifies the signature algorithm. In the end, at load time the TLS configuration is validated and groups, ciphersuites, and signature algorithms are condensed depending on configured server certificates. At session initiation time, once the client reports what it supports, these parameters are further cut down to eventually find some suitable cryptographic parameters for this session.

From the user perspective, earlier the certificate bundle and private key was a pair of X509.Certificate.t list and Mirage_crypto_pk.Rsa.priv, now the second part is a X509.Private_key.t - all provided constructors have been updates (notably X509_lwt.private_of_pems and Tls_mirage.X509.certificate).

Finally, conduit and mirage

Thanks to Romain, conduit* 4.0.0 was released which supports the modified API of X.509 and TLS. Romain also developed patches and released mirage 3.10.3 which supports the above mentioned work.

Conclusion

Elliptic curve cryptography is now available in OCaml using verified cryptographic primitives from the fiat-crypto project - opam install mirage-crypto-ec. X.509 since 0.12.0 and TLS since 0.13.0 and MirageOS since 3.10.3 support this new development which gives rise to smaller EC keys. Our old bindings, fiat-p256 and hacl_x25519 have been archived and will no longer be maintained.

Thanks to everyone involved on this journey: reporting issues, sponsoring parts of the work, helping with integration, developing initial prototypes, and keep motivating me to continue this until the release is done.

In the future, it may be possible to remove zarith and gmp from the dependency chain, and provide EC-only TLS servers and clients for MirageOS. The benefit will be much less C code (libgmp-freestanding.a is 1.5MB in size) in our trusted code base.

Another potential project that is very close now is a certificate authority developed in MirageOS - now that EC keys, PKCS 12, revocation lists, ... are implemented.

Footer

If you want to support our work on MirageOS unikernels, please donate to robur. I'm interested in feedback, either via twitter, hannesm@mastodon.social or an issue on the data repository.

Have you heard about our Try-Alt-Ergo website? Created in 2014 (see our blogpost), the first objective was to facilitate access to our performant SMT Solver Alt-Ergo. Try-Alt-Ergo allows you to write and run your problems in your browser without any server computation.

This playground website has been maintained by OCamlPro for many years, and it’s high time to bring it back to life with new updates. We are therefore pleased to announce the new version of the Try-Alt-Ergo website! In t…

Have you heard about our Try-Alt-Ergo website? Created in 2014 (see our blogpost), the first objective was to facilitate access to our performant SMT Solver Alt-Ergo. Try-Alt-Ergo allows you to write and run your problems in your browser without any server computation.

This playground website has been maintained by OCamlPro for many years, and it’s high time to bring it back to life with new updates. We are therefore pleased to announce the new version of the Try-Alt-Ergo website! In this article, we will first explain what has changed in the back end, and what you can use if you are interested in running your own version of Alt-Ergo on a website, or in an application! And then we will focus on the new front-end of our website, from its interface to its features through its tutorial about the program.

Try-Alt-Ergo 2014

Try-Alt-Ergo was designed to be a powerful and simple tool to use. Its interface was minimalist. It offered three panels, one panel (left) with a text area containing the problem to prove. The centered panel was composed of a button to run Alt-Ergo, load examples, set options. The right panel showed these options, examples and other information. This design lacked some features that have been added to our solver through the years. Features such as models (counter-examples), unsat-core, more options and debug information was missing in this version.

Try-Alt-Ergo did not offer a proper editor (with syntax coloration), a way to save the file problem nor an option to limit the run of the solver with a time limit. Another issue was about the thread. When the solver was called the webpage froze, that behavior was problematic in case of the long run because there was no way to stop the solver.

Alt-Ergo 1.30

The 1.30 version of Alt-Ergo was the version used in the back-end to prove problems. Since this version, a lot of improvements have been done in Alt-Ergo. To learn more about these improvements, see our changelog in the documentation.

Over the years we encountered some difficulties to update the Alt-Ergo version used in Try-Alt-Ergo. We used Js_of_ocaml to compile the OCaml code of our solver to be runnable as a JavaScript code. Some libraries were not available in JavaScript and we needed to manually disable them. The lack of automatism leads to a lack of time to update the JavaScript version of Alt-Ergo in Try-Alt-Ergo.

In 2019 we switched our build system to dune which opens the possibility to ease the cross-compilation of Alt-Ergo in JavaScript.

New back-end

With some simple modification, we were able to compile Alt-Ergo in JavaScript. This modification is simple enough that this process is now automated in our continuous integration. This will enable us to easily provide a JavaScript version of our Solver for each future version.

Two ways of using our solver in JavaScript are available:

• alt-ergo.js, a JavaScript version of the Alt-Ergo CLI. It can be runned with node: node alt-ergo.js <options> <file>. Note that this code is slower than the natively compiled CLI of Alt-Ergo.
  In our effort to open the SMT world to more people, an npm package is the next steps of this work.
• alt-ergo-worker.js, a web worker of Alt-Ergo. This web worker needs JSON file to input file problem, options into Alt-Ergo and to returns its answers:
  • Options are sent as a list of couple name:value like:
    {"debug":true,
"input_format":"Native",
"steps_bound":100,
"sat_solver": "Tableaux",
"file":"test-file"}
    You can specify all options used in Alt-Ergo. If some options are missing, the worker uses the default value for these options. For example, if debug is not specified the worker will use its defaults value :false.
  • Input file is sent as a list of string, with the following format:
    { "content": [ "goal g: true"] }
  • Alt-Ergo answers can be composed with its results, debug information, errors, warnings …
    { "results": [ "File \"test-file\", line 1, characters 9-13: Valid (0.2070) (0 steps) (goal g) ] ,
"debugs": [ "[Debug][Sat_solver]", "use Tableaux-like solver"] }
    like the options, a result value like debugs does not contains anything, "debugs": [...] is not returned.
  • See the Alt-Ergo web-worker documentation to learn more on how to use it.

New Front-end

The Try-Alt-Ergo has been completely reworked and we added some features:

• The left panel is still composed in an editor and answers area
  • Ace editor with custom syntax coloration (both native and smt-lib2) is now used to make it more pleasant to write your problems.
• A top panel that contains the following buttons:
  • Ask Alt-Ergo which retrieves content from the editor and options, launch the web worker and print answers in the defined areas.
  • Load and Save files.
  • Documentation, that sends users to the newly added native syntax documentation of Alt-Ergo.
  • Tutorial, that opens an interactive tutorial to introduce you to Alt-Ergo native syntax and program verification.
    

• A right panel composed of tabs:
  • Start and About that contains general information about Alt-Ergo, Try-Alt-Ergo and how to use it.
  • Outputs prints more information than the basic answer area under the editor. In these tabs you can find debugs (long) outputs, unsat-core or models (counter-example) generated by Alt-Ergo.
  • Options contains every option you can use, such as the time limit / steps limit or to set the format of the input file to prove .
  • Statistics is still a basic tab that only output axioms used to prove the input problem.
  • Examples contains some basic examples showing the capabilities of our solver.

We hope you will enjoy this new version of Try-Alt-Ergo, we can’t wait to read your feedback!

This work was done at OCamlpro.

About OCamlPro:

OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users’ Club). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: contact@ocamlpro.com.

I’ve been running QubesOS as my main desktop since 2015. It provides good security, by running applications in different Xen VMs. However, it is also quite slow and has some hardware problems. I’ve recently been trying out NixOS, KVM, Wayland and SpectrumOS, and attempting to create something similar with more modern/compatible/faster technology.

This post gives my initial impressions of these tools and describes my current setup.

Table of Contents

• QubesOS
• NixOS
  • nix-store

I’ve been running QubesOS as my main desktop since 2015. It provides good security, by running applications in different Xen VMs. However, it is also quite slow and has some hardware problems. I’ve recently been trying out NixOS, KVM, Wayland and SpectrumOS, and attempting to create something similar with more modern/compatible/faster technology.

This post gives my initial impressions of these tools and describes my current setup.

Table of Contents

• QubesOS
• NixOS
  • nix-store
  • nix-instantiate
  • nix-pkgs
  • nix-env
  • NixOS
  • Installing NixOS
  • Thoughts on NixOS
• Why use virtual machines?
• SpectrumOS
• Wayland
  • Protocol
  • Copying text
  • Security
• Future work

( this post also appeared on Hacker News and Lobsters )

QubesOS

QubesOS aims to provide “a reasonably secure operating system”. It does this by running multiple virtual machines under the Xen hypervisor. Each VM’s windows have a different colour and tag, but they appear together as a single desktop. The VMs I run include:

• com for email and similar (the only VM that sees my email password).
• dev for software development.
• shopping (the only VM that sees my card number).
• personal (with no Internet access)
• untrusted (general browsing)

The desktop environment itself is another Linux VM (dom0), used for managing the other VMs. Most of the VMs are running Fedora (the default for Qubes), although I run Debian in dev. There are also a couple of system VMs; one for dealing with the network hardware, and one providing a firewall between the VMs.

You can run qvm-copy in a VM to copy a file to another VM. dom0 pops up a dialog box asking which VM should receive the file, and it arrives there as ~/QubesIncoming/$source_vm/$file. You can also press Ctrl-Shift-C to copy a VM’s clipboard to the global clipboard, and then press Ctrl-Shift-V in a window of the target VM to copy to that VM’s clipboard, ready for pasting into an application.

I think Qubes does a very good job at providing a secure environment.

However, it has poor hardware compatibility and it feels sluggish, even on a powerful machine. I bought a new machine a while ago and found that the motherboard only provided a single video output, limited to 30Hz. This meant I had to buy a discrete graphics card. With the card enabled, the machine fails to resume from suspend, and locks up from time to time (it’s completely stable with the card removed or disabled). I spent some time trying to understand the driver code, but I didn’t know enough about graphics, the Linux kernel, PCI suspend, or Xen to fix it.

I was also having some other problems with QubesOS:

• Graphics performance is terrible (especially on a 4k monitor). Qubes disables graphics acceleration in VMs for security reasons, but it was slow even for software rendering.
• It recently started freezing for a couple of seconds from time to time - annoying when you’re trying to type.
• It uses LVM thin-pools for VM storage, which I don’t understand, and which sometimes need repairing (haven’t lost any data, though).
• dom0 is out-of-date and generally not usable. This is intentional (you should be using VMs), but my security needs aren’t that high and it would be nice to be able to do video conferencing these days. Also, being able to print over USB and use bluetooth would be handy.

Anyway, I decided it was time to try something new. Linux now has its own built-in hypervisor (KVM), and I thought that would probably work better with my hardware. I was also keen to try out Wayland, which is built around shared-memory and I thought it might therefore work better with VMs. How easy would it be to recreate a Qubes-like environment directly on Linux?

NixOS

I’ve been meaning to try NixOS properly for some time. Ever since I started using Linux, its package management has struck me as absurd. On Debian, Fedora, etc, installing a package means letting it put files wherever it likes; which effectively gives the package author root on your system. Not a good base for sandboxing!

Also, they make it difficult to try out 3rd-party software, or to test newer versions of just some packages.

In 2003 I created 0install to address these problems, and Nix has very similar goals. I thought Nix was a few years younger, but looking at its Git history the first commit was on Mar 12, 2003. I announced the first preview of 0install just two days later, so both projects must have started writing code within a few days of each other!

NixOS is made up of quite a few components. Here is what I’ve learned so far:

nix-store

The store holds the files of all the programs, and is the central component of the system. Each version of a package goes in its own directory (or file), at /nix/store/$HASH. You can add data to the store directly, like this:

1
2
3
4
5
6
7

$ echo hello > file

$ nix-store --add-fixed sha256 file
/nix/store/1vap48aqggkk52ijn2prxzxv7cnzvs0w-file

$ cat /nix/store/1vap48aqggkk52ijn2prxzxv7cnzvs0w-file
hello

Here, the store location is calculated from the hash of the contents of the file we added (as with 0install store add or git hash-object).

However, you can also add things to the store by asking Nix to run a build script. For example, to compile some source code:

1. You add the source code and some build instructions (a “derivation” file) to the store.
2. You ask the store to build the derivation. It runs your build script in a container sandbox.
3. The results are added to the store, using the hash of the build instructions (not the hash of the result) as the directory name.

If a package in the store depends on another one (at build time or run time), it just refers to it by its full path. For example, a bash script in the store will start something like:

1
2

#! /nix/store/vnyfysaya7sblgdyvqjkrjbrb0cy11jf-bash-4.4-p23/bin/bash
...

If two users want to use the same build instructions, the second one will see that the hash already exists and can just reuse that. This allows users to compile software from source and share the resulting binaries, without having to trust each other.

Ideally, builds should be reproducible. To encourage this, builds which use the hash of the build instructions for the result path are built in a sandbox without network access. So, you can’t submit a build job like “Download and compile whatever is the latest version of Vim”. But you can discover the latest version yourself and then submit two separate jobs to the store:

1. “Download Vim 8.2, with hash XXX” (a fixed-output job, which therefore has network access)
2. “Build Vim from hash XXX”

You can run nix-collect-garbage to delete everything from the store that isn’t reachable via the symlinks under /nix/var/nix/gcroots/. Users can put symlinks to things they care about keeping in /nix/var/nix/gcroots/per-user/$USER/.

By default, the store is also configured with a trusted binary cache service, and will try to download build results from there instead of compiling locally when possible.

nix-instantiate

Writing derivation files by hand is tedious, so Nix provides a templating language to create them easily. The Nix language is dynamically typed and based around maps/dictionaries (which it confusingly refers to as “sets”). nix-instantiate file.nix will generate a derivation from file.nix and add it to the store.

An Nix file looks like this:

1

derivation { system = "x86_64-linux"; builder = ./myfile; name = "foo"; }

Running nix-instantiate on this will:

1. Add myfile to the store.
2. Add the generated foo.drv to the store, including the full store path of myfile.

nix-pkgs

Writing Nix expressions for every package you want would also be tedious. The nixpkgs Git repository contains a Nix expression that evaluates to a set of derivations, one for each package in the distribution. It also contains a library of useful helper functions for packages (e.g. it knows how to handle GNU autoconf packages automatically).

Rather than evaluating the whole lot, you use -A to ask for a single package. For example, you can use nix-instantiate ./nixpkgs/default.nix -A firefox to generate a derivation for Firefox.

nix-build is a quick way to create a derivation with nix-instantiate and build it with nix-store. It will also create a ./result symlink pointing to its path in the store, as well as registering ./result with the garbage collector under /nix/var/nix/gcroots/auto/. For example, to build and run Firefox:

1
2

nix-build ./nixpkgs/default.nix -A firefox
./result/bin/firefox

If you use nixpkgs without making any changes, it will be able to download a pre-built binary from the cache service.

nix-env

Keeping track of all these symlinks would be tedious too, but you can collect them all together by making a package that depends on every application you want. Its build script will produce a bin directory full of symlinks to the applications. Then you could just point your $PATH variable at that bin directory in the store.

To make updating easier, you will actually add ~/.nix-profile/bin/ to $PATH and update .nix-profile to point at the latest build of your environment package.

This is essentially what nix-env does, except with yet more symlinks to allow for switching between multiple profiles, and to allow rolling back to previous environments if something goes wrong.

For example, to install Firefox so you can run it via $PATH:

1

nix-env -i firefox

NixOS

Finally, just as nix-env can create a user environment with bin, man, etc, a similar process can create a root filesystem for a Linux distribution.

nixos-rebuild reads the /etc/nixos/configuration.nix configuration file, generates a system environment, and then updates grub and the /run/current-system symlink to point to it.

In fact, it also lists previous versions of the system environment in the grub file, so if you mess up the configuration you can just choose an earlier one from the boot menu to return to that version.

Installing NixOS

To install NixOS you boot one of the live images at https://nixos.org. Which you use only affects the installation UI, not the system you end up with.

The manual walks you through the installation process, showing how to partition the disk, format and mount the partitions, and how to edit the configuration file. I like this style of installation, where it teaches you things instead of just doing it for you. Most of the effort in switching to a new system is learning about it, so I’d rather spend 3 hours learning stuff following an installation guide than use a 15-minute single-click installer that teaches me nothing.

The configuration file (/etc/nixos/configuration.nix) is just another Nix expression. Most things are set to off by default (I approve), but can be changed easily. For example, if you want sound support you change that setting to sound.enable = true, and if you also want to use PulseAudio then you set hardware.pulseaudio.enable = true too.

Every system service supported by NixOS is controlled from here, with all kinds of options, from programs.vim.defaultEditor = true (so you don’t get trapped in nano) to services.factorio.autosave-interval. Use man configuration.nix to see the available settings.

NixOS defaults to an X11 desktop, but I wanted to try Wayland (and Sway). Based on the NixOS wiki instructions, I used this:

1
2
3
4
5
6
7
8
9
10
11
12
13
14

  programs.sway = {
    enable = true;
    wrapperFeatures.gtk = true; # so that gtk works properly
    extraSessionCommands = "export MOZ_ENABLE_WAYLAND=1";
    extraPackages = with pkgs; [
      swaylock
      swayidle
      xwayland
      wl-clipboard
      mako
      alacritty
      dmenu
    ];
  };

The xwayland bit is important; without that you can’t run any X11 applications.

My only complaint with the NixOS installation instructions is that following them will leave you with an unencrypted system, which isn’t very useful. When partitioning, you have to skip ahead to the LUKS section of the manual, which just gives some options but no firm advice. I created two primary partitions: a 1G unencrypted /boot, and a LUKS partition for the rest of the disk. Then I created an LVM volume group from the /dev/mapper/crypted device and added the other partitions in that.

Once the partitions are mounted and the configuration file is complete, nixos-install downloads everything and configures grub. Then you reboot into the new system.

Once running the new system you can made further edits to the configuration file there in the same way, and use nixos-rebuild switch to generate a new system. It seems to be pretty good at updating the running system to the new settings, so you don’t normally need to reboot after making changes.

The big mistake I made was forgetting to add /boot to fstab. When I ran nixos-rebuild it put all the grub configuration on the encrypted partition, rendering the system unbootable. I fixed that with chattr +i /boot on the unmounted partition. That way, trying to rebuild with /boot unmounted will just give an error message.

Thoughts on NixOS

I’ve been using the system for a few weeks now and I’ve had no problems with Nix so far. Nix has been fast and reliable and there were fairly up-to-date packages for everything I wanted (I’m using the stable release). There is a lot to learn, but plenty of documentation.

When I wanted a newer package (socat with vsock support, only just released) I just told Nix to install it from the latest Git checkout of nixpkgs. Unlike on Debian and similar systems, doing this doesn’t interfere with any other packages (such as forcing a system-wide upgrade of libc).

I think Nix does download more data than most other systems, but networks are fast enough now that it doesn’t seem to matter. For example, let’s say you’re running Python 3.9.0 and you want to update to 3.9.1:

• With Debian: apt-get upgrade downloads the new version, which gets unpacked over the old one. As the files are unpacked, the system moves through an exciting series of intermediate states no-one has thought about. Running programs may crash as they find their library versions changing under them (though it’s usually OK). Only root can update software.

• With 0install: 0install update downloads the new version, unpacking it to a new directory. Running programs continue to use the old version. When a new program is started, 0install notices the update and runs the solver again. If the program is compatible with the new Python then it uses that. If not, it continues with the old one. You can run any previous version if there is a problem.

• With Nix: nix-env -u downloads the new version, unpacking it to a new directory. It also downloads (or rebuilds) every package depending on Python, creating new directories for each of them. It then creates a new environment with symlinks to the latest version of everything. Running programs continue to use the old version. Starting a new program will use the new version. You can revert the whole environment back to the previous version if there is a problem.

• With Docker: docker pull downloads the new version of a single application, downloading most or all of the application’s packages, whether Python related or not. Existing containers continue running with the old version. New containers will default to using the new version. You can specify which version to use when starting a program. Other applications continue using the old version of Python until their authors update them (you must update each application individually, rather than just updating Python itself).

The main problem with NixOS is that it’s quite different to other Linux systems, so there’s a lot to relearn. Also, existing knowledge about how to edit fstab, sudoers, etc, isn’t so useful, as you have to provide all configuration in Nix syntax. However, having a single (fairly sane) syntax for everything is a nice bonus, and being able to generate things using the templating language is useful. For example, for my network setup I use a bunch of tap devices (one for each of my VMs). It was easy to write a little Nix function (mktap) to generate them all from a simple list. Here’s that section of my configuration.nix:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

  networking = {
    useDHCP = false;
    interfaces =
      let mktap = ip: {
          virtual = true;
          virtualOwner = "tal";
          ipv4.addresses = [
            { address = ip; prefixLength = 31; }
          ];
        };
      in
      {
        eno2.useDHCP = true;
        wlo1.useDHCP = true;
        tapdev = mktap "10.0.0.2";
        tapcom = mktap "10.0.0.4";
        tapshopping = mktap "10.0.0.6";
        tapbanking = mktap "10.0.0.8";
        tapuntrusted = mktap "10.0.0.10";
      };
    nat = {
      enable = true;
      externalInterface = "eno2";
      internalIPs = [ "10.0.0.0/8" ];
    };
  };

Overall, I’m very happy with NixOS so far.

Why use virtual machines?

With NixOS I had a nice host environment, but after using Qubes I wanted to run my applications in VMs.

The basic problem is that Linux is the only thing that knows how to drive all the hardware, but Linux security is not ideal. There are several problems:

1. Linux is written in C. This makes security bugs rather common and, more importantly, means that a bug in one part of the code can impact any other part of the code. Nothing is secure unless everything is secure.
2. Linux has a rather large API (hundreds of syscalls).
3. The Linux (Unix) design predates the Internet, and security has been somewhat bolted on afterwards.

For example, imagine that we want to run a program with access to the network, but not to the graphical display. We can create a new Linux container for it using bubblewrap, like this:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

$ ls -l /run/user/1000/wayland-0 /tmp/.X11-unix/X0
srwxr-xr-x 1 tal users 0 Feb 18 16:41 /run/user/1000/wayland-0
srwxr-xr-x 1 tal users 0 Feb 18 16:41 /tmp/.X11-unix/X0

$ bwrap \
    --ro-bind / / \
    --dev /dev \
    --tmpfs /home/tal \
    --tmpfs /run/user \
    --tmpfs /tmp \
    --unshare-all --share-net \
    bash

$ ls -l /run/user/1000/wayland-0 /tmp/.X11-unix/X0
ls: cannot access '/run/user/1000/wayland-0': No such file or directory
ls: cannot access '/tmp/.X11-unix/X0': No such file or directory

The container has an empty home directory, empty /tmp, and no access to the display sockets. If we run Firefox in this environment then… it opens its window just fine! How? strace shows what happened:

1
2
3

connect(4, {sa_family=AF_UNIX, sun_path="/run/user/1000/wayland-0"}, 27) = -1 ENOENT (No such file or directory)
socket(AF_UNIX, SOCK_STREAM|SOCK_CLOEXEC, 0) = 4
connect(4, {sa_family=AF_UNIX, sun_path=@"/tmp/.X11-unix/X0"}, 20) = 0

After failing to connect to Wayland, it then tried using X11 (via Xwayland) instead. Why did that work? If the first byte of the socket pathname is \0 then Linux instead interprets it as an “abstract” socket address, not subject to the usual filesystem permission rules.

Trying to anticipate these kinds of special cases is just too much work. Linux really wants everything on by default, and you have to find and disable every feature individually. By contrast, virtual machines tend to have integrations with the host off by default. The also tend to have much smaller APIs (e.g. just reading and writing disk blocks or network frames), with the rich Unix API entirely inside the VM, provided by a separate instance of Linux.

SpectrumOS

I was able to set up a qemu guest and restore my dev Qubes VM in that, but it didn’t integrate nicely with the rest of the desktop. Installing ssh allowed me to connect in with ssh -Y dev, allowing apps in the VM to open an X connection to Xwayland on the host. That was somewhat usable, but still a bit slower than Qubes had been (which was already a bit too slow).

Searching for a way to forward the Wayland connection directly, I came across the SpectrumOS project. SpectrumOS aims to use one virtual machine per application, using shared directories so that VM files are stored on the host, simplifying management. It uses crosvm from the ChromiumOS project instead of qemu, because it has a driver that allows forwarding Wayland connections (and also because it’s written in Rust rather than C). The project’s single developer is currently taking a break from the project, and says “I’m currently working towards a proof of concept”.

However, there is some useful stuff in the SpectrumOS repository (which is a fork of nixpkgs). In particular, it contains:

• A version of Linux with the virtwl kernel module, which connects to crosvm’s Wayland driver.
• A package for sommelier, which connects applications to virtwl.
• A Nix expression to build a root filesystem for the VM.

Building that, I was able to run the project’s demo, which runs the Wayfire compositor inside the VM, appearing in a window on the host. Dragging the nested window around, the pixels flowed smoothly across my screen in exactly the way that pixels on QubesOS don’t.

This was encouraging, but I didn’t want to run a nested window manager. I tried running Firefox directly (without Wayfire), but it complained that sommelier didn’t provide a new enough version of something, and running weston-terminal immediately segfaulted sommelier.

Why do we need the sommelier process anyway? The problem is that, while virtwl mostly proxies Wayland messages directly, it can’t send arbitrary FDs to the host. For example, if you want to forward a writable stream from an application to virtwl you must first create a pipe from the host using a special virtwl ioctl, then read from that and copy the data to the application’s regular Linux pipe.

With help from the mailing list, I managed to get it somewhat usable:

• I enabled VIRTIO_FS, allowing me to mount a host directory into the VM (for sharing files).
• I created some tap devices (as mentioned above) to get guest networking going.
• Adding ext4 to the kernel image allowed me to mount the VM’s LVM partition.
• Setting FONTCONFIG_FILE got some usable fonts (otherwise, there was no monospace font for the terminal).
• I hacked sommelier to claim it supported the latest protocols, which got Firefox running.
• Configuring sommelier for Xwayland let X applications run.
• I replaced the non-interactive bash shell with fish so I could edit commands.
• I ran (while true; do socat vsock-listen:5000 exec:dash; done) at the end of the VM’s boot script. Then I could start e.g. the VM’s Firefox with echo 'firefox&' | socat stdin vsock-connect:7:5000 on the host, allowing me to add launchers for guest applications.

Making changes to the root filesystem was fairly easy once I’d read the Nix manuals. To add an application (e.g. libreoffice), you import it at the start of rootfs/default.nix and add it to the path variable. The Nix expression gets the transitive dependencies of path from the Nix store and packs them into a squashfs image.

True, my squashfs image is getting a bit big. Maybe I should instead make a minimal squashfs boot image, plus a shared directory of hard links to the required files. That would allow sharing the data with the host. I could also just share the whole /nix/store directory, if I wanted to make all host software available to guests.

I made another Nix script to add various VM boot commands to my host environment. For example, running qvm-start-shopping boots my shopping VM using crosvm, with the appropriate LVM data partition, network settings, and shared host directory.

I think, ideally, this would be a systemd socket-activated user service rather than a shell script. Then attempting to run Firefox by sending a command to the VM socket would cause systemd to boot the VM (if not already running). For now, I boot each VM manually in a terminal and then press Win-Shift-2 to banish it to workspace 2, with all the other VM root consoles.

The virlwl Wayland forwarding feels pretty fast (much faster than Qubes’ X graphics).

Wayland

I now had a mostly functional Qubes-like environment, running most of my applications in VMs, with their windows appearing on the host desktop like any other application. However, I also had some problems:

• A stated goal of Wayland is “every frame is perfect”. However, applications generally seemed to open at the wrong size and then jump to their correct size, which was a bit jarring.
• Vim opened its window with the scrollbar at the far left of the window, making the text invisible until you resized the window.
• Wayland is supposed to have better support for high-DPI displays. However, this doesn’t work with Xwayland, which turns everything blurry, and the recommended work-around is to use a scale-factor of 1 and configure each application to use bigger fonts. This is easy enough with X applications (e.g. set ft.dpi: 150 with xrdb), but Wayland apps must be configured individually.
• Wayland doesn’t have cursor themes and you have to configure every application individually to use a larger cursor too.
• Copying text didn’t seem to work reliably. Sometimes there would be a long delay, after which the text might or might not appear. More often, it would just paste something completely different and unexpected. Even when it did paste the right text, it would often have ^M characters inserted into it.

I decided it was time to learn more about Wayland. I discovered wayland-book.com, which does a good job of introducing it (though the book is only half finished at the moment).

Protocol

One very nice feature of Wayland is that you can run any Wayland application with WAYLAND_DEBUG=1 and it will display a fairly readable trace of all the Wayland messages it sends and receives. Let’s look at a simple application that just connects to the server (compositor) and opens a window:

1
2
3

$ WAYLAND_DEBUG=1 test.exe
-> wl_display@1.get_registry registry:+2
-> wl_display@1.sync callback:+3

The client connects to the server’s socket at /run/user/1000/wayland-0 and sends two messages to object 1 (of type wl_display), which is the only object available in a new connection. The get_registry request asks the server to add the registry to the conversation and call it object 2. The sync request just asks the server to confirm it got it, using a new callback object (with ID 3).

Both clients and servers can add objects to the conversation. To avoid numbering conflicts, clients assign low numbers and servers pick high ones.

On the wire, each message gives the object ID, the operation ID, the length in bytes, and then the arguments. Objects are thought of as being at server, so the client sends request messages to objects, while the server emits event messages from objects. At the wire level there’s no difference though.

When the server gets the get_registry request it adds the registry, which immediately emits one event for each available service, giving the maximum supported version. The client receives these messages, followed by the callback notification from the sync message:

1
2
3
4
5
6
7
8
9
10

<- wl_registry@2.global name:0 interface:"wl_compositor" version:4
<- wl_registry@2.global name:1 interface:"wl_subcompositor" version:1
<- wl_registry@2.global name:2 interface:"wl_shm" version:1
<- wl_registry@2.global name:3 interface:"xdg_wm_base" version:1
<- wl_registry@2.global name:4 interface:"wl_output" version:2
<- wl_registry@2.global name:5 interface:"wl_data_device_manager" version:3
<- wl_registry@2.global name:6 interface:"zxdg_output_manager_v1" version:3
<- wl_registry@2.global name:7 interface:"gtk_primary_selection_device_manager" version:1
<- wl_registry@2.global name:8 interface:"wl_seat" version:5
<- wl_callback@3.done callback_data:1129040

The callback tells the client it has seen all the available services, and so it now picks the ones it wants. It has to choose a version no higher than the one offered by the server. Protocols starting with wl_ are from of the core Wayland protocol; the others are extensions. The leading z in zxdg_output_manager_v1 indicates that the protocol is “unstable” (under development).

The protocols are defined in various XML files, which are scattered over the web. The core protocol is defined in wayland.xml. These XML files can be used to generate typed bindings for your programming language of choice.

Here, the application picks wl_compositor (for managing drawing surfaces), wl_shm (for sharing memory with the server), and xdg_wm_base (for desktop windows).

1
2
3

-> wl_registry@2.bind name:0 id:+4(wl_compositor:v4)
-> wl_registry@2.bind name:2 id:+5(wl_shm:v1)
-> wl_registry@2.bind name:3 id:+6(xdg_wm_base:v1)

The bind message is unusual in that the client gives the interface and version of the object it is creating. For other messages, both sides know the type from the schema, and the version is always the same as the parent object. Because the client chose the new IDs, it doesn’t need to wait for the server; it continues by using the new objects to create a top-level window:

1
2
3
4
5

-> wl_compositor@4.create_surface id:+7
-> xdg_wm_base@6.get_xdg_surface id:+8 surface:7
-> xdg_surface@8.get_toplevel id:+9
-> xdg_toplevel@9.set_title title:"example app"
-> wl_surface@7.commit 

This API is pretty strange. The core Wayland protocol says how to make generic drawing surfaces, but not how to make windows, so the application is using the xdg_wm_base extension to do that. Logically, there’s only one object here (a toplevel window), but it ends up making three separate Wayland objects representing the different aspects of it.

The commit tells the server that the client has finished setting up the window and the server should now do something with it.

The above was all in response to the callback firing. The client now processes the last message in that batch, which is the server destroying the callback:

1

<- wl_display@1.delete_id id:3

Object destruction is a bit strange in Wayland. Normally, clients ask for things to be destroyed (by sending a “destructor” message) and the server confirms by sending delete_id from object 1. But this isn’t symmetrical: there is no standard way for a client to confirm deletion when the server calls a destructor (such as the callback’s done), so these have to be handled on a case-by-case basis. Since callbacks don’t accept any messages, there is no need for the client to confirm that it got the done message and the server just sends a delete message immediately.

The client now waits for the server to respond to all the messages it sent about the new window, and gets a bunch of replies:

1
2
3
4
5
6
7
8
9

<- wl_shm@5.format format:0
<- wl_shm@5.format format:1
<- wl_shm@5.format format:875709016
<- wl_shm@5.format format:875708993
<- xdg_wm_base@6.ping serial:1129043
-> xdg_wm_base@6.pong serial:1129043
<- xdg_toplevel@9.configure width:0 height:0 states:""
<- xdg_surface@8.configure serial:1129042
-> xdg_surface@8.ack_configure serial:1129042

It gets some messages telling it what pixel formats are supported, a ping message (which the server sends from time to time to check the client is still alive), and a configure message giving the size for the new window. Oddly, Sway has set the size to 0x0, which means the client should choose whatever size it likes.

The client picks a suitable default size, allocates some shared memory (by opening a tmpfs file and immediately unlinking it), shares the file descriptor with the server (create_pool), and then carves out a portion of the memory to use as a buffer for the pixel data:

1
2
3

-> wl_shm@5.create_pool id:+3 fd:(fd) size:1228800
-> wl_shm_pool@3.create_buffer id:+10 offset:0 width:640 height:480 stride:2560 format:1
-> wl_shm_pool@3.destroy 

In this case it used the whole memory region. It could also have allocated two buffers for double-buffering. The client then draws whatever it wants into the buffer (mapping the file into its memory and writing to it directly), attaches the buffer to the window’s surface, marks the whole area as “damaged” (in need of being redrawn) and calls commit, telling the server the surface is ready for display:

1
2
3

-> wl_surface@7.attach buffer:10 x:0 y:0
-> wl_surface@7.damage x:0 y:0 width:2147483647 height:2147483647
-> wl_surface@7.commit 

At this point the window appears on the screen! The server lets the client know it has finished with the buffer and the client destroys it:

1
2
3

<- wl_display@1.delete_id id:3
<- wl_buffer@10.release 
-> wl_buffer@10.destroy 

Although the window is visible, the content is the wrong size. Sway now suddenly remembers that it’s a tiling window manager. It sends another configure event with the correct size, causing the client to allocate a fresh memory pool of the correct size, allocate a fresh buffer from it, redraw everything at the new size, and tell the server to draw it.

1
2

<- xdg_toplevel@9.configure width:1534 height:1029 states:""
...

This process of telling the client to pick a size and then overruling it explains why Firefox draws itself incorrectly at first and then flickers into position a moment later. It probably also explains why Vim tries to open a 0x0 window.

Copying text

A bit of searching revealed that the ^M problem is a known Sway bug.

However, the main reason copying text wasn’t working turned out to be a limitation in the design of the core wl_data_device_manager protocol. The normal way to copy text on X11 is to select the text you want to copy, then click the middle mouse button where you want it (or press Shift-Insert).

X also supports a clipboard mechanism, where you select text, then press Ctrl-C, then click at the destination, then press Ctrl-V. The original Wayland protocol only supports the clipboard system, not the selection, and so Wayland compositors have added selection support through extensions. Sommelier didn’t proxy these extensions, leading to failure when copying in or out of VMs.

I also found that the reason weston-terminal wouldn’t start was because I didn’t have anything in my clipboard, and sommelier was trying to dereference a null pointer.

One problem with the Wayland protocol is that it’s very hard to proxy. Although the wire protocol gives the length in bytes of each message, it doesn’t say how many file descriptors it has. This means that you can’t just pass through messages you don’t understand, because you don’t know which FDs go with which message. Also, the wire protocol doesn’t give types for FDs (nor does the schema), which is a problem for anything that needs to proxy across a VM boundary or over a network.

This all meant that VMs could only use protocols explicitly supported by sommelier, and sommelier limited the version too. Which means that supporting extra extensions or new versions means writing (and debugging) loads of C++ code.

I didn’t have time to write and debug C++ code for every missing Wayland protocol, so I took a short-cut: I wrote my own Wayland library, ocaml-wayland, and then used that to write my own version of sommelier. With that, adding support for copying text was fairly easy.

For each Wayland interface we need to handle each incoming message from the client and forward it to the host, and also forward each message from the host to the client. Here’s the code to handle the “selection” event in OCaml, which we receive from the host and send to the client (c):

1

method on_selection _ offer = C.Wl_data_device.selection c (Option.map to_client offer)

The host passes us an “offer” argument, which is a previously-created host offer object. We look up the corresponding client object with to_client and pass that as the argument to the client.

For comparison, here’s sommelier’s equivalent to this line of code, in C++:

1
2
3
4
5
6
7
8
9
10

static void sl_data_device_selection(void* data,
                                     struct wl_data_device* data_device,
                                     struct wl_data_offer* data_offer) {
  struct sl_host_data_device* host = static_cast<sl_host_data_device*>(
      wl_data_device_get_user_data(data_device));
  struct sl_host_data_offer* host_data_offer =
      static_cast<sl_host_data_offer*>(wl_data_offer_get_user_data(data_offer));

  wl_data_device_send_selection(host->resource, host_data_offer->resource);
}

I think this is a great demonstration of the difference between “type safety” and “type ceremony”. The C++ code is covered in types, making the code very hard to read, yet it crashes at runtime because it fails to consider that data_offer can be NULL.

By contract, the OCaml version has no type annotations, but the compiler would reject if I forgot to handle this (with Option.map).

Security

According to the GNOME wiki, the original justification for not supporting selection copies was “security concerns with unexpected data stealing if the mere act of selecting a text fragment makes it available to all running applications”. The implication is that applications stealing data instead from the clipboard is OK, and that you should therefore never put anything confidential on the clipboard.

This seemed a bit odd, so I read the security section of the Wayland specification to learn more about its security model. That section of the specification is fairly short, so I’ll reproduce it here in full:

Security and Authentication

• mostly about access to underlying buffers, need new drm auth mechanism (the grant-to ioctl idea), need to check the cmd stream?
• getting the server socket depends on the compositor type, could be a system wide name, through fd passing on the session dbus. or the client is forked by the compositor and the fd is already opened.

It looks like implementations have to figure things out for themselves.

The main advantage of Wayland over X11 here is that Wayland mostly isolates applications from each other. In X11 applications collaborate together to manage a tree of windows, and any application can access any window. In the Wayland protocol, each application’s connection only includes that application’s objects. Applications only get events relevant to their own windows (for example, you only get pointer motion events while the pointer is over your window). Communication between applications (e.g. copy-and-paste or drag-and-drop) is all handled though the compositor.

Also, to request the contents of the clipboard you need to quote the serial number of the mouse click or key press that triggered it. If it’s too far in the past, the compositor can ignore the request.

I’ve also heard people say that security is the reason you can’t take screenshots with Wayland. However, Sway lets you take screenshots, and this worked even from inside a VM through virtwl. I didn’t add screenshot support to the proxy, because I don’t want VMs to be able to take screenshots, but the proxy isn’t a security tool (it runs inside the VM, which isn’t trusted).

Clearly, the way to fix this was with a new compositor. One that would offer a different Wayland socket to each VM, tag the windows with the VM name, colour the frames, confirm copies across VM boundaries, and work with Vim. Luckily, I already had a handy pure-OCaml Wayland protocol library available. Unluckily, at this point I ran out of holiday.

Future work

There are quite a few things left to do here:

• One problem with virtwl is that, while we can receive shared memory FDs from the host, we can’t export guest memory to the host. This is unfortunate, because in Wayland the shared memory for window contents is allocated by the application from guest memory, and the proxy therefore has to copy each frame. If the host provided the memory to the guest, this wouldn’t be needed. There is a wl_drm protocol for allocating video memory, which might help here, but I don’t know how that works and, like many Wayland specifications, it seems to be in the process of being replaced by something else. Also, if we’re going to copy the memory, we should at least only copy the damaged region, not the whole thing. I only got this code working just far enough to run the Wayland applications I use (mainly Firefox and Evince).

• I’m still using ssh to proxy X11 connections (mainly for Vim and gitk). I’d prefer to run Xwayland in the VM, but it seems you need to provide a bit of extra support for that, which I haven’t implemented yet. Sommelier can do this, but then copying doesn’t work.

• The host Wayland compositor needs to be aware of VMs, so it can colour the titles appropriately and limit access to privileged operations.

• For the full Qubes experience, the network card should be handled by a VM, with another VM managing the firewall. Perhaps the Mirage unikernel firewall could be made to work on KVM too. I’m not sure how guest-to-guest communication works with KVM.

However, because the host NixOS environment is a fully-working Linux system, I can always trade off some security to get things working (e.g. by doing video conferencing directly on the host).

I hope the SpectrumOS project will resume at some point, or that Qubes will find a solution to its hardware compatibility and performance problems.

In collaboration with Nomadic Labs, Marigold and DaiLambda, we're happy to announce the completion of the next Tezos protocol proposal: Florence.

Tezos is an open-source decentralised blockchain network providing a platform for smart contracts and digital assets. A crucial feature of Tezos is self-amendment: the network protocol can be upgraded dynamically by the network participants themselves. This amendment process is initiated when a participant makes a proposal, which is then subject to a v…

In collaboration with Nomadic Labs, Marigold and DaiLambda, we're happy to announce the completion of the next Tezos protocol proposal: Florence.

Tezos is an open-source decentralised blockchain network providing a platform for smart contracts and digital assets. A crucial feature of Tezos is self-amendment: the network protocol can be upgraded dynamically by the network participants themselves. This amendment process is initiated when a participant makes a proposal, which is then subject to a vote. After several years working on the Tezos storage stack, this is our first contribution to a proposal; we hope that it will be the first of many!

As detailed in today's announcement from Nomadic Labs, the Florence proposal contains several important changes, from the introduction of Baking Accounts to major quality-of-life improvements for smart contract developers. Of all of these changes, we're especially excited about the introduction of sub-trees to the blockchain context API. In this post, we'll give a brief tour of what these sub-trees will bring for the future of Tezos. But first, what are they?

Merkle sub-trees

The Tezos protocol runs on top of a versioned tree called the “context”, which holds the chain state (balances, contracts etc.). Ever since the pre-Alpha era, the Tezos context has been implemented using Irmin – an open-source Merkle tree database originally written for use by MirageOS unikernels.

For MirageOS, Irmin’s key strength is flexibility: it can run over arbitrary backends. This is a perfect fit for Tezos, which must be agile and widely-deployable. Indeed, the Tezos shell has already leveraged this agility many times, all the way from initial prototypes using a Git backend to the optimised irmin-pack implementation used today.

But Irmin can do more than just swapping backends! It also allows users to manipulate the underlying Merkle tree structure of the store with a high-level API. This “Tree” API enables lots of interesting use-cases of Irmin, from mergeable data types (MRDTs) to zero-knowledge proofs. Tezos doesn't use these more powerful features directly yet; that’s where Merkle proofs come in!

Proofs and lightweight Tezos clients

Since the Tezos context keeps track of the current "state" of the blockchain, each participant needs their own copy of the tree to run transactions against. This context can grow to be very large, so it's important that it be stored as compactly as possible: this goal shaped the design of irmin-pack, our latest Irmin backend.

However, it's possible to reduce the storage requirements even further via the magic of Merkle trees: individuals only need to store a fragment of the root tree, provided they can demonstrate that this fragment is valid by sending “proofs” of its membership to the other participants.

This property can be used to support ultra-lightweight Tezos clients, a feature currently being developed by TweagIO. To make this a reality, the Tezos protocol needs fine-grained access to context sub-trees in order build Merkle proofs out of them. Fortunately, Irmin already supports this! We extended the protocol to understand sub-trees, lifting the power of Merkle trees to the user.

We’re excited to work with TweagIO and Nomadic Labs on lowering the barriers to entering the Tezos ecosystem and look forward to seeing what they achieve with sub-trees!

Efficient Merkle proof representations

Simply exposing sub-trees in the Tezos context API isn’t quite enough: lightweight clients will also need to serialize them efficiently, since proofs must be exchanged over the network to establish trust between collaborating nodes. Enter Plebeia.

Plebeia is an alternative Tezos storage layer – developed by DaiLambda – with strengths that complement those of Irmin. In particular, Plebeia is capable of generating very compact Merkle proofs. This is partly due to its specialized store structure, and partly due to clever optimizations such as path compression and inlining.

We’re working with the DaiLambda team to unite the strengths of Irmin and Plebeia, which will bring built-in Merkle proof support to the Tezos storage stack. The future is bright for Merkle proofs in Tezos!

Baking account migrations

Trees don’t just enable new features; they have a big impact on performance too! Currently, indexing into the context always happens from its root, which duplicates effort when accessing adjacent values deep in the tree. Fortunately, the new sub-trees provide a natural representation for “cursors” into the context, allowing the protocol to optimize its interactions with the storage layer.

To take just one example, DaiLambda recently exploited this feature to reduce the migration time necessary to introduce Baking Accounts to the network by a factor of 15! We’ll be teaming up with Nomadic Labs and DaiLambda to ensure that Tezos extracts every bit of performance from its storage.

It's especially exciting to have access to lightning-fast storage migrations, since this enables Tezos to evolve rapidly even as the ecosystem expands.

Storage in other languages

Of course, Tezos isn’t just an OCaml project: the storage layer also has a performant Rust implementation as part of TezEdge. We’re working with Simple Staking to bring Irmin to the Rust community via an FFI toolchain, enabling closer alignment between the different Tezos shell implementations.

Conclusion

All in all, it’s an exciting time to work on Tezos storage, with many open-source collaborators from around the world. We’re especially happy to see Tezos taking greater advantage of Irmin’s features, which will strengthen both projects and help them grow together.

If all of this sounds interesting, you can play with it yourself using the recently-released Irmin 2.5.0. Thanks for reading, and stay tuned for future Tezos development updates!

The Coq development team is proud to announce the immediate availability of the Coq Platform 2021.02.0

The Coq platform is a distribution of the Coq proof assistant together with a selection of Coq libraries. It provides a set of scripts to compile and install OPAM, Coq, Coq libraries and Coq plugins on MacOS, Windows and many Linux distributions in a reliable way with consistent results.

This release is based on Coq 8.13.1 and provides binary installers for Windows and Linux. We plan t…

The Coq development team is proud to announce the immediate availability of the Coq Platform 2021.02.0

The Coq platform is a distribution of the Coq proof assistant together with a selection of Coq libraries. It provides a set of scripts to compile and install OPAM, Coq, Coq libraries and Coq plugins on MacOS, Windows and many Linux distributions in a reliable way with consistent results.

This release is based on Coq 8.13.1 and provides binary installers for Windows and Linux. We plan to release 2021.02.1 as soon as the MacOS installer is ready. The following point releases, starting with 2021.02.2, will focus on including more Coq libraries (and no breaking change).

This is joint work with Marc Bezem, Thierry Coquand, Peter Dybjer.

We use the Burali-Forti argument to show that, in homotopy type theory and univalent foundations, the embedding $$ \mathcal{U} \to \mathcal{U}^+$$ of a universe $\mathcal{U}$ into its successor $\mathcal{U}^+$ is not an equivalence. We also establish this for the types of sets, magmas, monoids and groups. The arguments in this post are also written in Agda.

Ordinals in univalent type theory

The Burali-Forti paradox is about…

This is joint work with Marc Bezem, Thierry Coquand, Peter Dybjer.

We use the Burali-Forti argument to show that, in homotopy type theory and univalent foundations, the embedding $$ \mathcal{U} \to \mathcal{U}^+$$ of a universe $\mathcal{U}$ into its successor $\mathcal{U}^+$ is not an equivalence. We also establish this for the types of sets, magmas, monoids and groups. The arguments in this post are also written in Agda.

Ordinals in univalent type theory

The Burali-Forti paradox is about the collection of all ordinals. In set theory, this collection cannot be a set, because it is too big, and this is what the Burali-Forti argument shows. This collection is a proper class in set theory.

In univalent type theory, we can collect all ordinals of a universe $\mathcal{U}$ in a type $\operatorname{Ordinal}\,\mathcal{U}$ that lives in the successor universe $\mathcal{U}^+$: $$ \operatorname{Ordinal}\,\mathcal{U} : \mathcal{U}^+.$$ See Chapter 10.3 of the HoTT book, which uses univalence to show that this type is a set in the sense of univalent foundations (meaning that its equality is proposition valued).

The analogue in type theory of the notion of proper class in set theory is that of large type, that is, a type in a successor universe $\mathcal{U}^+$ that doesn't have a copy in the universe $\mathcal{U}$. In this post we show that the type of ordinals is large and derive some consequences from this.

We have two further uses of univalence, at least:

1. to adapt the Burali-Forti argument from set theory to our type theory, and

2. to resize down the values of the order relation of the ordinal of ordinals, to conclude that the ordinal of ordinals is large.

There are also a number of uses of univalence via functional and propositional extensionality.

Propositional resizing rules or axioms are not needed, thanks to (2).

An ordinal in a universe $\mathcal{U}$ is a type $X : \mathcal{U}$ equipped with a relation $$ - \prec - : X \to X \to \mathcal{U}$$

required to be

1. proposition valued,

2. transitive,

3. extensional (any two points with same lower set are the same),

4. well founded (every element is accessible, or, equivalently, the principle of transfinite induction holds).

The HoTT book additionally requires $X$ to be a set, but this follows automatically from the above requirements for the order.

The underlying type of an ordinal $\alpha$ is denoted by $\langle \alpha \rangle$ and its order relation is denoted by $\prec_{\alpha}$ or simply $\prec$ when we believe the reader will be able to infer the missing subscript.

Equivalence of ordinals in universes $\mathcal{U}$ and $\mathcal{V}$, $$ -\simeq_o- : \operatorname{Ordinal}\,\mathcal{U} \to \operatorname{Ordinal}\,\mathcal{V} \to \mathcal{U} \sqcup \mathcal{V},$$ means that there is an equivalence of the underlying types that preserves and reflects order. Here we denote by $\mathcal{U} \sqcup \mathcal{V}$ the least upper bound of the two universes $\mathcal{U}$ and $\mathcal{V}$. The precise definition of the type theory we adopt here, including the handling of universes, can be found in Section 2 of this paper and also in our Midlands Graduate School 2019 lecture notes in Agda form.

For ordinals $\alpha$ and $\beta$ in the same universe, their identity type $\alpha = \beta$ is canonically equivalent to the ordinal-equivalence type $\alpha \simeq_o \beta$, by univalence.

The lower set of a point $x : \langle \alpha \rangle$ is written $\alpha \downarrow x$, and is itself an ordinal under the inherited order. The ordinals in a universe $\mathcal{U}$ form an ordinal in the successor universe $\mathcal{U}^+$, denoted by $$ \operatorname{OO}\,\mathcal{U} : \operatorname{Ordinal}\,\mathcal{U}^+,$$ for ordinal of ordinals.

Its underlying type is $\operatorname{Ordinal}\,\mathcal{U}$ and its order relation is denoted by $-\triangleleft-$ and is defined by $$\alpha \triangleleft \beta = \Sigma b : \langle \beta \rangle , \alpha = (\beta \downarrow b).$$

This order has type $$-\triangleleft- : \operatorname{Ordinal}\,\mathcal{U} \to \operatorname{Ordinal}\,\mathcal{U} \to \mathcal{U}^+,$$ as required for it to make the type $\operatorname{\operatorname{Ordinal}} \mathcal{U}$ into an ordinal in the next universe.

By univalence, this order is equivalent to the order defined by $$\alpha \triangleleft^- \beta = \Sigma b : \langle \beta \rangle , \alpha \simeq_o (\beta \downarrow b).$$ This has the more general type $$ -\triangleleft^-- : \operatorname{\operatorname{Ordinal}}\,\mathcal{U} \to \operatorname{\operatorname{Ordinal}}\,\mathcal{V} \to \mathcal{U} \sqcup \mathcal{V},$$ so that we can compare ordinals in different universes. But also when the universes $\mathcal{U}$ and $\mathcal{V}$ are the same, this order has values in $\mathcal{U}$ rather than $\mathcal{U}^+$. The existence of such a resized-down order is crucial for our corollaries of Burali-Forti, but not for Burali-Forti itself.

For any $\alpha : \operatorname{Ordinal}\,\mathcal{U}$ we have $$ \alpha \simeq_o (\operatorname{OO}\,\mathcal{U} \downarrow \alpha),$$ so that $\alpha$ is an initial segment of the ordinal of ordinals, and hence $$ \alpha \triangleleft^- \operatorname{OO}\,\mathcal{U}.$$

The Burali-Forti theorem in HoTT/UF

We adapt the original formulation and argument from set theory.

Theorem. No ordinal in a universe $\mathcal{U}$ can be equivalent to the ordinal of all ordinals in $\mathcal{U}$.

Proof. Suppose, for the sake of deriving absurdity, that there is an ordinal $\alpha \simeq_o \operatorname{OO}\,\mathcal{U}$ in the universe $\mathcal{U}$. By the above discussion, $\alpha \simeq_o \operatorname{OO}\,\mathcal{U} \downarrow \alpha$, and, hence, by symmetry and transitivity, $\operatorname{OO}\,\mathcal{U} \simeq_o \operatorname{OO}\,\mathcal{U} \downarrow \alpha$. Therefore, by univalence, $\operatorname{OO}\,\mathcal{U} = \operatorname{OO}\,\mathcal{U} \downarrow \alpha$. But this means that $\operatorname{OO}\,\mathcal{U} \triangleleft \operatorname{OO}\,\mathcal{U}$, which is impossible as any accessible relation is irreflexive. $\square$

Some corollaries follow.

The type of ordinals is large

We say that a type in the successor universe $\mathcal{U}^+$ is small if it is equivalent to some type in the universe $\mathcal{U}$, and large otherwise.

Theorem. The type of ordinals of any universe is large.

Proof. Suppose the type of ordinals in the universe $\mathcal{U}$ is small, so that there is a type $X : \mathcal{U}$ equivalent to the type $\operatorname{Ordinal}\, \mathcal{U} : \mathcal{U}^+$. We can then transport the ordinal structure from the type $\operatorname{Ordinal}\, \mathcal{U}$ to $X$ along this equivalence to get an ordinal in $\mathcal{U}$ equivalent to the ordinal of ordinals in $\mathcal{U}$, which is impossible by the Burali-Forti theorem.

But the proof is not concluded yet, because we have to say how we transport the ordinal structure. At first sight we should be able to simply apply univalence. However, this is not possible because the types $X : \mathcal{U}$ and $\operatorname{Ordinal}\,\mathcal{U} :\mathcal{U}^+$ live in different universes. The problem is that only elements of the same type can be compared for equality.

1. In the cumulative universe hierarchy of the HoTT book, we automatically have that $X : \mathcal{U}^+$ and hence, being equivalent to the type $\operatorname{Ordinal}\,\mathcal{U} : \mathcal{U}^+$, the type $X$ is equal to the type $\operatorname{Ordinal}\,\mathcal{U}$ by univalence. But this equality is an element of an identity type of the universe $\mathcal{U}^+$. Therefore when we transport the ordinal structure on the type $\operatorname{Ordinal}\,\mathcal{U}$ to the type $X$ along this equality and equip $X$ with it, we get an ordinal in the successor universe $\mathcal{U}^+$. But, in order to get the desired contradiction, we need to get an ordinal in $\mathcal{U}$.

2. In the non-cumulative universe hierarchy we adopt here, we face essentially the same difficulty. We cannot assert that $X : \mathcal{U}^+$ but we can promote $X$ to an equivalent type in the universe $\mathcal{U}^+$, and from this point on we reach the same obstacle as in the cumulative case.

So we have to transfer the ordinal structure from $\operatorname{Ordinal}\,\mathcal{U}$ to $X$ manually along the given equivalence, call it $$f : X \to \operatorname{Ordinal}\,\mathcal{U}.$$ We define the order of $X$ from that of $\operatorname{Ordinal}\,\mathcal{U}$ by $$ x \prec y = f(x) \triangleleft f(y). $$ It is laborious but not hard to see that this order satisfies the required axioms for making $X$ into an ordinal, except that it has values in $\mathcal{U}^+$ rather than $\mathcal{U}$. But this problem is solved by instead using the resized-down relation $\triangleleft^-$ discussed above, which is equivalent to $\triangleleft$ by univalence. $\square$

There are more types and sets in $\mathcal{U}^+$ than in $\mathcal{U}$

By a universe embedding we mean a map $$f : \mathcal{U} \to \mathcal{V}$$ of universes such that, for all $X : \mathcal{U}$, $$f(X) \simeq X.$$ Of course, any two universe embeddings of $\mathcal{U}$ into $\mathcal{V}$ are equal, by univalence, so that there is at most one universe embedding between any two universes. Moreover, universe embeddings are automatically type embeddings (meaning that they have propositional fibers).

So the following says that the universe $\mathcal{U}^+$ is strictly larger than the universe $\mathcal{U}$:

Theorem. The universe embedding $\mathcal{U} \to \mathcal{U}^+$ doesn't have a section and therefore is not an equivalence.

Proof. A section would give a type in the universe $\mathcal{U}$ equivalent to the type of ordinals in $\mathcal{U}$, but we have seen that there is no such type. $\square$

(However, by Theorem 29 of Injective types in univalent mathematics, if propositional resizing holds then the universe embedding $\mathcal{U} \to \mathcal{U}^+$ is a section.)

The same argument of the above theorem shows that there are more sets in $\mathcal{U}^+$ than in $\mathcal{U}$, because the type of ordinals is a set. For a universe $\mathcal{U}$ define the type $$\operatorname{hSet}\,\mathcal{U} : \mathcal{U}^+$$ by $$ \operatorname{hSet}\,\mathcal{U} = \Sigma A : \mathcal{U} , \text{$A$ is a set}.$$ By an hSet embedding we mean a map $$f : \operatorname{hSet}\,\mathcal{U} → \operatorname{hSet}\,\mathcal{V}$$ such that the underlying type of $f(\mathbb{X})$ is equivalent to the underlying type of $\mathbb{X}$ for every $\mathbb{X} : \operatorname{hSet}\,\mathcal{U}$, that is, $$ \operatorname{pr_1} (f (\mathbb{X})) ≃ \operatorname{pr_1}(\mathbb{X}). $$ Again there is at most one hSet-embedding between any two universes, hSet-embeddings are type embeddings, and we have:

Theorem. The hSet-embedding $\operatorname{hSet}\,\mathcal{U} \to \operatorname{hSet}\,\mathcal{U}^+$ doesn't have a section and therefore is not an equivalence.

There are more magmas and monoids in $\mathcal{U}^+$ than in $\mathcal{U}$

This is because the type of ordinals is a monoid under addition with the ordinal zero as its neutral element, and hence also a magma. If the inclusion of the type of magmas (respectively monoids) of one universe into that of the next were an equivalence, then we would have a small copy of the type of ordinals.

Theorem. The canonical embeddings $\operatorname{Magma}\,\mathcal{U} → \operatorname{Magma}\,\mathcal{U}^+$ and $\operatorname{Monoid}\,\mathcal{U} → \operatorname{Monoid}\,\mathcal{U}^+$ don't have sections and hence are not equivalences.

There are more groups in $\mathcal{U}^+$ than in $\mathcal{U}$

This case is more interesting.

The axiom of choice is equivalent to the statement that any non-empty set can be given the structure of a group. So if we assumed the axiom of choice we would be done. But we are brave and work without assuming excluded middle, and hence without choice, so that our results hold in any $\infty$-topos.

It is also the case that the type of propositions can be given the structure of a group if and only if the principle of excluded middle holds. And the type of propositions is a retract of the type of ordinals, which makes it unlikely that the type of ordinals can be given the structure of a group without excluded middle.

So our strategy is to embed the type of ordinals into a group, and the free group does the job.

1. First we need to show that the inclusion of generators, or the universal map into the free group, is an embedding.

2. But having a large type $X$ embedded into a type $Y$ is not enough to conclude that $Y$ is also large. For example, if $P$ is a proposition then the unique map $P \to \mathbb{1}$ is an embedding, and the unit type $\mathbb{1}$ is small but $P$ may be large.

3. So more work is needed to show that the group freely generated by the type of ordinals is large. We say that a map is small if each of its fibers is small, and large otherwise. De Jong and Escardo showed that if a map $X \to Y$ is small and the type $Y$ is small, then so is the type $X$, and hence if $X$ is large then so is $Y$. Therefore our approach is to show that the universal map into the free group is small. To do this, we exploit the fact that the type of ordinals is locally small (its identity types are all equivalent to small types).

But we want to be as general as possible, and hence work with a spartan univalent type theory which doesn't include higher inductive types other than propositional truncation. We include the empty type, the unit type, natural numbers, list types (which can actually be constructed from the other type formers), coproduct types, $\Sigma$-types, $\Pi$-types, identity types and a sequence of universes. We also assume the univalence axiom (from which we automatically get functional and propositional extensionality) and the axiom of existence of propositional truncations.

1. We construct the free group as a quotient of a type of words following Mines, Richman and Ruitenburg. To prove that the universal map is an embedding, one first proves a Church-Rosser property for the equivalence relation on words. It is remarkable that this can be done without assuming that the set of generators has decidable equality.

2. Quotients can be constructed from propositional truncation. This construction increases the universe level by one, but eliminates into any universe.

3. To resize back the quotient used to construct the group freely generated by the type of ordinals to the original universe, we exploit the fact that the type of ordinals is locally small.

4. As above, we have to transfer manually group structures between equivalent types of different universes, because univalence can't be applied.

Putting the above together, and leaving many steps to the Agda code, we get the following in our spartan univalent type theory.

Theorem. For any large, locally small set, the free group is also large and locally small.

Corollary. In any successor universe $\mathcal{U}^+$ there is a group which is not isomorphic to any group in the universe $\mathcal{U}$.

Corollary. The canonical embedding $\operatorname{Group}\,\mathcal{U} → \operatorname{Group}\,\mathcal{U}^+$ doesn't have a section and hence is not an equivalence.

Can we formulate and prove a general theorem of this kind that specializes to a wide variety of mathematical structures that occur in practice?

Tarides is very glad to announce our partnership with Ada Tech School.

Founded in 2019 and based in Paris (France), Ada Tech School, named for pioneer computer scientist Ada Lovelace, is a programming school designed for women but open to all. The program is driven by three values: feminism, empathy and singularity. Its mission is to facilitate access to programming positions and promote the feminization of tech, by creating training that tackles the gender and cultural biases of IT.

Unfortunate…

Tarides is very glad to announce our partnership with Ada Tech School.

Founded in 2019 and based in Paris (France), Ada Tech School, named for pioneer computer scientist Ada Lovelace, is a programming school designed for women but open to all. The program is driven by three values: feminism, empathy and singularity. Its mission is to facilitate access to programming positions and promote the feminization of tech, by creating training that tackles the gender and cultural biases of IT.

Unfortunately, the diversity of the candidate pool is very limited when a company tries to fill positions. Barely 10% of computer science students in France are girls. Ada Tech School is an excellent initiative to democratize software education amongst women. The school was created so that women can land a job easily in the IT industry through rigorous training, and then offer ongoing coaching and support to ascend the professional ladder within tech companies.

At Tarides, we believe that a healthy team is a diverse one; and that trust, fairness and inclusion are values needed to build a strong company.

We are committed to doing better, not only by hiring a diverse team and providing a welcoming work environment, but also by putting people first at every stage. This means providing fair and equitable compensation as well as meaningful career advancement opportunities for every employee.

We believe that a great technology always derives from great people, regardless of their background. Head here to see our currently-open positions.

We are pleased to announce the minor release of opam 2.0.8.

This new version contains some backported fixes:

• Critical for fish users! Don’t add . to PATH. [#4078]
• Fix sandbox script for newer ccache versions. [#4079 and #4087]
• Fix sandbox crash when ~/.cache is a symlink. [#4068]
• User modifications to the sandbox script are no longer overwritten by opam init. [#4020 & #4092]
• macOS sandbox script always mounts /tmp read-write, regardless of TMPDIR [#3742, addressing ocaml/opam-reposi…

We are pleased to announce the minor release of opam 2.0.8.

This new version contains some backported fixes:

• Critical for fish users! Don’t add . to PATH. [#4078]
• Fix sandbox script for newer ccache versions. [#4079 and #4087]
• Fix sandbox crash when ~/.cache is a symlink. [#4068]
• User modifications to the sandbox script are no longer overwritten by opam init. [#4020 & #4092]
• macOS sandbox script always mounts /tmp read-write, regardless of TMPDIR [#3742, addressing ocaml/opam-repository#13339]
• pre- and post-session hooks can now print to the console [#4359]
• Switch-specific pre/post sessions hooks are now actually run [#4472]
• Standalone opam-installer now correctly builds from sources [#4173]
• Fix arch variable detection when using 32bit mode on ARM64 and i486 [#4462]

A more complete release note is available.

Note: To homogenise macOS name on system detection, we decided to keep macos, and convert darwin to macos in opam. For the moment, in order to avoid breaking jobs & CIs, we keep uploading darwin & macos binaries, but from the 2.1.0 release, only macos ones will be kept.

Installation instructions (unchanged):

1. From binaries: run sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) or download manually from the Github “Releases” page to your PATH. In this case, don’t forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script.
2. From source, using opam: opam update; opam install opam-devel (then copy the opam binary to your PATH as explained, and don’t forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script)
3. From source, manually: see the instructions in the README.

We hope you enjoy this new minor version, and remain open to bug reports and suggestions.

NOTE: this article is cross-posted on opam.ocaml.org and ocamlpro.com, and published in discuss.ocaml.org. Please head to the latter for the comments!

About OCamlPro:

OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users’ Club). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: contact@ocamlpro.com.

We are pleased to announce the minor release of opam 2.0.8.

This new version contains some backported fixes:

• Critical for fish users! Don't add . to PATH. [#4078]
• Fix sandbox script for newer ccache versions. [#4079 and #4087]
• Fix sandbox crash when ~/.cache is a symlink. [#4068]
• User modifications to the sandbox script are no longer overwritten by opam init. [#4020 & #4092]
• macOS sandbox script always mounts /tmp read-write, regardless of TMPDIR [#3742, addressing ocaml/opam-repository#13339]

We are pleased to announce the minor release of opam 2.0.8.

This new version contains some backported fixes:

• Critical for fish users! Don't add . to PATH. [#4078]
• Fix sandbox script for newer ccache versions. [#4079 and #4087]
• Fix sandbox crash when ~/.cache is a symlink. [#4068]
• User modifications to the sandbox script are no longer overwritten by opam init. [#4020 & #4092]
• macOS sandbox script always mounts /tmp read-write, regardless of TMPDIR [#3742, addressing ocaml/opam-repository#13339]
• pre- and post-session hooks can now print to the console [#4359]
• Switch-specific pre/post sessions hooks are now actually run [#4472]
• Standalone opam-installer now correctly builds from sources [#4173]
• Fix arch variable detection when using 32bit mode on ARM64 and i486 [#4462]

A more complete release note is available.

Note: To homogenise macOS name on system detection, we decided to keep macos, and convert darwin to macos in opam. For the moment, in order to avoid breaking jobs & CIs, we keep uploading darwin & macos binaries, but from the 2.1.0 release, only macos ones will be kept.

1. From binaries: run

   sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)

   or download manually from the Github "Releases" page to your PATH. In this case, don't forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script.

2. From source, using opam:

   opam update; opam install opam-devel

   (then copy the opam binary to your PATH as explained, and don't forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script)

3. From source, manually: see the instructions in the README.

We hope you enjoy this new minor version, and remain open to bug reports and suggestions.

NOTE: this article is cross-posted on opam.ocaml.org and ocamlpro.com, and published in discuss.ocaml.org. Please head to the latter for the comments!