4 ms·

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 encrypti

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.

naasking 4y ago
Cool, I've been meaning to try out Frama-C and other verification tools. Have you tried CBMC or similar tools at all?
- markdascher 4y ago
  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 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!
  - fdupress 4y ago
    You could also try VeriFast [0], which is closer to Frama-C than CBMC. (VeriFast and Frama-C are deductive verification tools, CBMC is a bounded model checking tool.) It is slightly less approachable than Frama-C because it uses separation logic, but it's slightly more approachable because it uses symbolic execution, which allows it to display an actual execution trace that causes the failure. (You can then inspect that and decide whether your code or model is wrong.) [0]: https://github.com/verifast/verifast https://github.com/verifast/verifast
    - naasking 4y ago
      Good reference, I had actually starred that on github to refer to later and totally forgot about it. Do you know of a review of the various open source verification tools available for C? The ones I'm aware of: CBMC, Frama-C, VeriFast, ESBMC. I've found papers like [1] which benchmark various model checkers, but no evaluation of the verification effort required for the various approaches. Edit: the tutorial for VeriFast does not make it look very usable compared to Frama-C's ACSL language. Their tutorial doesn't explain a bunch of the syntax or why they made certain choices, so it all feels very unergonomic. Edit 2: The SV-COMP competition on software verification [2] tests a whole bunch of tools, but Frama-C and VeriFast are not among them. Looks like CPAChecker [3] has the best power-to-weight ratio if you're looking for one tool to learn with the most errors caught across all benchmarks. [1] https://arxiv.org/abs/2003.11689 https://arxiv.org/abs/2003.11689 [2] https://sv-comp.sosy-lab.org/2020/ https://sv-comp.sosy-lab.org/2020/ [3] https://cpachecker.sosy-lab.org/ https://cpachecker.sosy-lab.org/
      - fdupress 4y ago
        No, sorry; I'm not aware of proper comparisons for C verification tools, or at least recent and maintained tools. SV-COMP tends to propose a huge number of relatively simple tasks, which attracts model checkers and static analysers. Frama-C and VeriFast are functional verification tools. You can use them as static analysers, but there's a barrier to entry in terms of minimal required annotations that might not be present for tools designed for static analysis.
junon 4y ago
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.
chasil 4y ago
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 $
- markdascher 4y ago
  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/openssl.sh 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.
  - chasil 4y ago
    I will take a look tomorrow. I recently discovered exactly how unsafe PuTTY's "psftp -pw" option is (20+ years after introduction), so purging argv is always prudent. https://www.linuxjournal.com/content/putty-scripted-passwords-are-exposed-passwords https://www.linuxjournal.com/content/putty-scripted-password...
intelVISA 4y ago
Cool as heck. Frama-C is quite tempting, could you share any resources on how you got started w/ it?
- rwmj 4y ago
  Here's an engineering tech talk I did at Red Hat about Frama-C. It was an internal talk but I don't suppose anyone cares ... http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4 http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4 [134M, mp4]

naasking 4y ago

Cool, I've been meaning to try out Frama-C and other verification tools. Have you tried CBMC or similar tools at all?

markdascher 4y ago
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 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!
- fdupress 4y ago
  You could also try VeriFast [0], which is closer to Frama-C than CBMC. (VeriFast and Frama-C are deductive verification tools, CBMC is a bounded model checking tool.) It is slightly less approachable than Frama-C because it uses separation logic, but it's slightly more approachable because it uses symbolic execution, which allows it to display an actual execution trace that causes the failure. (You can then inspect that and decide whether your code or model is wrong.) [0]: https://github.com/verifast/verifast https://github.com/verifast/verifast
  - naasking 4y ago
    Good reference, I had actually starred that on github to refer to later and totally forgot about it. Do you know of a review of the various open source verification tools available for C? The ones I'm aware of: CBMC, Frama-C, VeriFast, ESBMC. I've found papers like [1] which benchmark various model checkers, but no evaluation of the verification effort required for the various approaches. Edit: the tutorial for VeriFast does not make it look very usable compared to Frama-C's ACSL language. Their tutorial doesn't explain a bunch of the syntax or why they made certain choices, so it all feels very unergonomic. Edit 2: The SV-COMP competition on software verification [2] tests a whole bunch of tools, but Frama-C and VeriFast are not among them. Looks like CPAChecker [3] has the best power-to-weight ratio if you're looking for one tool to learn with the most errors caught across all benchmarks. [1] https://arxiv.org/abs/2003.11689 https://arxiv.org/abs/2003.11689 [2] https://sv-comp.sosy-lab.org/2020/ https://sv-comp.sosy-lab.org/2020/ [3] https://cpachecker.sosy-lab.org/ https://cpachecker.sosy-lab.org/
    - fdupress 4y ago
      No, sorry; I'm not aware of proper comparisons for C verification tools, or at least recent and maintained tools. SV-COMP tends to propose a huge number of relatively simple tasks, which attracts model checkers and static analysers. Frama-C and VeriFast are functional verification tools. You can use them as static analysers, but there's a barrier to entry in terms of minimal required annotations that might not be present for tools designed for static analysis.

junon 4y ago

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.

chasil 4y ago

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 $

markdascher 4y ago
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/openssl.sh 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.
- chasil 4y ago
  I will take a look tomorrow. I recently discovered exactly how unsafe PuTTY's "psftp -pw" option is (20+ years after introduction), so purging argv is always prudent. https://www.linuxjournal.com/content/putty-scripted-passwords-are-exposed-passwords https://www.linuxjournal.com/content/putty-scripted-password...

intelVISA 4y ago

Cool as heck. Frama-C is quite tempting, could you share any resources on how you got started w/ it?

rwmj 4y ago
Here's an engineering tech talk I did at Red Hat about Frama-C. It was an internal talk but I don't suppose anyone cares ... http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4 http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4 [134M, mp4]