Tarides takes great pride in a diverse workforce and strives to continue bringing talented people to its team from around the globe. This is why Sonja Heinze, a Tarides software engineer, and the Head of HR, Héloïse Lutton, will attend WomenHack, an online event dedicated to recruiting more women into the tech world. They're participating not only to present Tarides to the Women In Tech community, but to also network and possibly find new talented programmers to join our growing team.

The Wome…

Tarides takes great pride in a diverse workforce and strives to continue bringing talented people to its team from around the globe. This is why Sonja Heinze, a Tarides software engineer, and the Head of HR, Héloïse Lutton, will attend WomenHack, an online event dedicated to recruiting more women into the tech world. They're participating not only to present Tarides to the Women In Tech community, but to also network and possibly find new talented programmers to join our growing team.

The WomenHack event has a unique setup similar to 'speed dating,' but for prospective jobs. Each candidate is paired with a company, and they have 5 minutes to chat before moving on to the next company. This "rapid interview" is both fun and efficient for all involved, and it ensures each company will meet several talented candidates from diverse backgrounds, which increases their chance of finding that perfect fit for an open position!

From their website:

WomenHack is a community that empowers women in tech through events, jobs, and reviews. We aim to create a more inclusive and diverse workplace for all. Our diversity recruiting events target some of the most talented women in tech which include software developers, designers, and product talent. 

Join us tomorrow, July 21st, at WomenHack! You can get your ticket here.

In some discussions among OCaml developers around the empty type (PR#9459), some people mused about the possibility of annotating functions with an attribute telling the compiler that the function should be trivial, and always return a value strictly equivalent to its argument.
Curious about the feasibility of implementing this feature, we advertised an internship with our compiler team aimed at exploring this subject.
We welcomed Léo Boitel during three months to work on this topic, with Vincen…

In some discussions among OCaml developers around the empty type (PR#9459), some people mused about the possibility of annotating functions with an attribute telling the compiler that the function should be trivial, and always return a value strictly equivalent to its argument.
Curious about the feasibility of implementing this feature, we advertised an internship with our compiler team aimed at exploring this subject.
We welcomed Léo Boitel during three months to work on this topic, with Vincent Laviron as mentor, and we’re proud to let him show off what he has achieved in this post.

The problem at hand

OCaml’s strong typing system is one of its main perks: it allows to write safe code thanks to the abstraction it provides. Most of the basic design mistakes will directly result into a typing error and the user cannot mess up the memory as it is automatically handled by the compiler and runtime.

However, these perks keep a power-user from implementing some optimizations, in particular those linked to memory representation as they cannot be accessed directly.

A good example would be this piece of code:

type return = Ok of int | Failure
let id = function
| Some x -> Ok x
| None -> Failure

In terms of memory representation, this function is indeed the identity function. Some x and Ok x share the same representation (and so do None and Failure). However, this identity is invisible to the user. Even if the user knows the representation is the same, they would need to use this function to avoid a typing error.

Another good example would be this one:

type record = { a:int; b:int }
let id (x,y) = { a = x; b = y }

Even if those functions are the identity, they come with a cost: not only do they cost a function call, they reallocate the result instead of just returning their argument directly. Detecting those functions would allow us to produce interesting optimizations.

Hurdles

If we want to detect identities, we quickly hit the problem of recursive functions: how does one recognize identity in those cases? Can a function be an identity if it doesn’t always terminate, or if it never does?

Once we have a good definition of what exactly an identity function is, we still need to prove that an existing function fits the definition. Indeed, we want to ensure the user that this optimization will not change the observable behavior of the program.

We also want to avoid breaking type safety. As an example, the following function:

let rec fake_id = function
| [] -> 0
| t::q -> fake_id (t::q)

A naive induction proof would allow us to replace this function with the identity, as [] and 0 share the same memory representation. However, this is unsafe as applying this to a non-empty list would return a list even if this function has an int type (we’ll talk more about it later).

To tackle those challenges, we started the internship with a theoretical study that lasted for three fourths of the allocated time and lastly implemented a practical solution in the Flambda representation of the compiler.

Theoretical results

We worked on extensions of lambda-calculus (implemented in OCaml) in order to gradually test our ideas in a simpler framework than the full Flambda.

Pairs

We started with a lambda-calculus to which we only added the concept of pairs. To prove identities, every function has to be annotated as identity or not. We then prove these annotations by β-reducing the function bodies. After each recursive reduction, we apply a rule that states that a pair made of the first and second projection of a variable is equal to that variable. We do not reduce applications, but we replace them by the argument if the concerned function is annotated as identity.

Using this method, we maintain a reasonable complexity compared to a full β-reduction which would be unrealistic on a big program.

We then add higher-order capabilities by allowing annotations of the form Annotation → Annotation. Functions as List.map can that way be abstracted as Id → Id. Even though this solution doesn’t cover every case, most real-world usage are recognized by these patterns.

Tuple reconstruction

We then move from just pairs to tuples of arbitrary size. This adds a new problem: if we make a pair out of the first two fields of a variable, this is no longer necessarily that variable, as it may have more than two fields.

We then have two solutions: we can first annotate every projection with the size of the involved tuple to know if we are indeed reconstructing the entire variable. As an example, if we make a pair from the fields of a triplet, we know there is no way to simplify this reconstruction.

Another solution, more ambitious, is to adopt a less restrictive definition of equality and to allow the replacement of (x,y) by (x,y,z). Indeed, if the variable was typed as a pair, we are guaranteed that the third field will never be accessed. The behavior of the program will therefore never be affected by this extension.

Though this allows to avoid a lot of allocations, it may also increase memory usage in some cases: if the triplet ceases to be used, it won’t be deallocated by the Garbage Collector (GC) and the field z will be kept in memory as long as (x,y) is still accessible.

This approach remains interesting to us, as long as it is manually enabled by the user for some specific blocks.

Recursion

We now add recursive definitions to our language, through the use of a fixpoint operator.

To prove that a recursive function is the identity, we have to use induction. The main difficulty is to prove that the function indeed terminates to ensure the validity of the induction.

We can separate this into three different levels of safety. The first option is to not prove termination at all, and let the user state which function they know will return. We can then assume the function is the identity and replace its body on that hypothesis. This approach is enough for most practical cases, but its main problem lies in the fact that it allows to write unsafe code (as we’ve already seen).

Our second option is to limit our induction hypothesis to recursive applications on “smaller” elements than the argument. An element is defined as smaller if it is a projection of the argument or a projection of a smaller element. This is not enough to prove that the function will terminate (the argument might be cyclic, for example) but is enough to ensure type safety. The reason is that any possibly returned value is constructed (as it cannot directly come from a recursive call) and have therefore a defined type. Typing would fail if the function was to return a value that cannot be identified to its argument.

Finally, we may want to establish a perfect equivalence between the function and the identity function before simplifying it. In that case, we propose to create a special annotation for functions that are the identity when applied to a non-cyclical object. We can prove they have this property with the already described induction. The difficulty now lies into applying the simplification only to valid applications: if an object is immutable, wasn’t recursively defined and is made of components that also have that property, we can declare that object inductive and simplify applications on it. The inductive state of variables can be propagated during our recursive pass of optimization.

Block reconstruction

The representation of blocks in Flambda provides interesting challenges in terms of equality detection, which is often crucial to prove an identity. It is very hard to detect an identical block reconstruction.

Blocks in Flambda

Variants

The blocks in Flambda come from the existence of variants in OCaml: one type may have several different constructors, as we can see in

type choice = A of int | B of int

When OCaml is compiled to Flambda, the information used by the constructor is lost and replaced by a tag. The tag is a number contained in the header of the object’s memory representation between 0 and 255 that represents which constructor was used. As an example, an element of type choice would have tag 0 for the A constructor, and 1 for B.

That tag will be kept at runtime, which will allow for example to implement pattern matching as a simple switch in Flambda, that executes simple comparisons on the tag to know which branch to execute next.

This system complicates our task as Flambda’s typing doesn’t inform us which type the constructor is supposed to have, and therefore keeps us from easily knowing if two variants are indeed equal.

Tag generalization

To complicate things, tags are actually used for any block, meaning tuples, modules or functions (as a matter of fact, almost anything but constant constructors and integers). If the object doesn’t have variants, it will usually have tag 0. This tag is never read (as there are no variants to differentiate) but keeps us from simply comparing two tuples, because Flambda will simply see two blocks of unknown tag.

Inlining

Finally, this system is optimized by inlining tuples: if a variant has a shape Pair of int * int, it will be often be flattened into a tuple (tag Pair, int, int).

This also means that variants can have an arbitrary size, which is also unknown in Flambda.

Existing approach

A partial solution to the problem already existed in a Pull Request (PR) you can read here.

The chosen approach in this PR is the natural one: we use the switch to gain information on the tag of a block, depending on the branch taken. The PR also allows to know the mutability and size of the block in each branch, starting from OCaml (where this information is known as it is explicit in the pattern matching) and propagating the knowledge to Flambda.

This allows to register every block on which a switch is done with their tag, size and mutability. We can then detect if one of them is reconstructed with the use of a Pmakeblock primitive.

Unfortunately, this path has its limits as there are numerous cases where the tag and size could be known without performing a switch on the value. As an example, this doesn’t allow the simplification of tuple reconstruction.

New solution

Our new solution will have to propagate more information from OCaml into Flambda. This propagation is based on two PRs that already existed for Flambda 2, which annotated in the lambda representation each projection (Pfield) with typing informations. We add block mutability and tag and finally size.

Our first contribution was to translate these PRs to Flambda 1, and to propagate from lambda to Flambda correctly.

We then had access to every necessary information to detect and prove block reconstruction: not only we have a list of blocks that were pattern-matched, we can make a list of partially immutable blocks, meaning blocks for which we know that some fields are immutable.

Here’s how we use it:

Block discovery

As soon as we find a projection, we verify whether it is done on an immutable block of known size. If so, we add that block to the list of partial blocks. We verify that the information we have on the tag and size are compatible with the already known projections. If all of the fields of the block are known, the block is added to the list of simplifiable blocks.

Of course, we also keep track of known blocks though switches.

Simplification

This part is similar to the original PR: when an immutable block is met, we check whether this block is known as simplifiable. In that case we avoid a reallocation.

Compared to the original approach, we also reduced the asymptotic complexity (from quadratic to linear) by registering the association of every projection variable to its index and original block. We also modified some implementation details that could have triggered a bug when associated with our PR.

Example

Let’s consider this function:

type typ1 = A of int | B of int * int
type typ2 = C of int | D of {x:int; y:int}
let id = function
  | A n -> C n
  | B (x,y) -> D {x; y}

The current compiler would produce the resulting Flambda output:

End of middle end:
let_symbol
  (camlTest__id_21
    (Set_of_closures (
      (set_of_closures id=Test.8
        (id/5 = fun param/7 ->
          (switch*(0,2) param/7
           case tag 0:
            (let
              (Pmakeblock_arg/11 (field 0<{../../test.ml:4,4-7}> param/7)
               Pmakeblock/12
                 (makeblock 0 (int)<{../../test.ml:4,11-14}>
                   Pmakeblock_arg/11))
              Pmakeblock/12)
           case tag 1:
            (let
              (Pmakeblock_arg/15 (field 1<{../../test.ml:5,4-11}> param/7)
               Pmakeblock_arg/16 (field 0<{../../test.ml:5,4-11}> param/7)
               Pmakeblock/17
                 (makeblock 1 (int,int)<{../../test.ml:5,17-23}>
                   Pmakeblock_arg/16 Pmakeblock_arg/15))
              Pmakeblock/17)))
         free_vars={ } specialised_args={}) direct_call_surrogates={ }
        set_of_closures_origin=Test.1])))
  (camlTest__id_5_closure (Project_closure (camlTest__id_21, id/5)))
  (camlTest (Block (tag 0,  camlTest__id_5_closure)))
End camlTest

Our optimization allows to detect that this function reconstructs a similar block and therefore can simplify it:

End of middle end:
let_symbol
  (camlTest__id_21
    (Set_of_closures (
      (set_of_closures id=Test.7
        (id/5 = fun param/7 ->
          (switch*(0,2) param/7
           case tag 0 (1): param/7
           case tag 1 (2): param/7))
         free_vars={ } specialised_args={}) direct_call_surrogates={ }
        set_of_closures_origin=Test.1])))
  (camlTest__id_5_closure (Project_closure (camlTest__id_21, id/5)))
  (camlTest (Block (tag 0,  camlTest__id_5_closure)))
End camlTest

Possible improvements

Equality relaxation

We can use observational equality studied in the theoretical part for block equality in order to avoid more allocations. The implementation is simple:

When a block is created, to know if it will be allocated, the normal course of action is to check if all of its fields are the known projections of another block, with the same index, and if the block sizes are the same. We can just remove that last check.

Implementing this was a bit more tricky because of several practical details. First, we want that optimization to be only triggered on user-annotated blocks, we had to propagate that annotation to Flambda.

Additionally, if we only implement that optimization, numerous optimization cases will be ignored because unused variables are simplified before our optimization pass. As an example, if a function looks like

let loose_id (a,b,c) = (a,b)

The c variable will be simplified away before reaching Flambda, and there will be no way to prove that (a,b,c) is immutable as its third field could not be. This problem is being solved on Flambda2 thanks to a PR that propagates mutability information for every block, but we didn’t have the time necessary to migrate it on Flambda 1.

Detecting recursive identities

Now that we can detect block reconstruction, we’re left with solving the problem of recursive functions.

Unsafe approach

We began the implementation of a pass that contains no termination proof. The idea is to add the proof later, or to authorize non-terminating functions to be simplified as long as they type correctly (see previously in the theory part).

For now, we trust the user to verify these properties manually.

Hence, we modified the function simplification procedure: when a function with a single argument is modified, we first assume that this function is the identity before simplifying its body. We then check whether the result is equivalent to an identity by recursively going through it, so as to cover as many cases as possible (for example in conditional branchings). If it is the case, the function will be replaced by the identity ; otherwise, we go back to a normal simplification, without the induction hypothesis.

Constant propagation

We took some time to improve our code that checks whether the body of a function is an identity or not, so as to handle constant values. It propagates identity information we have on an argument during conditional branching.

This way, on a function like

type truc = A | B | C
let id = function
  | A -> A
  | B -> B
  | C -> C

or even

let id x = if x=0 then 0 else x

We can successfully detect identity.

Examples

Recursive functions

We can now detect recursive identities:

let rec listid = function
  | t::q -> t::(listid q)
  | [] -> []

Used to compile to:

End of middle end:
let_rec_symbol
  (camlTest__listid_5_closure
    (Project_closure (camlTest__set_of_closures_20, listid/5)))
  (camlTest__set_of_closures_20
    (Set_of_closures (
      (set_of_closures id=Test.11
        (listid/5 = fun param/7 ->
          (if param/7 then begin
            (let
              (apply_arg/13 (field 1<{../../test.ml:9,4-8}> param/7)
               apply_funct/14 camlTest__listid_5_closure
               Pmakeblock_arg/15
                 *(apply*[listid/5]<{../../test.ml:9,15-25}> apply_funct/14
                    apply_arg/13)
               Pmakeblock_arg/16 (field 0<{../../test.ml:9,4-8}> param/7)
               Pmakeblock/17
                 (makeblock 0<{../../test.ml:9,12-25}> Pmakeblock_arg/16
                   Pmakeblock_arg/15))
              Pmakeblock/17)
            end else begin
            (let (const_ptr_zero/27 Const(0a)) const_ptr_zero/27) end))
         free_vars={ } specialised_args={}) direct_call_surrogates={ }
        set_of_closures_origin=Test.1])))
let_symbol (camlTest (Block (tag 0,  camlTest__listid_5_closure)))
End camlTest

But is now detected as being the identity:

End of middle end:
let_symbol
  (camlTest__set_of_closures_20
    (Set_of_closures (
      (set_of_closures id=Test.13 (listid/5 = fun param/7 -> param/7)
        free_vars={ } specialised_args={}) direct_call_surrogates={ }
        set_of_closures_origin=Test.1])))
  (camlTest__listid_5_closure
    (Project_closure (camlTest__set_of_closures_20, listid/5)))
  (camlTest (Block (tag 0,  camlTest__listid_5_closure)))
End camlTest

Unsafe example

However, we can use the unsafety of the feature to go around the typing system and access a memory address as if it was an integer:

type bugg = A of int*int | B of int
let rec bug = function
  | A (a,b) -> (a,b)
  | B x -> bug (B x)
  
let (a,b) = (bug (B 42))
let _ = print_int b

This function will be simplified to the identity even though the bugg type is not compatible with tuples; trying to project on the second field of variant b will access an undefined part of memory:

$ ./unsafe.out
47423997875612

Possible improvements – short term

Function annotation

A theoretically simple thing to add would be to let the choice of applying unsafe optimizations to the user. We lacked the time to do the work of propagating the information to Flambda, but it would not be hard to implement.

Order on arguments

For a safer optimization, we could use the idea developed in the theoretical part to make the optimization correct on non-cyclical objects and more importantly give us typing guarantees to avoid the problem we just saw.

To get this guarantee, we would have to change the simplification pass by adding an optional pair of function-argument to the environment. When this option exists, the pair indicates that we are in the body in the process of simplification and that applications on smaller elements can be simplified as identity. Of course, the pass would need to be modified to remember which elements are not smaller than the previous argument.

Possible improvements – long term

Exclusion of cyclical objects

As described in the theoretical part, we could recursively deduce which objects are cyclical and attempt to remove them from our optimization. The problem is then that instead of having to replace functions by the identity, we need to add a special annotation that represents IdRec.

This amounts to a lot of added implementation complexity when compiling over several files, as we need access to the interface of already compiled files to know when the optimization can be used.

A possibility would be to use .cmx files to store this information when the file is compiled, but that kind of work would have taken too long to be achieved during the internship. Moreover, the practicality of that choice is far from obvious: it would complexify the optimization pass for a small improvement with respect to a version that would be correct on non-cyclical objects and activated through annotations.

About OCamlPro:
OCamlPro is a company 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

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.