[HN Gopher] Show HN: Moochacha, quantum-safe file encryption (an...
___________________________________________________________________
Show HN: Moochacha, quantum-safe file encryption (analyzed by
Frama-C)
Author : markdascher
Score : 53 points
Date : 2023-02-23 21:58 UTC (1 days ago)
(HTM) web link (codeberg.org)
(TXT) w3m dump (codeberg.org)
| tptacek wrote:
| Help me understand how this is quantum-safe in any sense that all
| other symmetric encryption is? I'm not critiquing, I'm just
| giving you the data point that I'm probably missing something
| here.
| monero-xmr wrote:
| Isn't all symmetric encryption using one time pads safe from
| quantum decryption? It's a weird thing to lead with considering
| all symmetric is safe
| tptacek wrote:
| I don't pretend to understand the "keyfile" thing here. I
| guess that's what I'm asking: if this is at bottom just a
| symmetric key cryptosystem, like, even an encrypted DMG is
| "safe" in that sense.
| markdascher wrote:
| 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.
| markdascher wrote:
| 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.
| chasil wrote:
| Can you make a mode that is compatible with the -chacha option
| to (modern) "openssl enc" output?
|
| That level of interoperability would greatly increase
| confidence, I think, but this doesn't use Argon2id and BLAKE2b.
| $ echo foobar > .pwfile $ openssl enc -chacha20 -e
| -pbkdf2 -pass file:.pwfile -in sensitive.db -out sensitive.cha
| $ openssl enc -chacha20 -d -pbkdf2 -pass file:.pwfile -in
| sensitive.cha -out test.db $ diff test.db
| sensitive.db $
| naasking wrote:
| Cool, I've been meaning to try out Frama-C and other
| verification tools. Have you tried CBMC or similar tools at
| all?
| markdascher wrote:
| 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!
| junon wrote:
| Frama-C is indeed pretty cool, as long as your application is
| pretty self contained. Using frama-c on code that runs e.g. in
| the kernel breaks its models too much.
| zxexz wrote:
| I love this, thank you. It's a topic I've oft thought about, and
| I'm having fun reading through the code - I was just thinking
| earlier today that I need to brush up on my C, as I was going
| through some of my own, old, code, I can barely follow.
|
| Thanks for posting!
| bawolff wrote:
| Its pretty clickbaity to call symmetric encryption "quantum
| safe". Of course its quantum safe, the whole quantum crypto
| issues are with asymmetric crypto not symmetric*
|
| * yes, yes, you want longer key lengths because of grover, but
| realistically that's not a threat anytime soon and also trivial
| to work around.
| ThePhysicist wrote:
| Looks really cool. A bit surprised no one here told you to "not
| roll your own crypto yet". Great that you specified the protocol
| and threat model in any case. Why 12288 bytes for p0?
| progre wrote:
| I think most people mean "don't roll yor own _and use it in
| production_ "
|
| Writing your own crypto for fun should be encuraged.
| markdascher wrote:
| > 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 Padme 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 Padme, 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.
| latenightcoding wrote:
| Author is not rolling their own crypto. They are using
| libsodium.
| touisteur wrote:
| Almost as fun as SPARK's own Rod Chapman doing some tweetnacl
| porting and proof https://blog.adacore.com/sparknacl-two-
| years-of-optimizing-c...
| stan_kirdey wrote:
| nothing is quantum safe until there is quantum compute
___________________________________________________________________
(page generated 2023-02-24 23:01 UTC)