markdascher

It's a good idea, and some sort of easily-verified compatibility with openssl was actually an early goal. But I gave up on that since the algorithms are so different. A compatible mode would end up sharing very little code, so it wouldn't say much about moochacha itself.

But good news! I've come up with... something.

https://codeberg.org/markdascher/moochacha/src/branch/main/o...

That strings together a combination of argon2 and openssl commands to decrypt a file. It's extremely unsafe though, since all of the secrets end up in command-line arguments. Also some of those commands might be new in OpenSSL 3.

I haven't yet. This was my path to Frama-C:

1. Try writing C code that's "obviously safe." Gave up on that pretty quickly.

2. Maybe if I make all buffers global, I can verify some basics with a script. Gave up when I learned that "abstract interpretation" already exists, and it's way more advanced than anything I could whip up. (But kept the global buffers for now...)

3. The only example I found for a while was https://github.com/NASA-SW-VnV/ikos, but it needed an old version of Clang, and my laptop didn't have enough memory to build it.

4. Found a couple other examples that were clearly someone's research project.

5. Finally found Frama-C by searching through Fedora packages. And it's exactly what I needed.

There's definitely a learning curve, and it's not always obvious how to get it to do what you want. But I can at least install it, there's a nice GUI, and it's thoroughly documented.

I didn't hear of CBMC until later, but I see there a Fedora package for that too. Should probably take a crack at it!

You're right. The honest answer is that my nose has been in this for so long that I've lost track of what's interesting and what isn't. =)

A big reason to mention quantum safety is just to make it an explicit goal. If I've accidentally chosen something that even smells uncertain, it's a bug. There are plenty of ways for symmetric key cryptosystems to accidentally weaken themselves, like leveraging a 128-bit intermediate key at some stage of the process.

Now, that might not even weaken things realistically, for all sorts of reasons. But I want something that you look at and say "yeah that's obviously fine," without having to think much. No surprises.

> Why 12288 bytes for p0?

Good question! Tripling the first block's size (12288=3x4096) happened the most recent commit, to make all of the Padmé sizes possible.

https://codeberg.org/markdascher/moochacha/commit/3145d7fb95...

The original encrypted format was more straightforward: 32 + 4112 + 4112 + ... + (last block, less than 4112) bytes. That initial 32-byte seed messed up the math just enough that a 2 MiB output was impossible. (It would require the last block be exactly 4112 bytes, which isn't allowed.)

If those extra 32 bytes weren't there, then it's a lot easier to calculate the impossible sizes, since they're just multiples of 4112. And those never collide with Padmé, at least for all 64-bit file sizes.

I like to think of that first block as 32+12288+16, getting block boundaries lined back up on even multiples of 4112.

This started out as an excuse to try writing C code safely. Eventually stumbled upon Frama-C, which is amazing.

But anyway, moochacha is a simple file encryption command based on libsodium's Argon2id, BLAKE2b, and ChaCha20-Poly1305. Nothing fancy, just symmetric encryption with a keyfile. It also supports optional padding to conceal file sizes.

After goofing around for months, I've just about reached the limit of my abilities, and am tempted to actually use it. Please talk some sense into me! See the README for a full specification. The UI could certainly be improved, but I'm mostly curious if there's anything unsafe about it.

Also, am I reinventing the wheel here? Similar tools either involve asymmetric algorithms or derive encryption keys directly from the password. I want the output to be safe even with a bad password, and even if quantum computing becomes absurdly successful.