cryptoverif
cryptsetup-ssh-unlocker
| cryptoverif | cryptsetup-ssh-unlocker | |
|---|---|---|
| 1 | 1 | |
| 4 | 14 | |
| - | - | |
| - | - | |
| over 7 years ago | over 5 years ago | |
| OCaml | Python | |
| GNU General Public License v3.0 or later | MIT License |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
cryptoverif
-
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):
cryptsetup-ssh-unlocker
-
Tinyssh
A tool based on Dropbear that does exactly this, automatically.
https://github.com/ViktorStiskala/cryptsetup-ssh-unlocker