cryptoverif
ultrablue
| cryptoverif | ultrablue | |
|---|---|---|
| 1 | 2 | |
| 4 | 126 | |
| - | 0.0% | |
| - | - | |
| over 7 years ago | about 1 year ago | |
| OCaml | Kotlin | |
| GNU General Public License v3.0 or later | Apache License 2.0 |
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):
ultrablue
- Ultrablue: User-Friendly Lightweight TPM Remote Attestation over Bluetooth
-
Tinyssh
Question: when remotely unlock the boot disk via ssh, how do you make sure the boot has not been compromised and that you are not just sending the password to the bad guys?
At some point I wanted to do something with utrablue [1], to work over network rather than Bluetooth, but then it was in go and I got lazy suddenly :)
[1] https://github.com/ANSSI-FR/ultrablue