Implement proper encryption and define FRAM format

[machdyne]

The "encryption" in the <= 0.0.3 firmware is not good and needs to be replaced with something better.

Additionally, because all of the FRAM is not used, there is an opportunity to use the extra space for something useful.

[machdyne]

An update for anyone interested in encryption on Stahl:

I have implemented ChaCha20-Poly1305 encryption on Blaustahl, the successor to Stahl, as it is a bit easier to work with, and there are many more of them "in the wild" than the original Stahl.

I would like to eventually get this working on Stahl as well, but it may take a while.

In the meantime I will gladly send a Blaustahl to anyone who previously purchased a Stahl, you can use this form to request one: https://machdyne.com/sample-request/

Thanks to @whitequark for the helpful advice on algorithms.

[whitequark]

@machdyne It's really nice to see AEAD based on mbedtls in Blaustahl! Something I want to highlight is the potential of nonce reuse. For ChaCha20-Poly1305, the key stream is determined by the (key, nonce) pair. If you ever reuse that pair, then you can decrypt both messages. This means that an attacker with physical read/write access can, through doing nothing but rolling back the nonce counter (i.e. no code changes, nothing else), break the confidentiality.

As I understand, an attacker with physical read/write access isn't a part of the threat model of the device, since the high-level architecture choices mean that anyone who holds the device in their hand must have this kind of access, and you'd have to lock it in a safe or something to avoid it.

The only way I can think of to alleviate this vulnerability is to display the nonce in the editor somehow, so that if someone rolls it back, a particularly paranoid user who is already ensuring the code on the RP2040 is exactly what it should be, would be able to guard against nonce rollbacks. But I don't think this is really a good way to do so since it relies on humans' notoriously great ability to remember long, meaningless numbers that change often.

Perhaps if you used RP2350 and its Secure Boot support you could detect and prevent nonce reuse, but with RP2040 I think you might be out of luck.

[whitequark]

On second thought, it might be worth it to use a scheme where for messages A, B (B comes directly after A), nonce_B = digest(A || nonce_A). In this case, nonces would no longer be sequential, and an attacker who has been reading out encrypted messages without modifying anything could no longer decrypt them after the fact by simply resetting the nonce counter to zero and then spending a while reading them out without modifying anything once more.

The whole thing feels really sketchy to me though.

[machdyne]

Thanks @whitequark, I hadn't considered that attack.

If I understand correctly this would only work if the attacker had access to the device on multiple occasions, where the user accessed it in between without noticing the rolled back nonce? But, if you simply lost the device, someone who found it wouldn't be able to access anything.

I thought about XChaCha20 with a random nonce and there is space for a 192-bit nonce, but I don't think it's supported by the version of mbedtls that's included with pico-sdk. Maybe that would solve the problem?

[whitequark]

If I understand correctly this would only work if the attacker had access to the device on multiple occasions, where the user accessed it in between without noticing the rolled back nonce? But, if you simply lost the device, someone who found it wouldn't be able to access anything.

That is correct. I was thinking about e.g. a partner who has access to your things being able to read the encrypted data. (This is more commonly called in the field an "evil maid attack", but I find it that domestic abuse is a lot more common in life than evil maids.)

I thought about XChaCha20 with a random nonce and there is space for a 192-bit nonce, but I don't think it's supported by the version of mbedtls that's included with pico-sdk. Maybe that would solve the problem?

Sorry, I don't fully understand the scheme proposed here, so I can't comment on it. I assumed that you have no source of randomness though, hence the digest-based nonce generation scheme that I proposed.