Live data from Hacker News

TinySSH is a small SSH server using NaCl, TweetNaCl

github.com

101–110 of 128 posts

Re: TinySSH is a small SSH server using NaCl, TweetNaCl

#101

[flagged]

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[3]

The eye opening bits in the paper (given the claims of tinyssh to be small at The bad news would be that it's not very performant: 30MB/s compared to 90MB/s for openssh on the same hardware, in the paper. Since HACL is from the same stable and was designed to perform well as well as be verified, it might be worth dusting off and seeing if this could be made more usable. The implementation probably has value even if just as a test oracle.

[1]: https://bblanche.gitlabpages.inria.fr/CryptoVerif/

[2]: https://bblanche.gitlabpages.inria.fr/publications/CadeBlanc...

[3]: https://github.com/mgrabovsky/cryptoverif/tree/master/implem... the official implementation appears to be here now https://gitlab.inria.fr/bblanche/CryptoVerif/-/tree/master/c...

Re: TinySSH is a small SSH server using NaCl, TweetNaCl

#102
post #58

Cool but something i saw that was weird, this may be the first repo i've ever seen to advertise ... words of code, i've always seen secure repos advertise their "in only X LOC" seeing words of code as a metric was funny

The Wren language[0] uses semicolons as its size metric: Wren is small. The VM implementation is under 4,000 semicolons. You can skim the whole thing in an afternoon. It’s small, but not dense. It is readable and lovingly-commented. [0] https://wren.io/

Semicolons seems an odd metric since complexity is often introduced by if-else branches, while loops, and function declarations. Each of those doesn't involve semicolons.

Re: TinySSH is a small SSH server using NaCl, TweetNaCl

#104

Earlier quoted context omitted.

> how do you make sure the boot has not been compromised and that you are not just sending the password to the bad guys? In my case, I can't. This is a NAS in my house and this is mostly to prevent me from having to go to another room and plug in a monitor and keyboard. (Also, I've done this from across the country after a power outage.) The threat vectors I'm protecting against are I guess mostly theft of the entire…

This is mostly me but the case that's the most common is that a disk can't be wiped because its dead. Gotta do that before hand.

Well you can always drill holes in the platter, or hit them with a strong magnet, or just separate them and toss them in the trash. Unless you're fighting the NSA, you can probably get away with enough physical destruction to make recovery challenging.

Re: TinySSH is a small SSH server using NaCl, TweetNaCl

#105
post #84
post #44

Earlier quoted context omitted.

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

Isn’t there a host SSH key involved? The server itself may have been physically breached, and if so you can’t trust anything. But, if your host key matches, you should be confident that at least you’re logging into the correct machine (there was no IP takeover).

[deleted]

Re: TinySSH is a small SSH server using NaCl, TweetNaCl

#106
post #37

tinyssh is great. One use case for it that people may not know about: using it during Linux boot so you can remotely unlock encrypted drives. I have a headless NAS server that uses dm-crypt/LUKS under ZFS. When I update my kernel/ZFS I remotely reboot the server, wait a few seconds, and then ssh into a tinyssh powered encryption key prompt to unlock the drives. (I am immediately booted from ssh, as tinyssh exits.) I…

A tool based on Dropbear that does exactly this, automatically. https://github.com/ViktorStiskala/cryptsetup-ssh-unlocker

The documentation for Cryptsetup SSH unlocker states “To further limit the attack possibility, you should use monitoring and possibly disable SSH unlocker in the case of unexpected behavior.” Mandos has a built-in feature to deal with this, enabled by default.

(Again, disclosure: I am the co-author of Mandos.)

Re: TinySSH is a small SSH server using NaCl, TweetNaCl

#107

>easy auditable - TinySSH has less than 100000 words of code Is approximately one hundred thousand words really easily auditable?

What is a "word of code"? I've seen "lines of code" but what's a "word" in C?

Maybe M-x count-words?

Re: TinySSH is a small SSH server using NaCl, TweetNaCl

#108
post #83

tinyssh is great. One use case for it that people may not know about: using it during Linux boot so you can remotely unlock encrypted drives. I have a headless NAS server that uses dm-crypt/LUKS under ZFS. When I update my kernel/ZFS I remotely reboot the server, wait a few seconds, and then ssh into a tinyssh powered encryption key prompt to unlock the drives. (I am immediately booted from ssh, as tinyssh exits.) I…

For debian/ubuntu users, there's also dropbear-initramfs package with same functionality (works with any fs luks/ext4/lvm/zfs/etc). https://packages.debian.org/bookworm/dropbear-initramfs https://packages.ubuntu.com/jammy/dropbear-initramfs

Note: Mandos is also in Debian and Ubuntu.

(Obligatory disclaimer: I am a co-author of Mandos)

Re: TinySSH is a small SSH server using NaCl, TweetNaCl

#109

I don't see anyone sensible replacing OpenSSH with anything else for two fundamental reasons: 1. OpenSSH has more eyes on it and more deployments than almost any other piece of non-OS/kernel software on the planet. By this stage in its life, it is very mature. Look at the vulnerability database, OpenSSH has not had a serious REMOTE vulnerability for a long time, all the recent vulnerabilities require the attacker to…

Bad reasons to trust code:

* “Many __informal__ eyes have probably looked at it”

* Lack of recent __number__ of (known) vulnerabilities

* “Serious guys” (appeal to authority)

I think you’re using short-hand, but perhaps the short-hand should be different. E.g.

* A list of audits by date, independent organization, is provided __here__ which is evidence of review

* The vulnerability acknowledgement, correction and release process is prompt, accurate and detailed, which is documented __here__

* XYZ coding, testing, fuzzing, proving, bounty, integration with other systems, documentation, defaults etc. practices are used in the interest in hardening the code, limiting moving parts, attack radius, etc.

Re: TinySSH is a small SSH server using NaCl, TweetNaCl

#110
post #44

tinyssh is great. One use case for it that people may not know about: using it during Linux boot so you can remotely unlock encrypted drives. I have a headless NAS server that uses dm-crypt/LUKS under ZFS. When I update my kernel/ZFS I remotely reboot the server, wait a few seconds, and then ssh into a tinyssh powered encryption key prompt to unlock the drives. (I am immediately booted from ssh, as tinyssh exits.) I…

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

Mandos tries to mitigate this problem by periodically checking that the rebooting server is still up. Exactly how this is done is configurable, but by default it uses ssh-keyscan to check if the server is up and using the SSH server key from its normal encrypted root file system. If a server is ever down too long (configurable, default 5 minutes), the Mandos server will “disable” that server in its server list, and not provide the password to that server anymore.

The idea is that you should configure the timeout to be long enough to allow for a normal kernel panic and reboot, but hopefully short enough that it would be hard for anyone to compromise the server in that time. It’s not a perfect solution, but it’s the best anyone has come up with as far as I know.

(Disclosure: I am a co-author of Mandos.)

Post reply on HN