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.

Sign up for GitHub

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

Jump to bottom

Refactor AES spec to meet "gold standard" requirements #77

Closed
8 tasks done
marsella opened this issue Jun 18, 2024 · 0 comments · Fixed by #92
Closed
8 tasks done

Refactor AES spec to meet "gold standard" requirements #77

marsella opened this issue Jun 18, 2024 · 0 comments · Fixed by #92
Assignees
@marsella

Comments

@marsella
Copy link
Contributor

marsella commented Jun 18, 2024 •
edited
Loading

The current AES spec doesn't quite meet the gold standard that we'd like to see for important cryptol specs. This concerns just "plain" AES -- the block cipher itself, not any modes of operation layered on top of it -- as described in FIPS-197.

Here are the tasks I'm pretty sure need to happen:

  • Convert to literate Cryptol -- determine whether we have access to a latex file of the spec -- EDIT: moved this to Convert AES to a literate spec #91
  • Update module structure to compile all the allowable key sizes by default (a la Kyber)
    • Uncomment all the test vectors for all the key sizes -- put them in each module
  • Determine whether any other aspects of the structure of the module needs to change to better match the spec
  • Double-check that every data type and function described in the spec has a cryptol corollary
  • Make sure every property in the spec has an equivalent cryptol property
  • Add a batch file to prove or check every property -- done as of Fix docstrings for AES & friends #105
  • Re-review the gold standard and determine whether anything else needs to change.
This was referenced Jun 21, 2024
Closed
Merged
@marsella marsella self-assigned this Jun 21, 2024
marsella added a commit that referenced this issue Jun 21, 2024
@marsella
aes: add first attempt of refactor #77
81cc5c0
marsella added a commit that referenced this issue Jun 24, 2024
@marsella
aes: add explicit parameterizations of aes #77
d4a94d9 
this also refactors ctr mode
marsella added a commit that referenced this issue Jun 24, 2024
@marsella
aes: use explicit AES in cbc, cfb, ctr modes #77
548ac2a
marsella added a commit that referenced this issue Jun 24, 2024
@marsella
aes: use explicit AES in gcm and gcm-siv mode #77
a074359
marsella added a commit that referenced this issue Jun 24, 2024
@marsella
aes: remove aes_parameterized version #77
5b7ca52 
This has been fully replaced by the explicit parameterizations of AES
(AES128, AES256) in the internal codebase
marsella added a commit that referenced this issue Jun 24, 2024
@marsella
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!
marsella added a commit that referenced this issue Jun 24, 2024
@marsella
aes: use explicit params in cbc, cfb, ctr mode #77
6b1af4b
marsella added a commit that referenced this issue Jun 24, 2024
@marsella
aes: use explicit AES in gcm and gcm-siv mode #77
8c14010
marsella added a commit that referenced this issue Jun 24, 2024
@marsella
aes: remove aes_parameterized version #77
7718abf 
This has been fully replaced by the explicit parameterizations of AES
(AES128, AES256) in the internal codebase
marsella added a commit that referenced this issue Jun 24, 2024
@marsella
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
marsella added a commit that referenced this issue Jun 24, 2024
@marsella
aes: add concrete instantiation for AES-192 #77
9e1b9a0
marsella added a commit that referenced this issue Jun 24, 2024
@marsella
aes: add basic test vector for 128, 192 #77
c46fa18
marsella added a commit that referenced this issue Jun 24, 2024
@marsella
aes: replace duplicate AES.cry with AES256 #77
0244aa4 
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 added a commit that referenced this issue Jun 26, 2024
@marsella
aes: update KeySize definition, accessibility #77
6430913 
- 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)
marsella added a commit that referenced this issue Jun 26, 2024
@marsella
aes: add migration guide for aes API changes #77
4280f7e
marsella added a commit that referenced this issue Jun 26, 2024
@marsella
aes: add migration guide for aes API changes #77
d736d81
marsella added a commit that referenced this issue Jul 5, 2024
@marsella
gf28 WIP: modify naming in GF28 module #77
ffd374d
marsella added a commit that referenced this issue Jul 5, 2024
@marsella
gf28: update GF28 module to match spec #77
9d96268 
- modifies the order a little bit
- adds documentation, esp. references to where things live in the spec.
marsella added a commit that referenced this issue Jul 5, 2024
@marsella
gf28: update GF28 module to match spec #77
9abaa08 
- modify naming and call sites
- modifies the order a little bit
- adds documentation, esp. references to where things live in the spec.
marsella added a commit that referenced this issue Jul 8, 2024
@marsella
aes: add decryption to test vectors #77
03980cb 
We could always check the correctness properties too, but I added an
explicit check of the decryption method to each set of test vectors.
marsella added a commit that referenced this issue Jul 8, 2024
@marsella
aes: improve top-level naming and params #77
9edf059 
- Updates AES::Algorithm to use more spec-conformant names and improve
  documentation
- Fixes a bug in key expansion for decryption and simplify associated
  APIs
- Removes unnecssary parameterization in AES::Algorithm
marsella added a commit that referenced this issue Jul 9, 2024
@marsella
gf28: update GF28 module to match spec #77
114d5ad 
- modify naming and call sites
- modifies the order a little bit
- adds documentation, esp. references to where things live in the spec.
marsella added a commit that referenced this issue Jul 9, 2024
@marsella
aes: add decryption to test vectors #77
8fd1faa 
We could always check the correctness properties too, but I added an
explicit check of the decryption method to each set of test vectors.
marsella added a commit that referenced this issue Jul 9, 2024
@marsella
aes: improve top-level naming and params #77
a9ba10b 
- Updates AES::Algorithm to use more spec-conformant names and improve
  documentation
- Fixes a bug in key expansion for decryption and simplify associated
  APIs
- Removes unnecssary parameterization in AES::Algorithm
marsella added a commit that referenced this issue Jul 10, 2024
@marsella
aes: expand docs and properties #77
249414d
marsella added a commit that referenced this issue Jul 12, 2024
@marsella
aes: simplify s-box implementationa #77
7aed5de
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: clean up key expansion notation #77
a9fc967
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: improve state documentation #77
03df7c8
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: fix copyright notices #77
3cd6557
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
gf28: update GF28 module to match spec #77
32b2b1c 
- modify naming and call sites
- modifies the order a little bit
- adds documentation, esp. references to where things live in the spec.
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: add decryption to test vectors #77
845f618 
We could always check the correctness properties too, but I added an
explicit check of the decryption method to each set of test vectors.
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: improve top-level naming and params #77
1ce19cc 
- Updates AES::Algorithm to use more spec-conformant names and improve
  documentation
- Fixes a bug in key expansion for decryption and simplify associated
  APIs
- Removes unnecssary parameterization in AES::Algorithm
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: expand docs and properties #77
5e5d01d
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: simplify s-box implementationa #77
fd9a3f1
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: clean up key expansion notation #77
e334f6d
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: improve state documentation #77
c33c012
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: fix copyright notices #77
d6a55c8
@marsella marsella mentioned this issue Jul 15, 2024
Merged
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: add copyright notices #77
a21a863 
also fix the spelling of Nichole's name.
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
gf28: update GF28 module to match spec #77
ba34f2a 
- modify naming and call sites
- modifies the order a little bit
- adds documentation, esp. references to where things live in the spec.
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: add decryption to test vectors #77
2da773c 
We could always check the correctness properties too, but I added an
explicit check of the decryption method to each set of test vectors.
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: improve top-level naming and params #77
85fa6e5 
- Updates AES::Algorithm to use more spec-conformant names and improve
  documentation
- Fixes a bug in key expansion for decryption and simplify associated
  APIs
- Removes unnecssary parameterization in AES::Algorithm
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: expand docs and properties #77
a89a99d
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: simplify s-box implementationa #77
977a650
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: clean up key expansion notation #77
d12ffe9
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: improve state documentation #77
2843693
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: fix copyright notices #77
022e158
marsella added a commit that referenced this issue Jul 15, 2024
@marsella
aes: add copyright notices #77
5eaab4f 
also fix the spelling of Nichole's name.
marsella added a commit that referenced this issue Jul 17, 2024
@marsella
aes: consolidate AES main functions #77
d7a2692 
Removes the `Round` module and some extraneous names that aren't in the
spec and don't add a significant amount of clarity.
marsella added a commit that referenced this issue Jul 17, 2024
@marsella
aes: add code fences to property checking #77
b1c89c2 
Adds an explicit demo of how to prove / check each property
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@marsella marsella

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Bring AES closer in line with gold standard GaloisInc/cryptol-specs
1 participant
@marsella