cryptoverif VS tinyssh

A better question to ask would have been, why settle for just memory safety - does a formally verified sshd exist? That kind of thing seems to be implemented more in OCaml and F#, like Project Everest, which has formally verified implementations of primitives (HACL) TLS, QUIC, and Signal https://project-everest.github.io/ ... ssh is notably missing?

I had a dig and found that ssh had in fact been done 9 years ago, tho it doesn't seem to have made it to a distribution: it's an offshoot of the CryptoVerif project[1] (which is, maybe unsurprisingly, under the umbrella of the same Prosecco team at Inria who worked on Project Everest). In 2015 Bruno Blanchet and David Cadé wrote a paper "From Computationally-Proved Protocol Specifications to Implementations and Application to SSH"[2] which describes using CryptoVerif to generate an implementation of SSH from the spec; the code is in the CryptoVerif tarball, but someone's helpfully put that up on github if you want a look https://github.com/mgrabovsky/cryptoverif/tree/master/implem...

The eye opening bits in the paper (given the claims of tinyssh to be small at < 100k words):

While on topic of sshd having minimal dependencies, shout-out to Jan Mojžíš and his minimalist implementation:

https://github.com/janmojzis/tinyssh/

> [after] hardening steps [...] most of the bots can't even negotiate a connection

Yep, same here, except I'm using [tinyssh], which organically does not support anything other than ed25519/curve25519, sha256, and chacha-poly.

[tinyssh] https://tinyssh.org/

djb suggested that for openssh instead of the tinydns kex, so tinydns switched also:

https://github.com/janmojzis/tinyssh/issues/50