Simplify AES module structure #79

marsella · 2024-06-24T16:21:20Z

This addresses some duplication in the AES specifications. Previously, there was a version that was concretely parameterized to be AES256 and a version with a top-level type constraint that could be parameterized to any of AES-128, -192, or -256 (and maybe others as well, I am not totally clear whether it was explicit about the upper bound). This PR does the following:

Converts the parameterizable version to a functor called AES_specification.cry to match a precedent set elsewhere in the repo (see Kyber). It was formerly AES_parameterized.cry
Adds three concrete instantiations of the functor version for the three allowable key sizes, and adds a minimal test vector for each (AES128.cry, AES192.cry, and AES256.cry)
Replaces all uses of the concretely parameterized version (AES.cry) with the AES256 instantiation of the functor, and removes the (now duplicate) concretely parameterized version.
- One or two specs used AES.cry but expected a 128-bit key, so I put in the correct version there.
Updated the implementations of the modes of operation. Previously, these were just some test vectors that implicitly instantiated AES128. I added explicit functions to each AES-instantiated mode of operation and made it clearer what key size they're using.

This does not preserve any kind of backwards compatibility. @RyanGlScott suggested a migration guide to using the new APIs, which I have not produced yet. My main blocker is that I'm not sure how to write modules that operate over AES (of any key size). E.g. I'd want to write them with respect to AES_specification but require you to pick a key size before you can use them.

I welcome feedback across the board: naming and style conventions, architecture review, type constraint design, cryptographic correctness. I am least concerned about the latter, since this does not introduce any new cryptography, just rearranges what was already there. The diff is fairly large, but I tried to keep my commits coherent if you would prefer to review them one by one.

I noted several possible follow-up issues inline. Another few are:

The modes of operation are written in terms of functions (the block cipher type signature). These should probably be updated to be functors¹ parameterized over the nice Cipher type, which defines the encrypt / decrypt functions. This would hopefully enforce the reality of modes of operation, which is that they are meaningless without an appropriate block cipher to bring them to life.
There are two AES-GCM implementations. These can hopefully be deduplicated, perhaps in Update AES-GCM to meet "gold standard" requirements #78.
The modes of operation instantiated with AES (of all sizes) are missing many test vectors that exist in their specifications.

I have acquired one hammer and every file is a nail now. ↩

- Creates a new specification functor that's generic over the key size - Instantiates it for AES 128 and 256 - Adds one test vector; more to come!

This has been fully replaced by the explicit parameterizations of AES (AES128, AES256) introduced in 53d6e68 in the internal codebase

Previously, the AES.cry file was not super explicit about the fact that it was parameterized only for AES 256. Now that we have concrete instantiations for the three allowable key sizes, use them explicitly. I locally spot-checked test vectors and properties where I could find them to make sure that this didn't break anything. There are some instances (key wrap) that use a specific key size for AES, but which should actually support arbitrary key sizes. This will be addressed separately. This maintains the status quo, since these implementations previously did not actually support arbitrary key sizes. Also, fixes a bug in DRBG, which was hard-coded to use AES128 but had accidentally been switched to AES256 and broke.

marsella · 2024-06-24T17:02:30Z

Primitive/Symmetric/Cipher/Block/AES_specification.cry

+parameter
+   type m : #
+   type constraint (fin m, m <= 2)
+
+type AesKeySize = 64 * (m + 2)


question: I was trying to come up with a way to set the key size as the parameter instead of m (which we still need in order to set a bunch of other parameters) but couldn't get the inference to do what I wanted. The reason for doing so would be so that the parameterized modules are more obvious -- it's not clear why "m=1" means AES-192. The argument for not bothering is that there are only 3 instances and I put documentation in there already.

When I (most recently) specified this I used:

/** * This constraint enforces the standard key sizes of 128, 192, and * 256-bits [FIPS-PUB-197 Sections 1, 5, and 6.1]. */ type constraint Key k = (fin k, k % 64 == 0, k / 64 >= 2, k / 64 <= 4)

This allowed me to keep the key size as a type. So, we get functions typed like this:

KeyExpansion : {k} (Key k) => [k] -> [Nr k + 1]Block

and

Cipher : {k} (Key k) => [Nr k + 1]Block -> Block -> Block

Thanks, this definitely makes the API nicer to use!

Primitive/Symmetric/Cipher/Block/AES128.cry

Primitive/Symmetric/Cipher/Block/AES_specification.cry

marsella · 2024-06-24T17:13:35Z

Primitive/Symmetric/Cipher/Authenticated/AES_GCM_SIV.cry

note: I constrained AES-GCM-SIV to just use AES256, which is effectively what it was doing before (due to the type constraint below). I think a nicer option would be to write GCM-SIV in terms of a Cipher parameter and instantiate it with AES128 and 256.

I also don't think this works right now; I tried dropping a test vector in but it didn't work in either the before or after version and I chose not to spend much time debugging right now. There are some weird constraints here (for example, the RFC allows the associated data to be 0-64 bytes long; here it's restricted to a minimum of 44 bytes?). I think all of this is better suited to a separate issue, which I'm happy to write up. This work does not make anything worse, at least.

On second look, I misread the comparison in L22. This previously supported both AES versions, but now it only supports one. I'll take another pass and try to fix it.

Fixed the supporting-multiple-keys issue in 6430913.

For the test vectors not working issue, I made a note in #82.

marsella · 2024-06-24T17:20:18Z

Primitive/Symmetric/Cipher/Block/AESKeyWrap.cry

+// One important deviation: this is currently instantiated only for AES256;
+// the RFC supports all three standardized AES key sizes.


note: this and the padded version should both be generalized over any AES key size. I am not exactly sure of the right architecture to do that -- would we write this as a functor with the same parameter as in AES_parameterized? Or like a Cipher? Or maybe something else.

In any case, this currently maintains the status quo of only instantiating it for AES256. I can write a separate issue to parameterize this to match the spec if we think it's worth having that recorded.

Lets log an issue for this to not lose it.

marsella · 2024-06-24T17:28:31Z

Primitive/Symmetric/Cipher/Block/AES_specification.cry

note: This is mostly not new; it's almost identical to the old AES_parameterized.cry except I added a parameter m and changed the definitions of EncKey and DecKey.

marsella · 2024-06-24T17:36:18Z

Primitive/Symmetric/Cipher/Block/Modes/AES128_CBC.cry

+AES128_CBC_encrypt: {n} (fin n) => [AES128::AesKeySize] -> iv -> [n]block -> [n]block
+AES128_CBC_encrypt = cbcEnc AES128::encrypt
+
+AES128_CBC_decrypt: {n} (fin n) => [AES128::AesKeySize] -> iv -> [n]block -> [n]block
+AES128_CBC_decrypt = cbcDec AES128::decrypt


note: this is the only thing I added to this file -- concrete names for "cbc mode using AES128." The test vectors are reformatted but the same content as in the old AES_CBC.cry.

marsella · 2024-06-24T17:37:03Z

Primitive/Symmetric/Cipher/Block/Modes/AES128_CFB.cry

+AES128_CFB_encrypt: {n} (fin n) => [AES128::AesKeySize] -> iv -> [n]block -> [n]block
+AES128_CFB_encrypt = cfbEnc AES128::encrypt
+
+AES128_CFB_decrypt: {n} (fin n) => [AES128::AesKeySize] -> iv -> [n]block -> [n]block
+AES128_CFB_decrypt = cfbDec AES128::decrypt


note: ditto here - this is the only new thing in this file compared to AES_CFB.cry.

marsella · 2024-06-24T17:37:24Z

Primitive/Symmetric/Cipher/Block/Modes/AES128_CTR.cry

+AES128_CTR_encrypt: {n} (fin n) => [AES128::AesKeySize] -> ic -> [n]block -> [n]block
+AES128_CTR_encrypt = ctrEnc AES128::encrypt
+
+AES128_CTR_decrypt: {n} (fin n) => [AES128::AesKeySize] -> ic -> [n]block -> [n]block
+AES128_CTR_decrypt = ctrDec AES128::decrypt


note: ditto here - this is the only thing new in this file compared to AES_CTR.cry.

marsella · 2024-06-24T17:38:10Z

Primitive/Symmetric/Cipher/Block/Tests/TestAES.cry

+ * Test vectors for AES256
+ * I don't actually know where these are sourced from.


note: These test vectors previously lived in AES.cry; the 128- and 192-bit ones were commented out.

marsella · 2024-06-25T14:53:24Z

I added #80 with some of the comments on block ciphers.

mccleeary-galois

Overall looks like a good step in the right direction! Thanks for doing this @marsella. I think we should try and get the migration guide in and ensure we have the follow on tickets logged but happy with approving this.

Primitive/Symmetric/Cipher/Block/AES128.cry

mccleeary-galois · 2024-06-25T14:21:08Z

Primitive/Symmetric/Cipher/Block/AESKeyWrap.cry

+// One important deviation: this is currently instantiated only for AES256;
+// the RFC supports all three standardized AES key sizes.


Lets log an issue for this to not lose it.

Primitive/Symmetric/Cipher/Block/AES_specification.cry

- For human-readability, updates the type constraint on AES to be the key size, not the mode - Makes `KeySize` a public type on the AES spec and replaces references to AesKeySize - Updates AES-GCM-SIV to support multiple key sizes (fixing a bug intorduced in 8c14010)

weaversa · 2024-06-27T14:47:12Z

Primitive/Symmetric/Cipher/Block/AES_specification.cry

+type Mode = (KeySize / 64) - 2
+
+// Make KeySize accessible outside the module.
+type KeySize = KeySize'


I do this all the time too...Is there a more elegant way to get access to parameters?

I'll ask on our internal channels!

There is not a more elegant way! The parameter blocks are anonymous interface modules that are then imported into the named module. But the module system does not automatically export things you've imported, so we have to do it manually.

I'm a poor judge of "elegance", but ~~a modern~~ another approach is to specify a (sub)module for parameterizations whose values are intended to be reused. Then a user needing the parameter values could import the named (sub)module.

For a parameterized AES module that takes a KeySize parameter, an anonymous parameterization like

module Primitive::Symmetric::Cipher::Block::AES128 = Primitive::Symmetric::Cipher::Block::AES_specification where // This produces a key size of 128 type KeySize = 128

could be refactored to

module Primitive::Symmetric::Cipher::Block::AES128::Parameters where // This produces a key size of 128 type KeySize = 128

module Primitive::Symmetric::Cipher::Block::AES128 = Primitive::Symmetric::Cipher::Block::AES_specification { Primitive::Symmetric::Cipher::Block::AES128::Parameters }

import Primitive::Symmetric::Cipher::Block::AES128::Parameters (KeySize) import Primitive::Symmetric::Cipher::Block::AES128 (encrypt, decrypt)

This approach is a tradeoff -- it ~~is not supported in older Cryptol versions (<3.0),~~ requires another import to access an instantiation's parameter values, and at the module level clutters the filesystem, but it reduces redundancy.

A similar concept (for Cryptol 3.0+) applies to reusing parameter blocks by promoting them to named interface (sub)(module)s.

marsella added 7 commits June 24, 2024 10:26

aes: add concrete instantiations of AES #77

53d6e68

- Creates a new specification functor that's generic over the key size - Instantiates it for AES 128 and 256 - Adds one test vector; more to come!

aes: use explicit params in cbc, cfb, ctr mode #77

6b1af4b

aes: use explicit AES in gcm and gcm-siv mode #77

8c14010

aes: remove aes_parameterized version #77

302d249

This has been fully replaced by the explicit parameterizations of AES (AES128, AES256) introduced in 53d6e68 in the internal codebase

aes: add concrete instantiation for AES-192 #77

9e1b9a0

aes: add basic test vector for 128, 192 #77

c46fa18

marsella commented Jun 24, 2024

View reviewed changes

marsella requested a review from mccleeary-galois June 24, 2024 17:48

marsella marked this pull request as ready for review June 24, 2024 17:52

mccleeary-galois approved these changes Jun 25, 2024

View reviewed changes

marsella added 2 commits June 26, 2024 09:25

aes: add migration guide for aes API changes #77

d736d81

marsella force-pushed the 77-refactor-aes-modules branch from 4280f7e to d736d81 Compare June 26, 2024 14:34

marsella mentioned this pull request Jun 26, 2024

Genericize key wrap modes of operation #81

Closed

marsella merged commit 2e8d412 into master Jun 27, 2024

marsella deleted the 77-refactor-aes-modules branch June 27, 2024 14:43

weaversa reviewed Jun 27, 2024

View reviewed changes

WeeknightMVP mentioned this pull request Jul 3, 2024

Rexporting functor parameters in an instantiation GaloisInc/cryptol#1699

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Simplify AES module structure #79

Simplify AES module structure #79

marsella commented Jun 24, 2024 •

edited

Loading

marsella Jun 24, 2024

weaversa Jun 24, 2024

weaversa Jun 24, 2024

marsella Jun 26, 2024

marsella Jun 24, 2024

marsella Jun 25, 2024

marsella Jun 26, 2024

marsella Jun 24, 2024

mccleeary-galois Jun 25, 2024

marsella Jun 25, 2024

marsella Jun 24, 2024

marsella Jun 24, 2024

marsella Jun 24, 2024

marsella Jun 24, 2024

marsella Jun 24, 2024

marsella commented Jun 25, 2024

mccleeary-galois left a comment

mccleeary-galois Jun 25, 2024

weaversa Jun 27, 2024

marsella Jun 27, 2024

marsella Jun 28, 2024 •

edited

Loading

WeeknightMVP Jun 29, 2024 •

edited

Loading

		// One important deviation: this is currently instantiated only for AES256;
		// the RFC supports all three standardized AES key sizes.

		* Test vectors for AES256
		* I don't actually know where these are sourced from.

Simplify AES module structure #79

Simplify AES module structure #79

Conversation

marsella commented Jun 24, 2024 • edited Loading

Footnotes

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

marsella commented Jun 25, 2024

mccleeary-galois left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

marsella Jun 28, 2024 • edited Loading

Choose a reason for hiding this comment

WeeknightMVP Jun 29, 2024 • edited Loading

Choose a reason for hiding this comment

marsella commented Jun 24, 2024 •

edited

Loading

marsella Jun 28, 2024 •

edited

Loading

WeeknightMVP Jun 29, 2024 •

edited

Loading