Sometimes software is written using whatever built-ins you find in your programming language of choice.
This is usually great!
However, it can happen that you depend on the precise semantics of those built-ins.
This can be a problem if those semantics become important to your software and you need to port it to another programming language.
@@ -49,18 +48,18 @@ In that case OCaml would escape the double quote with a backslash (\"
So a regular expression substitution was added to replace the escape sequence with just a double quote.
This pattern of finding small differences between Python and OCaml escaping had been repeated,
and eventually I decided to take a more rigorous approach to it.
-
What is a string?
+
What is a string?
First of all, what is a string? In Python? And in OCaml?
In OCaml a string is just a sequence of bytes.
Any bytes, even NUL bytes.
There is no concept of unicode in OCaml strings.
-In Python there is the str type which is a sequence of Unicode code points[1].
+In Python there is the str type which is a sequence of Unicode code points[^python-bytes].
I can recommend reading Daniel Bünzli's minimal introduction to Unicode.
Already here there is a significant gap in semantics between Python and OCaml.
For many practical purposes we can get away with using the OCaml string type and treating it as a UTF-8 encoded Unicode string.
This is what I will do as in both the Python code and the OCaml code the data being read is a UTF-8 (or often only the US ASCII subset) encoded string.
-
What does a string literal look like?
-
OCaml
+
What does a string literal look like?
+
OCaml
I will not dive too deep into the details of OCaml string literals, and focus mostly on how they are escaped by the language built-ins (String.escaped, Printf.printf "%S").
Normal printable ASCII is printed as-is.
That is, letters, numbers and other symbols except for backslash and double quote.
@@ -71,7 +70,7 @@ Finally I also want to mention the Unicode code point escape sequence \u{3
While the escape functions do not use it, it will become handy later on.
Illegal escape sequences (escape sequences that are not recognized) will emit a warning but otherwise result in the escape sequence as-is.
It is common to compile OCaml programs with warnings-as-errors, however.
-
Python
+
Python
Python has a number of different string literals and string-like literals.
They all use single quote or double quote to delimit the string (or string-like) literals.
There is a preference towards single quotes in str.__repr__().
@@ -82,7 +81,7 @@ The string literal can optionally have a prefix character that modifies what typ
That means backslash escape sequences are not interpreted.
In my experiments they seem to be quasi-interpreted, however!
The string r"\" is considered unterminated!
-But r"\"" is fine as is interpreted as '\\"'[2].
+But r"\"" is fine as is interpreted as '\\"'[^raw-escape-example].
Why this is the case I have not found a good explanation for.
The b-prefixed strings are bytes literals.
This is close to OCaml strings.
@@ -94,7 +93,7 @@ There is as far as I know no decimal notation.
The output of str.__repr__() uses the hexadecimal notation over the octal notation.
As Python strings are Unicode code point sequences we need more than two hexadecimal digits to be able to represent all valid "characters".
Thus there are the longer \u0032 and the longest \U00000032.
-
Intermezzo
+
Intermezzo
While studying Python string literals I discovered several odd corners of the syntax and semantics besides the raw string quasi-escape sequence mentioned earlier.
One fact is that Python doesn't have a separate character or Unicode code point type.
Instead, a character is a one element string.
@@ -118,7 +117,7 @@ Well, bytes is a byte sequence and b"\u0032" is not inter
Writing "\xff".encode() which encodes the string "\xff" to UTF-8 is not the same as b"\xff".
The bytes "\xff" consist of a single byte with decimal value 255,
and the Unicode wizards reading will know that the Unicode code point 255 (or U+FF) is encoded in two bytes in UTF-8.
-
Where is the Python code?
+
Where is the Python code?
Finding the implementation of str.__repr__() turned out to not be so easy.
In the end I asked on the Internet and got a link to cpython's Objects/unicodeobject.c.
And holy cow!
@@ -138,14 +137,14 @@ The first 32 characters and the last US ASCII character (DEL or \x7fpy library which provides bindings to Python from OCaml.
Great! This I can use to test my implementation against Python!
-
How about Unicode?
+
How about Unicode?
For the non-ascii characters (or code points rather) they are either considered printable or non-printable.
For now let's look at what that means for the output.
A printable character is copied as-is.
That is, there is no escaping done.
Non-printable characters must be escaped, and python wil use \xHH, \uHHHH or \UHHHHHHHH depending on how many hexadecimal digits are necessary to represent the code point.
That is, the latin-1 subset of ASCII (0x80-0xff) can be represented using \xHH and neither \u00HH nor \U000000HH will be used etc.
-
What is a printable Unicode character?
+
What is a printable Unicode character?
In the cpython function mentioned earlier they use the function Py_UNICODE_ISPRINTABLE.
I had a local clone of the cpython git repository where I ran git grep Py_UNICODE_ISPRINTABLE to find information about it.
In unicode.rst I found a documentation string for the function that describes it to return false if the character is nonprintable with the definition of nonprintable as the code point being in the categories "Other" or "Separator" in the Unicode character database with the exception of ASCII space (U+20 or ).
@@ -234,7 +233,7 @@ Not only is the code that instigated this journey highly dependent on Python-spe
Great! I modify the test suite to first detect the unicode version python uses and then pass that version to the OCaml function.
Now I can't find anymore failing test cases!
-
Epilogue
+
Epilogue
What can we learn from this?
It is easy to say in hindsight that a different representation should have been chosen.
However, arriving at this insight takes time.
@@ -248,7 +247,7 @@ Below is the output of help(str.__repr__):
Language and (standard) library designers could consider whether the slightly nicer looking strings are worth the added complexity users eventually are going to rely on - inadvertently or not.
I do think strings and bytes in Python are a bit too complex.
-It is not easy to get a language lawyer[3] level understanding.
+It is not easy to get a language lawyer[^language-lawyer] level understanding.
In my opinion it is a mistake to not at least print a warning if there are illegal escape sequences - especially considering there are escape sequences that are valid in one string literal but not another.
Unfortunately it is often the case that to get a precise specification it is necessary to look at the implementation.
For testing your implementation hand-written tests are good.
@@ -262,15 +261,10 @@ It may be the last time I need to understand Python's str.__repr__()
If you have a project in OCaml or want to port something to OCaml and would like help from me and my colleagues at Robur please get in touch with us and we will figure something out.
-
-
-
There is as well the bytes type which is a byte sequence like OCaml's string.
+
[^python-bytes]: There is as well the bytes type which is a byte sequence like OCaml's string.
The Python code in question is using str however.
At Robur we have been busy at work implementing our OpenVPN™-compatible MirageVPN software.
Recently we have implemented the server side.
In order to implement this side of the protocol I studied parts of the OpenVPN™ source code and performed experiments to understand what the implementation does at the protocol level.
Studying the OpenVPN™ implementation has lead me to discover two security issues: CVE-2024-28882 and CVE-2024-5594.
In this article I will talk about the relevant parts of the protocol, and describe the security issues in detail.
A VPN establishes a secure tunnel in which (usually) IP packets are sent.
-The OpenVPN protocol establishes a TLS tunnel[1] with which key material and configuration options are negotiated.
+The OpenVPN protocol establishes a TLS tunnel[^openvpn-tls] with which key material and configuration options are negotiated.
Once established the TLS tunnel is used to exchange so-called control channel messages.
They are NUL-terminated (well, more on that later) text messages sent in a single TLS record frame (mostly, more on that later).
I will describe two (groups) of control channel messages (and a bonus control channel message):
@@ -41,7 +40,7 @@ They are NUL-terminated (well, more on that later) text messages sent in a singl
(AUTH_FAILED)
The EXIT, RESTART, and HALT messages share similarity.
-They are all three used to signal to the client that it should disconnect[2] from the server.
+They are all three used to signal to the client that it should disconnect[^disconnect] from the server.
HALT tells the client to disconnect and suggests the client should terminate.
RESTART also tells the client to disconnect and suggests the client can reconnect either to the same server or the next server if multiple are configured depending on flags in the message.
EXIT tells the peer that it is exiting and the peer should disconnect.
@@ -50,13 +49,13 @@ It informs the peer that the sender is exiting and will (soon) not be receiving
Because the underlying transport can either be TCP or UDP the sender may have no guarantees that the message arrives.
OpenVPN's control channel implements a reliable layer with ACKs and retransmissions to work around that.
To accomodate this OpenVPN™ will wait five seconds before disconnecting to allow for retransmission of the exit message.
-
The bug
+
The bug
While I was working on implementing more control channel message types I modified a client application that connects to a server and sends pings over the tunnel - instead of ICMPv4 echo requests I modified it to send the EXIT control channel message once a second.
In the server logs I saw that the server successfully received the EXIT message!
But nothing else happened.
The server just kept receiving EXIT messages but for some reason it never disconnected the client.
Curious about this behavior I dived into the OpenVPN™ source code and found that on each EXIT message it (re)schedules an exit (disconnect) timer! That is, every time the server receives an EXIT message it'll go "OK! I'll shut down this connection in five seconds" forgetting it promised to do so earlier, too.
-
Implications
+
Implications
At first this seemed like a relatively benign bug.
What's the worst that could happen if a client says "let's stop in five second! No, five seconds from now! No, five seconds from now!" etc?
Well, it turns out the same timer is used when the server sends an exit message.
@@ -68,7 +67,7 @@ The management interface is a text protocol to communicate with the OpenVPN serv
One command is the client-kill command.
The documentation says to use this command to "[i]mmediately kill a client instance[...]".
In practice it sends an exit message to the client (either a custom one or the default RESTART).
-I learnt that it shares code paths with the exit control messages to schedule an exit (disconnect)[3].
+I learnt that it shares code paths with the exit control messages to schedule an exit (disconnect)[^kill-immediately].
That is, client-kill schedules the same five second timer.
Thus a malicious client can, instead of exiting on receiving an exit or RESTART message, send back repeatedly EXIT to the server to reset the five second timer.
This way the client can indefinitely delay the exit/disconnect assuming sufficiently stable and responsive network.
@@ -82,12 +81,12 @@ I don't know.
If you do or are aware of software that enforces policies this way please do reach out to me.
It would be interesting to hear and discuss.
The OpenVPN security@ mailing list took it seriously enough to assign it CVE-2024-28882.
-
OpenVPN configuration language
+
OpenVPN configuration language
Next up we have PUSH_REQUEST / PUSH_REPLY.
As the names suggest it's a request/response protocol.
It is used to communicate configuration options from the server to the client.
These options include routes, ip address configuration, negotiated cryptographic algorithms.
-The client signals it would like to receive configuration options from the server by sending the PUSH_REQUEST control channel message[4].
+The client signals it would like to receive configuration options from the server by sending the PUSH_REQUEST control channel message[^proto-push-request].
The server then sends a PUSH_REPLY message.
The format of a PUSH_REPLY message is PUSH_REPLY, followed by a comma separated list of OpenVPN configuration directives terminated by a NUL byte as in other control channel messages.
Note that this means pushed configuration directives cannot contain commas.
@@ -95,8 +94,8 @@ Note that this means pushed configuration directives cannot contain commas.
I learned some quirks of the configuration language which I find surprising and somewhat hard to implement.
I will not cover all corners of the configuration language.
In some sense you could say the configuration language of OpenVPN™ is line based.
-At least, the first step to parsing configuration directives as OpenVPN 2.X does is to read one line at a time and parse it as one configuration directive[5].
-A line is whatever fgets() says it is - this includes the newline if not at the end of the file[6].
+At least, the first step to parsing configuration directives as OpenVPN 2.X does is to read one line at a time and parse it as one configuration directive[^inline-files].
+A line is whatever fgets() says it is - this includes the newline if not at the end of the file[^configuration-newlines].
This is how it is for configuration files.
However, if it is a PUSH_REPLY a "line" is the text string up to a comma or the end of file (or, importantly, a NUL byte).
This "line" tokenization is done by repeatedly calling OpenVPN™'s buf_parse(buf, ',', line, sizeof(line)) function.
@@ -196,14 +195,14 @@ As a proof of concept I sent a PUSH_REPLY with an embedded BEL char
The ^G is how the BEL character is printed in my terminal.
I was also able to hear an audible bell.
A more thorough explanation on how terminal escape sequences can be exploited can be found on G-Reasearch's blog.
-
The fix
+
The fix
The fix also is also a first step towards decoupling the control channel messaging from the TLS record frames.
First, the data is split on NUL bytes in order to get the control channel message(s), and then messages are rejected if they contain illegal characters.
This solves the vulnerability described previously.
Unfortunately, it turns out that especially for the AUTH_FAILED control channel message it is easy to create invalid messages:
If 2FA is implemented using the script mechanism sending custom messages they easily end with a newline asking the client to enter the verification code.
I believe in 2.6.12 the client tolerates trailing newline characters.
-
Conclusion
+
Conclusion
The first bug, the timer rescheduling bug, is at least 20 years old!
It hasn't always been exploitable, but the bug itself goes back as far as the git history does.
I haven't attempted further software archeology to find the exact time of introduction.
@@ -211,20 +210,12 @@ Either way, it's old and gone unnoticed for quite a while.
I think this shows that diversity in implementations is a great way to exercise corner cases, push forward (protocol) documentation efforts and get thorough code review by motivated peers.
This work was funded by the EU NGI Assure Fund through NLnet.
In my opinion, this shows that funding one open source project can have a positive impact on other open source projects, too.
-
-
-
This is not always the case. It is possible to use static shared secret keys, but it is mostly considered deprecated.
As the alert reader might have realized this is inaccurate. It does not kill the client "immediately" as it will wait five seconds after the exit message is sent before exiting. At best this will kill a cooperating client once it's received the kill message.
There is another mechanism to request a PUSH_REPLY earlier with less roundtrips, but let's ignore that for now. The exact message is PUSH_REQUEST<NUL-BYTE> as messages need to be NUL-terminated.
An exception being inline files which can span multiple lines. They vaguely resemble XML tags with an open <tag> and close </tag> each on their own line with the data in between. I doubt these are sent in PUSH_REPLYs, but I can't rule out without diving into the source code that it isn't possible to send inline files.
This results in the quirk that it is possible to sort-of escape a newline in a configuration directive. But since the line splitting is done first it's not possible to continue the directive on the next line! I believe this is mostly useless, but it is a way to inject line feeds in configuration options without modifying the OpenVPN source code.
[^openvpn-tls]: This is not always the case. It is possible to use static shared secret keys, but it is mostly considered deprecated.
+[^disconnect]: I say "disconnect" even when the underlying transport is the connection-less UDP.
+[^kill-immediately]: As the alert reader might have realized this is inaccurate. It does not kill the client "immediately" as it will wait five seconds after the exit message is sent before exiting. At best this will kill a cooperating client once it's received the kill message.
+[^proto-push-request]: There is another mechanism to request a PUSH_REPLY earlier with less roundtrips, but let's ignore that for now. The exact message is PUSH_REQUEST<NUL-BYTE> as messages need to be NUL-terminated.
+[^inline-files]: An exception being inline files which can span multiple lines. They vaguely resemble XML tags with an open <tag> and close </tag> each on their own line with the data in between. I doubt these are sent in PUSH_REPLYs, but I can't rule out without diving into the source code that it isn't possible to send inline files.
+[^configuration-newlines]: This results in the quirk that it is possible to sort-of escape a newline in a configuration directive. But since the line splitting is done first it's not possible to continue the directive on the next line! I believe this is mostly useless, but it is a way to inject line feeds in configuration options without modifying the OpenVPN source code.
diff --git a/articles/gptar.html b/articles/gptar.html
index 3e636af..22d046c 100644
--- a/articles/gptar.html
+++ b/articles/gptar.html
@@ -1,4 +1,3 @@
-
@@ -6,13 +5,13 @@
- Robur's blog - GPTar
+ Robur's blogGPTar
-
-
-
-
+
+
+
+
@@ -21,17 +20,17 @@
The Robur cooperative blog.
- Back to index
+ Back to index
At Robur we developed a piece of software for mirroring or exposing an opam repository.
We have it deployed at opam.robur.coop, and you can use it as an alternative to opam.ocaml.org.
It is usually more up-to-date with the git opam-repository than opam.ocaml.org although in the past it suffered from occasional availability issues.
I can recommend reading Hannes' post about opam-mirror.
This article is about adding a partition table to the disk as used by opam-mirror.
For background I can recommend reading the previously linked subsection of the opam-mirror article.
-
The opam-mirror persistent storage scheme
+
The opam-mirror persistent storage scheme
Opam-mirror uses a single block device for its persistent storage.
On the block device it stores cached source code archives from the opam repository.
These are stored in a tar archive consisting of files whose file name is the sha256 checksum of the file contents.
@@ -49,7 +48,7 @@ Therefore I have for a long time been wanting to use an on-disk partition table.
The problem is both MBR and GPT (GUID Partition Table) store the table at the beginning of the disk.
If we write a partition table at the beginning it is suddenly not a valid tar archive anymore.
Of course, in Mirage we can just write and read the table at the end if we please, but then we lose the ability to inspect the partition table in the host system.
-
GPT header as tar file name
+
GPT header as tar file name
My first approach, which turned out to be a dead end, was when I realized that a GPT header consists of 92 bytes at the beginning followed by reserved space for the remainder of the LBA.
The reserved space should be all zeroes, but it seems no one bothers to enforce this.
What's more is that a tar header starts with the file name in the first 100 bytes.
@@ -71,7 +70,7 @@ The changes made are viewable on bug in ocaml-tar.
GNU tar was successfully able to list the archive.
A quirk is that the archive will start with a dummy file GPTAR which consists of any remaining space in the first LBA if the sector size is greater than 512 bytes followed by the partition table.
-
Protective MBR
+
Protective MBR
Unfortunately, neither fdisk nor parted recognized the GPT partition table.
I was able to successfully read the partition table using ocaml-gpt however.
This puzzled me.
@@ -79,7 +78,7 @@ Then I got a hunch: I had read about [1].
+The V7 format is differentiated by the UStar, POSIX/pax and old GNU tar formats by not having the string ustar at byte offset 257[^tar-ustar].
The master boot record format starts with the bootstrap code area.
In the classic format it is the first 446 bytes.
In the modern standard MBR format the first 446 bytes are mostly bootstrap code too with the exception of a handful bytes at offset 218 or so which are used for a timestamp or so.
@@ -113,7 +112,7 @@ Number Start End Size File system Name Flags
-r-------- 0/0 14 1970-01-01 01:00 test.txt
One thing that bothers me a bit is the dummy file GPTAR.
By using the G link indicator GNU tar will print a warning about the unknown file type G,
but it will still extract the dummy file when extracting the archive.
@@ -132,10 +131,7 @@ If the sector size is greater than 512 we can use the remaining space in LBA 0 t
I may try this for a sector size of 4096, but I'm not happy that it doesn't work with sector size 512 which solo5 will default to.
If you have other ideas what I can do please reach out!
-
-
-
This is somewhat simplified. There are some more nuances between the different formats, but for this purpose they don't matter much.
Here's a concrete example of the notion of availability and the scheduler used
(in this case Lwt). As you may know, at Robur we have developed a unikernel:
opam-mirror. It launches an HTTP service that can be used as an
OPAM overlay available from a Git repository (with opam repository add <name> <url>).
@@ -47,7 +46,7 @@ can be interesting to have such a unikernel available).
about it at the Mirleft retreat, when we tried to get the repository from Git,
we had a (fairly long) unavailability of our HTTP server. Basically, we had to
wait ~10 min before the service offered by the unikernel was available.
-
Availability
+
Availability
If you follow my articles, as far as Miou is concerned, from
the outset I talk of the notion of availability if we were to make yet another
new scheduler for OCaml 5. We emphasised this notion because we had quite a few
@@ -71,7 +70,7 @@ occurred. Lwt always tries to go as far down your chain as possible:
Lwt is rather sparse in adding cooperation points besides Lwt.pause and
read/write operations, in contrast with Async where the bind operator is a
cooperation point.
-
If there is no I/O, do not wrap in Lwt
+
If there is no I/O, do not wrap in Lwt
It was (bad1) advice I was given. If a function doesn't do
I/O, there's no point in putting it in Lwt. At first glance, however, the idea
may be a good one. If you have a function that doesn't do I/O, whether it's in
@@ -135,7 +134,7 @@ sort1: [|0; 6|]
1: However, if you are not interested in availability
and would like the scheduler to try to resolve your promises as quickly as
possible, this advice is clearly valid.
-
Performances
+
Performances
It should be noted, however, that Lwt has an impact. Even if the behaviour is
the same, the Lwt layer is not free. A quick benchmark shows that there is an
overhead:
@@ -162,7 +161,7 @@ sort1 0.000676s
This is the fairly obvious argument for not using Lwt when there's no I/O. Then,
if the Lwt monad is really needed, a simple Lwt.return at the very last
instance is sufficient (or, better, the use of Lwt.map / >|=).
-
Cooperation and concrete example
+
Cooperation and concrete example
So Lwt.both is the one to use when we want to run two processes
"at the same time". For the example, ocaml-git attempts both to
retrieve a repository and also to analyse it. This can be seen in this snippet
@@ -172,7 +171,7 @@ case, both the left and right side do I/O (the left side binds into a socket
while the right side saves Git objects in your file system). So, in our tests
with Git_unix, we were able to see that the analysis (right-hand side) was
well executed and 'interleaved' with the reception of objects from the network.
-
Composability
+
Composability
However, if we go back to our initial problem, we were talking about our
opam-mirror unikernel. As you might expect, there is no standalone MirageOS file
system (and many of our unikernels don't need one). So, in the case of
@@ -208,7 +207,7 @@ will always offer a certain availability to other services (such as an HTTP
service) while the other will offer a Lwt function which will try to go as far
as possible quite to make other services unavailable.
Composing with one or the other therefore does not produce the same behavior.
-
Where to put Lwt.pause?
+
Where to put Lwt.pause?
In this case, our analyse_pack does read/write on the Git store. As far as
Git_mem is concerned, we said that these read/write accesses were just
accesses to a Hashtbl.
@@ -225,7 +224,7 @@ to put, by hand, Lwt.pause.
In the end, Lwt has no mechanisms for ensuring the availability of a service
(this is something that must be taken into account by the implementer).
-
In-depth knowledge of Lwt
+
In-depth knowledge of Lwt
I haven't mentioned another problem we encountered with Armael when
implementing multipart_form where the use of stream meant that
Lwt didn't interleave the two processes and the use of a bounded stream was
@@ -234,7 +233,7 @@ possible in one of two branches of a Lwt.both.
This allows us to conclude that beyond the monad, Lwt has subtleties in its
behaviour which may be different from another scheduler such as Async (hence the
incompatibility between the two, which is not just of the 'a t type).
-
Digression on Miou
+
Digression on Miou
That's why we put so much emphasis on the notion of availability when it comes
to Miou: to avoid repeating the mistakes of the past. The choices that can be
made with regard to this notion in particular have a major impact, and can be
@@ -245,7 +244,7 @@ through the use of Effect.Shallow which requires us to always re-at
handler (our scheduler) as soon as an effect is produced, unlike Effect.Deep
which can re-use the same handler for several effects. In other words, and as
we've described here, an effect yields!
-
Conclusion
+
Conclusion
As far as opam-mirror is concerned, we now have an unikernel that is available
even if it attempts to clone a Git repository and save Git objects in memory. At
least, an HTTP service can co-exist with ocaml-git!
diff --git a/articles/miragevpn-ncp.html b/articles/miragevpn-ncp.html
index eaf440a..34a6770 100644
--- a/articles/miragevpn-ncp.html
+++ b/articles/miragevpn-ncp.html
@@ -1,4 +1,3 @@
-
@@ -6,13 +5,13 @@
- Robur's blog - MirageVPN updated (AEAD, NCP)
+ Robur's blogMirageVPN updated (AEAD, NCP)
-
-
-
-
+
+
+
+
@@ -21,13 +20,13 @@
The Robur cooperative blog.
- Back to index
+ Back to index
As announced earlier this month, we've been working hard over the last months on MirageVPN (initially developed in 2019, targeting OpenVPN™ 2.4.7, now 2.6.6). We managed to receive funding from NGI Assure call (via NLnet). We've made over 250 commits with more than 10k lines added, and 18k lines removed. We closed nearly all old issues, and opened 100 fresh ones, of which we already closed more than half of them. :D
-
Actual bugs fixed (that were leading to non-working MirageVPN applications)
+
Actual bugs fixed (that were leading to non-working MirageVPN applications)
In more detail, we had a specific configuration running over all the years, namely UDP mode with static keys (no TLS handshake, etc.). There were several issues (bitrot) that we encountered and solved along the path, amongst others:
To avoid any future breakage while revising the code (cleaning it up, extending it), we are now building several unikernels as part of our CI system. We also have setup OpenVPN™ servers with various configurations that we periodically test with our new code (we'll also work on further automation thereof).
-
New features: AEAD ciphers, supporting more configuration primitives
+
New features: AEAD ciphers, supporting more configuration primitives
We added various configuration primitives, amongst them configuratble tls ciphersuites, minimal and maximal tls version to use, tls-crypt-v2, verify-x509-name, cipher, remote-random, ...
From a cryptographic point of view, we are now supporting more authentication hashes via the configuration directive auth, namely the SHA2 family - previously, only SHA1 was supported, AEAD ciphers (AES-128-GCM, AES-256-GCM, CHACHA20-POLY1305) - previously only AES-256-CBC was supported.
-
NCP - Negotiation of cryptographic parameters
+
NCP - Negotiation of cryptographic parameters
OpenVPN™ has a way to negotiate cryptographic parameters, instead of hardcoding them in the configuration. The client can propose its supported ciphers, and other features (MTU, directly request a push message for IP configuration, use TLS exporter secret instead of the hand-crafted (TLS 1.0 based PRF), ...) once the TLS handshake has been completed.
We are now supporting this negotiation protocol, and have been working on the different extensions that are useful to us. Namely, transmitting the supported ciphers, request push (which deletes an entire round-trip), TLS-exporter. This will also be part of the protocol specification that we're working on while finishing our implementation.
-
Cleanups and refactorings
+
Cleanups and refactorings
We also took some time to cleanup our code base, removing Lwt.fail (which doesn't produce proper backtraces), using lzo from the decompress package (since that code has been upstreamed a while ago), remove unneeded dependencies (rresult, astring), avoiding assert false in pattern matches by improving types, improve the log output (include a timestamp, show log source, use colors).
-
Future
+
Future
There is still some work that we want to do, namely a QubesOS client implementation, an operators manual, extending our specification, resurrecting and adapting the server implementation, supporting more NCP features (if appropriate), etc. So stay tuned, we'll also provide reproducible binaries once we're ready.
Don't hesitate to reach out to us on GitHub, by mail or me personally on Mastodon if you're stuck.
diff --git a/articles/miragevpn-performance.html b/articles/miragevpn-performance.html
index ca43706..fba0826 100644
--- a/articles/miragevpn-performance.html
+++ b/articles/miragevpn-performance.html
@@ -1,4 +1,3 @@
-
@@ -6,13 +5,13 @@
- Robur's blog - Speeding up MirageVPN and use it in the wild
+ Robur's blogSpeeding up MirageVPN and use it in the wild
-
-
-
-
+
+
+
+
@@ -21,33 +20,30 @@
The Robur cooperative blog.
- Back to index
+ Back to index
As we were busy continuing to work on MirageVPN, we got in touch with eduVPN, who are interested about deploying MirageVPN. We got example configuration from their side, and fixedsomeissues, and also implemented tls-crypt - which was straightforward since we earlier spend time to implement tls-crypt-v2.
As we were busy continuing to work on MirageVPN, we got in touch with eduVPN, who are interested about deploying MirageVPN. We got example configuration from their side, and fixedsomeissues, and also implemented tls-crypt - which was straightforward since we earlier spend time to implement tls-crypt-v2.
In January, they gave MirageVPN another try, and measured the performance -- which was very poor -- MirageVPN (run as a Unix binary) provided a bandwith of 9.3Mb/s, while OpenVPN provided a bandwidth of 360Mb/s (using a VPN tunnel over TCP).
We aim at spending less resources for computing, thus the result was not satisfying for us. We re-read a lot of code, refactored a lot, and are now at ~250Mb/s.
-
Tooling for performance engineering of OCaml
+
Tooling for performance engineering of OCaml
As a first approach we connected with the MirageVPN unix client & OpenVPN client to a eduVPN server and ran speed tests using fast.com. This was sufficient to show the initial huge gap in download speeds between MirageVPN and OpenVPN. There is a lot of noise in this approach as there are many computers and routers involved in this setup, and it is hard to reproduce.
To get more reproducible results we set up a local VM with openvpn and iperf3 installed. On the host machine we can then connect to the VM's OpenVPN server and run iperf3 against the VPN ip address. This worked more reliably. However, it was still noisy and not suitable to measure single digit percentage changes in performance.
To better guide the performance engineering, we also developed a microbenchmark using OCaml tooling. This will setup a client and server without any input and output, and transfer data in memory.
We also re-read our code and used the Linux utility perf together with Flamegraph to graph its output. This works nicely with OCaml programs (we're using the 4.14.1 compiler and runtime system). We did the performance engineering on Unix binaries, i.e. not on MirageOS unikernels - but the MirageVPN protocol is used in both scenarios - thus the performance improvements described here are also in the MirageVPN unikernels.
-
Takeaway of performance engineering
+
Takeaway of performance engineering
The learnings of our performance engineering are in three areas:
-
Formatting strings is computational expensive -- thus if in an error case a hexdump is produced of a packet, its construction must be delayed for when the error case is executed (we have this PR and that PR). Alain Frisch wrote a nice blog post at LexiFi about performance of Printf and Format[1].
+
Formatting strings is computational expensive -- thus if in an error case a hexdump is produced of a packet, its construction must be delayed for when the error case is executed (we have this PR and that PR). Alain Frisch wrote a nice blog post at LexiFi about performance of Printf and Format[^lexifi-date].
Rethink allocations: fundamentally, only a single big buffer (to be send out) for each incoming packet should be allocated, not a series of buffers that are concatenated (see this PR and that PR). Additionally, not zeroing out the just allocated buffer (if it is filled with data anyways) removes some further instructions (see this PR). And we figured that appending to an empty buffer nevertheless allocated and copied in OCaml, so we worked on this PR.
Still an open topic is: we are in the memory-safe language OCaml, and we sometimes extract data out of a buffer (or set data in a buffer). Now, each operation lead to bounds checks (that we do not touch memory that is not allocated or not ours). However, if we just checked for the buffer being long enough (either by checking the length, or by allocating a specific amount of data), these bounds checks are superfluous. So far, we don't have an automated solution for this issue, but we are discussing it in the OCaml community, and are eager to find a solution to avoid unneeded computations.
-
Conclusion
+
Conclusion
To conclude: we already achieved a factor of 25 in performance by adapting the code in various ways. We have ideas to improve the performance even more in the future - we also work on using OCaml string and bytes, instead of off-the-OCaml-heap-allocated bigarrays (see our previous article, which provided some speedups).
Don't hesitate to reach out to us on GitHub, or by mail if you're stuck.
We want to thank NLnet for their funding (via NGI assure), and eduVPN for their interest.
-
-
-
It has come to our attention that the blog post is rather old (2012) and that the implementation has been completely rewritten since then.
[^lexifi-date]: It has come to our attention that the blog post is rather old (2012) and that the implementation has been completely rewritten since then.
diff --git a/articles/miragevpn-server.html b/articles/miragevpn-server.html
index 0657cd0..2e1250a 100644
--- a/articles/miragevpn-server.html
+++ b/articles/miragevpn-server.html
@@ -1,4 +1,3 @@
-
@@ -6,13 +5,13 @@
- Robur's blog - MirageVPN server
+ Robur's blogMirageVPN server
-
-
-
-
+
+
+
+
@@ -21,13 +20,13 @@
The Robur cooperative blog.
- Back to index
+ Back to index
It is a great pleasure to finally announce that we have finished a server implementation for MirageVPN (OpenVPN™-compatible). This allows to setup a very robust VPN network on both the client and the server side.
It is a great pleasure to finally announce that we have finished a server implementation for MirageVPN (OpenVPN™-compatible). This allows to setup a very robust VPN network on both the client and the server side.
As announced last year, MirageVPN is a reimplemtation of OpenVPN™ in OCaml, with MirageOS unikernels.
-
Why a MirageVPN server?
+
Why a MirageVPN server?
Providing Internet services with programming languages that have not much safety requires a lot of discipline by the developers to avoid issues which may lead to exploitable services that are attacked (and thus will circumvent any security goals). Especially services that are critical for security and privacy, it is crucial to avoid common memory safety pitfalls.
Some years back, when we worked on the client implementation, we also drafted a server implementation. The reasoning was that a lot of the code was already there, and just a few things needed to be developed to allow clients to connect there.
Now, we spend several months to push our server implementation into a state where it is usable and we are happy for everyone who wants to test it. We also adapted the modern ciphers we recently implemented for the client, and also tls-crypt and tls-crypt-v2 for the server implementation.
diff --git a/articles/miragevpn.html b/articles/miragevpn.html
index 4a42cf9..8ee224a 100644
--- a/articles/miragevpn.html
+++ b/articles/miragevpn.html
@@ -1,4 +1,3 @@
-
@@ -6,13 +5,13 @@
- Robur's blog - MirageVPN & tls-crypt-v2
+ Robur's blogMirageVPN & tls-crypt-v2
-
-
-
-
+
+
+
+
@@ -21,15 +20,15 @@
The Robur cooperative blog.
- Back to index
+ Back to index
In 2019 Robur started working on a OpenVPN™-compatible implementation in OCaml.
The project was funded for 6 months in 2019 by prototypefund.
In late 2022 we applied again for funding this time to the NGI Assure open call, and our application was eventually accepted.
In this blog post I will explain why reimplementing the OpenVPN™ protocol in OCaml is a worthwhile effort, and describe the Miragevpn implementation and in particular the tls-crypt-v2 mechanism.
-
What even is OpenVPN™?
+
What even is OpenVPN™?
OpenVPN™ is a protocol and software implementation to provide virtual private networks: computer networks that do not exist in hardware and are encrypted and tunnelled through existing networks.
Common use cases for this is to provide access to internal networks for remote workers, and for routing internet traffic through another machine for various reasons e.g. when using untrusted wifi, privacy from a snooping ISP, circumventing geoblock etc.
It is a protocol that has been worked on and evolved over the decades.
@@ -38,16 +37,16 @@ The modes can be categorized into two main categories: static mode and TLS mode.
The former mode uses static symmetric keys, and will be removed in the upcoming OpenVPN™ 2.7 (community edition).
I will not focus on static mode in this post.
The latter uses separate data & control channels where the control channel uses TLS - more on that later.
-
Why reimplement it? And why in OCaml?
+
Why reimplement it? And why in OCaml?
Before diving into TLS mode and eventually tls-crypt-v2 it's worth to briefly discuss why we spend time reimplementing the OpenVPN™ protocol.
You may ask yourself: why not just use the existing tried and tested implementation?
OpenVPN™ community edition is implemented in the C programming language.
-It heavily uses the OpenSSL library[1] which is as well written in C and has in the past had some notable security vulnerabilities.
+It heavily uses the OpenSSL library[^mbedtls] which is as well written in C and has in the past had some notable security vulnerabilities.
Many vulnerabilities and bugs in C can be easily avoided in other languages due to bounds checking and stricter and more expressive type systems.
The state machine of the protocol can be more easily be expressed in OCaml, and some properties of the protocol can be encoded in the type system.
Another reason is Mirage OS, a library operating system implemented in OCaml.
We work on the Mirage project and write applications (unikernels) using Mirage.
-In many cases it would be desirable to be able to connect to an existing VPN network[2],
+In many cases it would be desirable to be able to connect to an existing VPN network[^vpn-network],
or be able to offer a VPN network to clients using OpenVPN™.
Consider a VPN provider:
The VPN provider runs many machines that run an operating system in order to run the user-space OpenVPN™ service.
@@ -61,7 +60,7 @@ The networking provided to a application (virtual machine) can be restricted to
It is possible to use OpenVPN™ for such a setup, but that requires running OpenVPN™ in a full Linux virtual machine.
With Mirage OS the resource footprint is typically much smaller than an equivalent application running in a Linux virtual machine; often the memory footprint is smaller by an order.
Finally, while it's not an explicit goal of ours, reimplementing a protocol without an explicit specification can help uncover bugs and things that need better documentation in the original implementation.
-
TLS mode
+
TLS mode
There are different variants of TLS mode, but what they share is separate "control" channel and "data" channel.
The control channel is used to do a TLS handshake, and with the established TLS session data channel encryption keys, username/password authentication, etc. is negotiated.
Once this dance has been performed and data channel encryption keys have been negotiated the peers can exchange IP packets over the data channel.
@@ -72,7 +71,7 @@ This makes it possible for an OpenVPN™ server to reject early clients that don
In tls-crypt the control channel is encrypted as well as hmac authenticated using a pre-shared key.
Common to both is that the pre-shared key is shared between the server and all clients.
For large deployments this significantly reduces the usefulness - the key is more likely to be leaked the greate the number of clients who share this key.
-
tls-crypt-v2
+
tls-crypt-v2
To improve on tls-crypt, tls-crypt-v2 uses one pre-shared key per client.
This could be a lot of keys for the server to keep track of, so instead of storing all the client keys on the server the server has a special tls-crypt-v2 server key that is used to wrap the client keys.
That is, each client has their own client key as well as the client key wrapped using the server key.
@@ -98,7 +97,7 @@ The server responds in a similar manner with a sequence number of 0x0f0000
At the moment only one tag and one value is defined which signifies the server supports HMAC cookies - this seems unnecessarily complex, but is done to allow future extensibility.
Finally, if the server supports HMAC cookies, the client sends a packet where the wrapped key is appended in cleartext.
The server is now able to decrypt the third packet without having to keep the key from the first packet around and can verify the session id.
-
Cool! Let's deploy it!
+
Cool! Let's deploy it!
Great!
We build on a daily basis unikernels in our reproducible builds setup.
At the time of writing we have published a Miragevpn router unikernel acting as a client.
@@ -106,12 +105,8 @@ For general instructions on running Mirage unikernels see our GitHub, by mail or me personally on Mastodon if you're stuck.
-
-
-
It is possible to compile OpenVPN™ community edition with Mbed TLS instead of OpenSSL which is written in C as well.
I use the term "VPN network" to mean the virtual private network itself. It is a bit odd because the 'N' in 'VPN' is 'Network', but without disambiguation 'VPN' could refer to the network itself, the software or the service.
[^mbedtls]: It is possible to compile OpenVPN™ community edition with Mbed TLS instead of OpenSSL which is written in C as well.
+
[^vpn-network]: I use the term "VPN network" to mean the virtual private network itself. It is a bit odd because the 'N' in 'VPN' is 'Network', but without disambiguation 'VPN' could refer to the network itself, the software or the service.
diff --git a/articles/qubes-miragevpn.html b/articles/qubes-miragevpn.html
index b47e5a1..3f0ca9b 100644
--- a/articles/qubes-miragevpn.html
+++ b/articles/qubes-miragevpn.html
@@ -1,4 +1,3 @@
-
@@ -6,13 +5,13 @@
- Robur's blog - qubes-miragevpn, a MirageVPN client for QubesOS
+ Robur's blogqubes-miragevpn, a MirageVPN client for QubesOS
-
-
-
-
+
+
+
+
@@ -21,11 +20,11 @@
The Robur cooperative blog.
- Back to index
+ Back to index
We are pleased to announce the arrival of a new unikernel:
qubes-miragevpn. The latter is the result of work begun
several months ago on miragevpn.
Indeed, with the ambition of completing our unikernel suite and the success of
@@ -34,7 +33,7 @@ QubesOS - we thought it would be a good idea to offer this community a unikernel
capable of acting as an OpenVPN client, from which other virtual machines (app
qubes) can connect so that all their connections pass through the OpenVPN
tunnel.
-
QubesOS & MirageOS
+
QubesOS & MirageOS
Unikernels and QubesOS have always been a tempting idea for users in the sense
that a network application (such as a firewall or VPN client) could be smaller
than a Linux kernel: no keyboard, mouse, wifi management, etc. Just network
@@ -60,7 +59,7 @@ fine example of what can actually be done with MirageOS, and of real utility.
mato were (and still are) heavily involved in the work between QubesOS
and MirageOS. We'd also like to thank them, because if we're able to continue
this adventure, it's also thanks to them.
-
QubesOS & MirageVPN
+
QubesOS & MirageVPN
So, after a lengthy development phase for MirageVPN, we set about developing a
unikernel for QubesOS to offer an OpenVPN client as an operating system. We'd
like to give special thanks to Pierre Alain, who helped us to better
diff --git a/articles/speeding-ec-string.html b/articles/speeding-ec-string.html
index ed0099b..3242982 100644
--- a/articles/speeding-ec-string.html
+++ b/articles/speeding-ec-string.html
@@ -1,4 +1,3 @@
-
@@ -6,13 +5,13 @@
- Robur's blog - Speeding elliptic curve cryptography
+ Robur's blogSpeeding elliptic curve cryptography
-
-
-
-
+
+
+
+
@@ -21,24 +20,24 @@
The Robur cooperative blog.
- Back to index
+ Back to index
TL;DR: replacing cstruct with string, we gain a factor of 2.5 in performance.
+
Mirage-crypto-ec
In April 2021 We published our implementation of elliptic curve cryptography (as mirage-crypto-ec opam package) - this is DSA and DH for NIST curves P224, P256, P384, and P521, and also Ed25519 (EdDSA) and X25519 (ECDH). We use fiat-crypto for the cryptographic primitives, which emits C code that by construction is correct (note: earlier we stated "free of timing side-channels", but this is a huge challenge, and as reported by Edwin Török likely impossible on current x86 hardware). More C code (such as point_add, point_double, and further 25519 computations including tables) have been taken from the BoringSSL code base. A lot of OCaml code originates from our TLS 1.3 work in 2018, where Etienne Millon, Nathan Rebours, and Clément Pascutto interfaced elliptic curves for OCaml (with the goal of being usable with MirageOS).
The goal of mirage-crypto-ec was: develop elliptic curve support for OCaml & MirageOS quickly - which didn't leave much time to focus on performance. As time goes by, our mileage varies, and we're keen to use fewer resources - and thus fewer CPU time and a smaller memory footprint is preferable.
-
Memory allocation and calls to C
+
Memory allocation and calls to C
OCaml uses managed memory with a generational copying collection. To safely call a C function at any point in time when the arguments are OCaml values (memory allocated on the OCaml heap), it is crucial that while the C function is executed, the arguments should stay at the same memory location, and not being moved by the GC. Otherwise the C code may be upset retrieving wrong data or accessing unmapped memory.
There are several strategies to achieve this, ranging from "let's use another memory area where the GC doesn't mess around with", "do not run any GC while executing the C code" (read further in the OCaml cheaper C calls manual), "deeply copy the arguments to a non-moving memory area before executing C code", and likely others.
For our elliptic curve operations, the C code is pretty simple - there are no memory allocations happening in C, neither are exceptions raised. Also, the execution time of the code is constant and pretty small.
-
ocaml-cstruct
+
ocaml-cstruct
In the MirageOS ecosystem, a core library is cstruct - which purpose is manifold: provide ppx rewriters to define C structure layouts in OCaml (getter/setter functions are generated), as well as enums; also a fundamental idea is to use OCaml bigarray which is non-moving memory not allocated on the OCaml heap but directly by calling malloc. The memory can even be page-aligned, as required by some C software, such as Xen. Convenient functionality, such as "retrieve a big-endian unsigned 32 bit integer from offset X in this buffer" are provided as well.
But there's a downside to it - as time moves along, Xen is no longer the only target for MirageOS, and other virtualization mechanisms (such as KVM / virtio) do not require page-aligned memory ranges that are retained at a given memory address. It also turns out that cstruct spends a lot of time in bounds checks. Another huge downside is that OCaml tooling (such as statmemprof) was for a long time (maybe still is not?) unaware of out-of-OCaml-GC allocated memory (cstruct uses bigarray as underlying buffer). Freeing up the memory requires finalizers to be executed - after all pretty tedious (expensive) and against the OCaml runtime philosophy.
As time moves forward, also the OCaml standard library got support for (a) strings are immutable byte vectors now (since 4.06 - released in 2017 -- there's as well an interface for mutable/immutable cstruct, but that is not used as far as I can tell), (b) retrieve a certain amount of octets in a string or byte as (unsigned) integer number (since 4.08 - released in 2019, while some additional functionality is only available in 4.13).
Still, bigarrays are necessary in certain situations - if you need to have a non-moving (shared) area of memory, as in the Xen interface, but also e.g. when you compute in parallel in different processes, or when you need mmap()ed files.
-
Putting it together
+
Putting it together
Already in October 2021, Romain proposed to not use cstruct, but bytes for mirage-crypto-ec. The PR was sitting around since there were benchmarks missing, and developer time was small. But recently, Virgile Robles proposed another line of work to use pre-computed tables for NIST curves to speed up the elliptic curve cryptography. Conducting performance evaluation resulted that the "use bytes instead of cstruct" combined with pre-computed tables made a huge difference (factor of 6) compared to the latest release.
To ease reviewing changes, we decided to focus on landing the "use bytes instead of cstruct" first, and gladly Pierre Alain had already rebased the existing patch onto the latest release of mirage-crypto-ec. We also went further and use string where applicable instead of bytes. For safety reasons we also introduced an API layer which (a) allocates a byte vector for the result (b) calls the primitive, and (c) transforms the byte vector into an immutable string. This API is more in line with functional programming (immutable values), and since allocations and deallocations of values are cheap, there's no measurable performance decrease.
All the changes are internal, there's no external API that needs to be adjusted - still there's at the API boundary one conversion of cstruct to string (and back for the return value) done.
@@ -48,81 +47,25 @@
With PR#146, the flame graph looks different:
Now, the allocation towers do not exist anymore. The time of a sign operation is spend in inv, scalar_mult, and x_of_finite_point_mod_n. There's still room for improvements in these operations.
-
Performance numbers
+
Performance numbers
All numbers were gathered on a Lenovo X250 laptop with a Intel i7-5600U CPU @ 2.60GHz. We used OCaml 4.14.1 as compiler. The baseline is OpenSSL 3.0.12. All numbers are in operations per second.
NIST P-256
-
-
-
op
-
0.11.2
-
PR#146
-
speedup
-
OpenSSL
-
speedup
-
-
-
sign
-
748
-
1806
-
2.41x
-
34392
-
19.04x
-
-
-
verify
-
285
-
655
-
2.30x
-
12999
-
19.85x
-
-
-
ecdh
-
858
-
1785
-
2.08x
-
16514
-
9.25x
-
-
Curve 25519
-
-
-
op
-
0.11.2
-
PR#146
-
speedup
-
OpenSSL
-
speedup
-
-
-
sign
-
10713
-
11560
-
1.08x
-
21943
-
1.90x
-
-
-
verify
-
7600
-
8314
-
1.09x
-
7081
-
0.85x
-
-
-
ecdh
-
12144
-
13457
-
1.11x
-
26201
-
1.95x
-
-
Note: to re-create the performance numbers, you can run openssl speed ecdsap256 ecdhp256 ed25519 ecdhx25519 - for the OCaml site, use dune bu bench/speed.exe --rel and _build/default/bench/speed.exe ecdsa-sign ecdsa-verify ecdh-share.
Note: to re-create the performance numbers, you can run openssl speed ecdsap256 ecdhp256 ed25519 ecdhx25519 - for the OCaml site, use dune bu bench/speed.exe --rel and _build/default/bench/speed.exe ecdsa-sign ecdsa-verify ecdh-share.
The performance improvements are up to 2.5 times compared to the latest mirage-crypto-ec release (look at the 4th column). In comparison to OpenSSL, we still lack a factor of 20 for the NIST curves, and up to a factor of 2 for 25519 computations (look at the last column).
If you have ideas for improvements, let us know via an issue, eMail, or a pull request :) We started to gather some for 25519 by comparing our code with changes in BoringSSL over the last years.
As a spoiler, for P-256 sign there's another improvement of around 4.5 with Virgile's PR using pre-computed tables also for NIST curves.
-
The road ahead for 2024
+
The road ahead for 2024
Remove all cstruct, everywhere, apart from in mirage-block-xen and mirage-net-xen ;). It was a fine decision in the early MirageOS days, but from a performance point of view, and for making our packages more broadly usable without many dependencies, it is time to remove cstruct. Earlier this year we already removed cstruct from ocaml-tar for similar reasons.
Our MirageOS work is only partially funded, we cross-fund our work by commercial contracts and public (EU) funding. We are part of a non-profit company, you can make a (tax-deducable - at least in the EU) donation (select "DONATION robur" in the dropdown menu).
We're keen to get MirageOS deployed in production - if you would like to do that, don't hesitate to reach out to us via eMail team at robur.coop
diff --git a/articles/tar-release.html b/articles/tar-release.html
index 91ed602..faf10bf 100644
--- a/articles/tar-release.html
+++ b/articles/tar-release.html
@@ -1,4 +1,3 @@
-
@@ -6,13 +5,13 @@
- Robur's blog - The new Tar release, a retrospective
+ Robur's blogThe new Tar release, a retrospective
-
-
-
-
+
+
+
+
@@ -21,11 +20,11 @@
The Robur cooperative blog.
- Back to index
+ Back to index
We are delighted to announce the new release of ocaml-tar. A small library for
reading and writing tar archives in OCaml. Since this is a major release, we'll
take the time in this article to explain the work that's been done by the
cooperative on this project.
@@ -37,7 +36,7 @@ and a project that's been around since... 2012 (over 10 years!).
But we intend to maintain and improve it, since we're using it for the
opam-mirror project among other things - this unikernel is to
provide an opam-repository "tarball" for opam when you do opam update.
-
Cstruct.t & bytes
+
Cstruct.t & bytes
As some of you may have noticed, over the last few months we've begun a fairly
substantial change to the Mirage ecosystem, replacing the use of Cstruct.t in
key places with bytes/string.
@@ -54,7 +53,7 @@ buffer, invalid access). There's also a small benchmark to support our initial
intuition1.
But this PR can also be an opportunity to understand the existence of
Cstruct.t in the Mirage ecosystem and the reasons for this historic choice.
-
Cstruct.t as a non-moveable data
+
Cstruct.t as a non-moveable data
I've already made a list of pros/cons when it comes to
bigarrays. Indeed, Cstruct.t is based on a bigarray:
type buffer = (char, Bigarray.int8_unsigned_elt, Bigarray.c_layout) Bigarray.Array1.t
@@ -111,7 +110,7 @@ knowing when to free() the zone as soon as the value is no longer i
Reference-counting is used to then allocate "small" values in the OCaml heap
and use them to manipulate indirectly the bigarray.
-
Ownership, proxy and GC
+
Ownership, proxy and GC
This last point deserves a little clarification, particularly with regard to the
Bigarray.sub function. This function will not create a new, smaller bigarray
and copy what was in the old one to the new one (as Bytes.sub/String.sub
@@ -155,7 +154,7 @@ ownership of a Cstruct.t in the type to prevent unauthorized access
place on this subject2.
It should be noted that, with regard to the third point, the problem also
applies to bytes and the use of Bytes.unsafe_to_string!
-
Conclusion about Cstruct
+
Conclusion about Cstruct
We hope we've been thorough enough in our experience with Cstruct. If we go back
to the initial definition of our Cstruct.t shown above and take all the
history into account, it becomes increasingly difficult to argue for a
@@ -181,7 +180,7 @@ seems that the change is worthwhile.
capabilities and using the type system to enforce certain characteristics. To
date, Cstruct_cap has not been used anywhere, which raises a real question
about the advantages/disadvantages in everyday use.
-
Functors
+
Functors
This is perhaps the other point of the Mirage ecosystem that is also the subject
of debate. Functors! Before we talk about functors, we need to understand their
relevance in the context of Mirage.
@@ -272,7 +271,7 @@ do, then let the user implement the run function according to the s
In short, based on this list and the various experiments we've carried out on a
number of projects, we've decided to remove the functors from ocaml-tar! The
crucial question now is: which method to choose?
-
The best answers
+
The best answers
There's no real answer to that, and in truth it depends on what level of
abstraction you're at. In fact, you'd like to have a fairly simple method of
abstraction from the system at the start and at the lowest level, to end up
@@ -316,7 +315,7 @@ type ('a, 'err) t =
However, and this is where we come back to OCaml's limitations and where
functors could help us: higher kinded polymorphism!
-
Higher kinded Polymorphism
+
Higher kinded Polymorphism
If we return to our functor example above, there's one element that may be of
interest: T with type t = T.t succ
In other words, add a constraint to a signature type. A constraint often seen
@@ -388,7 +387,7 @@ val miou : 'a -> ('a, 'err, miou) t
But this way, Tar can always be derived from another system, and the process for
extracting entries from a Tar file is the same for all systems!