Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve code quality on modes of operation #80

Open
3 of 9 tasks
marsella opened this issue Jun 25, 2024 · 0 comments
Open
3 of 9 tasks

Improve code quality on modes of operation #80

marsella opened this issue Jun 25, 2024 · 0 comments
Labels
good first issue Good for newcomers improvement Addresses fixes or changes to existing specs

Comments

@marsella
Copy link
Contributor

marsella commented Jun 25, 2024

We have implementations of most of the modes of operations for block ciphers based on NIST 800-38A (and I think some subsequent publications) but they're not very formal. There are a couple things to do here.

On the presentation side:

  • these aren't literate specs. NIST is currently revising the modes of operation document 800-38A, but it's primarily focused on changing guidance and use cases. The updated recommendations for IVs and counter blocks might be relevant for us, but I think they will be more focused on how to choose those fields when encrypting a lot of items, which isn't something Cryptol can capture. It also incorporates some additional versions of CBC mode from an addendum into the spec, but we don't implement those right now. So, if we want to turn this into a literate spec, it's probably reasonable to use the current version of 800-38A as the basis.
  • The organization of this part of the module a little scattered. Key wrapping is not in the Modes directory and is instantiated just for AES, instead of generically(edit: I realized key wrap is an AES-only mode; see also Genericize key wrap modes of operation #81). Authenticated modes of operation are under Authenticated/ instead of Block/Modes/. Modes of operation are interspersed with instantiations and implementations for specific block ciphers. I think it would be nice to either update the organization or have a README pointing users to available ciphers and modes, briefly explaining what guarantees different modes get you (confidentiality, integrity, side-channel security...), and sharing which modes have been concretely instantiated for which block ciphers.

On the engineering side, there are several possible changes to make.

  • Currently, most of the modes of operation are defined in terms of a key size; each mode hand-writes the signature for the encrypt and decrypt methods for the block cipher that they'll be used with (others are implemented in terms of a specific block cipher, like AES256). It would be nice to have a more programmatic way to define the mode of operation generically over a block cipher, and then instantiate it for a given block cipher. There is a Cipher type that encodes the key size and type of the encryption/decryption methods which is sufficient for almost all modes of operation, except GCM-SIV. We should consider rewriting the modes in terms of Cipher, somehow.
  • There are many test vectors in NIST 800-38A that are not implemented. I noticed that CBC/CFB/CTR mode are only instantiated for AES128; there are more AES128 vectors to use for those as well as vectors for other sizes of AES that we could test. There may be others as well, I didn't look very carefully.

Related issue: #82

  • Refactor CBC mode to be parameterized by a CipherInterface
    • Refactor the test vectors to match the organization for CTR mode (instantiations in one directory, tests in another, consistent naming)
    • Add further test vectors
  • Refactor CFB mode to be parameterized by a CipherInterface
    • Refactor the test vectors to match the organization for CTR mode (instantiations in one directory, tests in another, consistent naming)
    • Add further test vectors
  • Improve variable naming in implementation of CTR mode to better match the spec: see CBC mode refactor/improvements #124 (comment) .
  • Decide whether other modes of operation are worth refactoring to use the CipherInterface and make follow-up issues
  • Decide which modes have a need to be literate and make follow-up issues
marsella added a commit that referenced this issue Jun 28, 2024
- Rewrite CTR mode to be in terms of the `CipherInterface`
- Update CTR mode to more closely match the original spec (naming,
  parameter order, etc.), and add docs for deviations
- Adds top-level documentation on deviations from the original spec and
  warnings for failure modes that cryptol cannot detect
- Rearranges instantiations and test vectors for AES (including adding
  more test vectors)
marsella added a commit that referenced this issue Jul 1, 2024
- Adds a type constraint that ensures messages are not so long that we'd
  reuse counters within a single encryption.
@mccleeary-galois mccleeary-galois added enhancement New feature or request good first issue Good for newcomers labels Aug 8, 2024
staslyakhov added a commit that referenced this issue Aug 26, 2024
The previous implementation of CBC (not yet removed) takes as input a
keysize and an encrypt/decrypt function, and hardcodes the IV and block
size to 128 bits.

Instead, we'd like to make use of CipherInterface, which makes it easier
to instantiate CBC with different block ciphers (and without any
hardcoded assumptions on the block size).

Removal of the old implementation and updating module-level comments is
reserved for future commits
staslyakhov added a commit that referenced this issue Aug 26, 2024
Further tests the new CipherInterface implementation of CBC
by instantiating it with AES128.

The instantiation can be imported from:
Primitive::Symmetric::Cipher::Block::Instantiations::AES128_CBC
staslyakhov added a commit that referenced this issue Aug 26, 2024
Now that we've established Modes/CBC.cry,
Instantiations/AES128_CBC.cry, and Tests/TestAES_CBC.cry as
the CBC implementation, instantiation, and testing, we can remove the
old implementations.
staslyakhov added a commit that referenced this issue Aug 26, 2024
Comment updated to follow format set throughout cryptol-specs.
staslyakhov added a commit that referenced this issue Aug 28, 2024
* Mention Appendix D that discusses what can go wrong if the IV is
  predictable.
* Emphasize that cryptol cannot check that IVs were generated correctly.
staslyakhov added a commit that referenced this issue Aug 28, 2024
* Match variable capitalization
* Use C_j_1 instead of c' to refer to $C_{j-1}$
@marsella marsella added improvement Addresses fixes or changes to existing specs and removed enhancement New feature or request labels Aug 29, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
good first issue Good for newcomers improvement Addresses fixes or changes to existing specs
Projects
None yet
Development

No branches or pull requests

2 participants