diff --git a/articles/2024-02-03-python-str-repr.html b/articles/2024-02-03-python-str-repr.html index fb280db..a7cdb2e 100644 --- a/articles/2024-02-03-python-str-repr.html +++ b/articles/2024-02-03-python-str-repr.html @@ -53,7 +53,7 @@ and eventually I decided to take a more rigorous approach to it.

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[^python-bytes]. +In Python there is the str type which is a sequence of Unicode code points[1]. 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. @@ -81,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 '\\"'[^raw-escape-example]. +But r"\"" is fine as is interpreted as '\\"'[2]. 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.

@@ -247,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[^language-lawyer] level understanding. +It is not easy to get a language lawyer[3] 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. @@ -261,10 +261,15 @@ 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.

-

[^python-bytes]: There is as well the bytes type which is a byte sequence like OCaml's string. +

    +
  1. +

    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.

    -

    [^raw-escape-example]: Note I use single quotes for the output. This is what Python would do. It would be equivalent to "\\\"".

    -

    [^language-lawyer]: A person, usually an experienced or senior software engineer, who is intimately familiar with many or most of the numerous restrictions and features (both useful and esoteric) applicable to one or more computer programming languages. A language lawyer is distinguished by the ability to show you the five sentences scattered through a 200-plus-page manual that together imply the answer to your question “if only you had thought to look there”.

    +↩︎︎
  2. +

    Note I use single quotes for the output. This is what Python would do. It would be equivalent to "\\\"".

    +↩︎︎
  3. +

    A person, usually an experienced or senior software engineer, who is intimately familiar with many or most of the numerous restrictions and features (both useful and esoteric) applicable to one or more computer programming languages. A language lawyer is distinguished by the ability to show you the five sentences scattered through a 200-plus-page manual that together imply the answer to your question “if only you had thought to look there”.

    +↩︎︎
diff --git a/articles/2024-08-21-OpenVPN-and-MirageVPN.html b/articles/2024-08-21-OpenVPN-and-MirageVPN.html index bd820bf..0683731 100644 --- a/articles/2024-08-21-OpenVPN-and-MirageVPN.html +++ b/articles/2024-08-21-OpenVPN-and-MirageVPN.html @@ -30,7 +30,7 @@ In order to implement this side of the protocol I studied parts of the OpenVPN 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[^openvpn-tls] with which key material and configuration options are negotiated. +The OpenVPN protocol establishes a TLS tunnel[1] 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):

@@ -40,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[^disconnect] from the server. +They are all three used to signal to the client that it should disconnect[2] 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. @@ -67,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)[^kill-immediately]. +I learnt that it shares code paths with the exit control messages to schedule an exit (disconnect)[3]. 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. @@ -86,7 +86,7 @@ The OpenVPN security@ mailing list took it seriously enough to assign it CVE-202 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[^proto-push-request]. +The client signals it would like to receive configuration options from the server by sending the PUSH_REQUEST control channel message[4]. 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.

    @@ -94,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[^inline-files]. -A line is whatever fgets() says it is - this includes the newline if not at the end of the file[^configuration-newlines]. +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]. 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.

    @@ -210,12 +210,20 @@ 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.

    -

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

    +
      +
    1. +

      This is not always the case. It is possible to use static shared secret keys, but it is mostly considered deprecated.

      +↩︎︎
    2. +

      I say "disconnect" even when the underlying transport is the connection-less UDP.

      +↩︎︎
    3. +

      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.

      +↩︎︎
    4. +

      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.

      +↩︎︎
    5. +

      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.

      +↩︎︎
    6. +

      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 22d046c..aeba524 100644 --- a/articles/gptar.html +++ b/articles/gptar.html @@ -78,7 +78,7 @@ Then I got a hunch: I had read about [1]. 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. @@ -131,7 +131,10 @@ 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!

    -

    [^tar-ustar]: This is somewhat simplified. There are some more nuances between the different formats, but for this purpose they don't matter much.

    +
      +
    1. +

      This is somewhat simplified. There are some more nuances between the different formats, but for this purpose they don't matter much.

      +↩︎︎
    diff --git a/articles/miragevpn-performance.html b/articles/miragevpn-performance.html index fba0826..591b8f9 100644 --- a/articles/miragevpn-performance.html +++ b/articles/miragevpn-performance.html @@ -35,7 +35,7 @@ To better guide the performance engineering, we also developed Takeaway of performance engineering

    The learnings of our performance engineering are in three areas:

    @@ -43,7 +43,10 @@ To better guide the performance engineering, we also developed 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.

    -

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

    +
      +
    1. +

      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.html b/articles/miragevpn.html index 8ee224a..bb531fc 100644 --- a/articles/miragevpn.html +++ b/articles/miragevpn.html @@ -41,12 +41,12 @@ The latter uses separate data & control channels where the control channel u

    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[^mbedtls] which is as well written in C and has in the past had some notable security vulnerabilities. +It heavily uses the OpenSSL library[1] 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[^vpn-network], +In many cases it would be desirable to be able to connect to an existing VPN network[2], 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. @@ -105,8 +105,12 @@ For general instructions on running Mirage unikernels see our GitHub, by mail or me personally on Mastodon if you're stuck.

    -

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

    +
      +
    1. +

      It is possible to compile OpenVPN™ community edition with Mbed TLS instead of OpenSSL which is written in C as well.

      +↩︎︎
    2. +

      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/speeding-ec-string.html b/articles/speeding-ec-string.html index 3242982..09c3085 100644 --- a/articles/speeding-ec-string.html +++ b/articles/speeding-ec-string.html @@ -50,18 +50,74 @@

    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.

    +
    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    op0.11.2PR#146speedupOpenSSLspeedup
    sign74818062.41x3439219.04x
    verify2856552.30x1299919.85x
    ecdh85817852.08x165149.25x

    Curve 25519

    +
    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    op0.11.2PR#146speedupOpenSSLspeedup
    sign10713115601.08x219431.90x
    verify760083141.09x70810.85x
    ecdh12144134571.11x262011.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.

    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.