cryptoverif VS ssh

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):

I think for these use case a SSH server in Go would be way simpler such as https://github.com/gliderlabs/ssh

I’ve done very nearly this exact same thing using https://github.com/gliderlabs/ssh