AES-XTS Ciphertext_stealing safety proofs#367

Draft

nebeid wants to merge 136 commits into

awslabs:mainfrom

nebeid:aes-xts-safety

Commits on Dec 23, 2025

aes-xts experiments
pennyannn
committed
More experiments
pennyannn
committed
Add Decrypt function- its instructions are all understood by the decoder.

nebeid
authored and
pennyannn
committed
The decrypt version is now from linux-aarch64.

nebeid
authored and
pennyannn
committed
enable stopping at first error.

nebeid
authored and
pennyannn
committed
Save decoded output to a text file.

nebeid
authored and
pennyannn
committed
Update decoded output after adding post-index register offset to the decoder.

nebeid
authored and
pennyannn
committed
New decoded output after shuffling around some instructions.

nebeid
authored and
pennyannn
committed
Start proof for AES256 encrypt
pennyannn
committed
Continuing the AES specification.

nebeid
authored and
pennyannn
committed
The spec test vector succeeds after converting the inputs to little endian representation.

nebeid
authored and
pennyannn
committed
Post conditions and MAYCHANGE for an AES block encryption proof.

nebeid
authored and
pennyannn
committed
Proof of AES encryption of one block.

nebeid
authored and
pennyannn
committed
Add aes-xts decrypt programs
pennyannn
committed
Add aes program and spec
pennyannn
committed
Symbolic simulation and fixed a bug in code
pennyannn
committed
Finish the proof for aes-xts-decrypt
pennyannn
committed
Fix a bug
pennyannn
committed
Set up for aes-xts one block proof
pennyannn
committed
Define spec for one block xts and define conversion
pennyannn
committed
Add proof for one block xts
pennyannn
committed
Update one block proof to use more clean version
pennyannn
committed
WIP: define XTS full specification
pennyannn
committed
Experiment with conversions
pennyannn
committed
Fix type issue in cipher stealing
pennyannn
committed
Write conversions and add tests
pennyannn
committed
The ultimate clean up
pennyannn
committed
The ultimate ultimate clean up to fix perror
pennyannn
committed
Update the specification to match the standard for tweak calculation
pennyannn
committed
Update clean version of xts decrypt
pennyannn
committed
Add a structure for the proof
pennyannn
committed
Eliminating some CHEAT_TACs
pennyannn
committed
Eliminate more CHEAT_TACs and prove a bunch of lemmas
pennyannn
committed
Fixing MAYCHANGE and preserved registers
pennyannn
committed
WIP: proving main goal
pennyannn
committed
Simplify specification
pennyannn
committed
WIP: proving main goal
pennyannn
committed
Further simplify the spec
pennyannn
committed
WIP: proving main goal
pennyannn
committed
Update the spec
pennyannn
committed
WIP: prove main goal
pennyannn
committed
Revert "Update the spec"
pennyannn
committed
Finished: prove main goal
pennyannn
committed
WIP: prove tail
pennyannn
committed
Restructure proof to add a cut point before cipher stealing and finish up the invariant proof
pennyannn
committed
Update the program with respect to AWS-LC PR2734
pennyannn
committed
Finished: verify cipher stealing
pennyannn
committed
Tried to fix the non-overlapping issue
pennyannn
committed
Fixing some issues
pennyannn
committed
Prepare for bounded proofs
pennyannn
committed
Finished: bounded proofs
pennyannn
committed
Add the final subroutine theorem
pennyannn
committed
Thanks for John Harrison, cleaning up the last CHEAT_TAC
pennyannn
committed
More experiments
pennyannn
committed
One block of AES-256-XTS encrypt: Spec and a test vector (using conversions).

nebeid
authored and
pennyannn
committed
Adding new assembly for AES-XTS:

nebeid
authored and
pennyannn
committed
Proof of one-block AES-XTS encrypt.

nebeid
authored and
pennyannn
committed
AES-XTS encrypt (any input length) spec. To be tested

nebeid
authored and
pennyannn
committed
Make encrypt_spec match decrypt_spec.

nebeid
authored and
pennyannn
committed
Working through the conversions for AES-XTS encrypt test vector.

nebeid
authored and
pennyannn
committed
Fixed a bug in cipher_stealing_encrypt in the computation of the last tweak.

nebeid
authored and
pennyannn
committed
Completed AES-XTS Encrypt specs and their tests.

nebeid
authored and
pennyannn
committed
Use the asm code integrated in AWS-LC and redo the 1-block proof based on the new specs 1-block function.

nebeid
authored and
pennyannn
committed
WIP: full proof: - loop invariant, one subgoal proven. - proof of code before the loop started.

nebeid
authored and
pennyannn
committed
Moved udiv and second tweak operations to later, WIP: full proof; code before the loop proven

nebeid
authored and
pennyannn
committed
Update byte_list_at.

nebeid
authored and
pennyannn
committed
Update AES-XTS encrypt spec removing the byte list returned in case of error, matching the decrypt spec updates.

nebeid
authored and
pennyannn
committed
Subgoal 2 of the loop invariant proven.

nebeid
authored and
pennyannn
committed
Changed back bytes_to_int128 to its original definition.

nebeid
authored and
pennyannn
committed
WIP: subgoal 3 of the loop invariant.

nebeid
authored and
pennyannn
committed
WIP: subgoal 3 of the loop invariant, arrived at the inductive step.

nebeid
authored and
pennyannn
committed
WIP: subgoal 3 of the loop invariant, going through the inductive step.

nebeid
authored and
pennyannn
committed
WIP: subgoal 3 of the loop invariant, at the inductive step, reduced the goal by proving the last round in the loop (following the decrypt proof).

nebeid
authored and
pennyannn
committed
WIP: subgoal 3 of the loop invariant, at the inductive step, reduced the goal by proving the last 3 rounds in the loop (following the decrypt proof).

nebeid
authored and
pennyannn
committed
subgoal 3 of the loop invariant; the inductive step - DONE.

nebeid
authored and
pennyannn
committed
Subgoal 4 of main loop invariant: backedge is not taken until i = num_5blocks.

nebeid
authored and
pennyannn
committed
Assembly changes in cipher-stealing from AWS-LC PR2734 to avoid looping. Subgoal 5: WIP.

nebeid
authored and
pennyannn
committed
Subgoal 5: case len mod 0x50 = 0x40.

nebeid
authored and
pennyannn
committed
Subgoal 5: case len mod 0x50 = 0x30.

nebeid
authored and
pennyannn
committed
Subgoal 5: case len mod 0x50 = 0x20.

nebeid
authored and
pennyannn
committed
Subgoal 5: case len mod 0x50 = 0x10.

nebeid
authored and
pennyannn
committed
Subgoal 5: case len mod 0x50 = 0 (wip).

nebeid
authored and
pennyannn
committed
Subgoal 5: case len mod 0x50 = 0.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail = 0.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant up to subgoal 2.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant subgoal 3: WIP.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant back to subgoal 2: WIP.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant subgoal 2: done.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant subgoal 3: symbolic simulation.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant subgoal 3: symbolic simulation completed. Went back to subgoal 2.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant subgoal 3: symbolic simulation completed. Went back to subgoal 2, fix typos and an extra pre-condition.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant: Reworking subgoal 2 based on l1_curr_len, using the same cipher_stealing_inv as decrypt.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant: Reworking subgoal 2 (wip), needing a new lemma.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant: Subgoal 2: Done, pending a new lemma.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant: Subgoal 3: case i=3 working, now case i = 0 is wip. Subgoal 2 new lemma from Yan working

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant: Subgoal 3: complete.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant: Subgoal 4: complete.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant: Subgoal 5, wip.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant: Subgoal 5, wip (incomplete subgoals l. 3977 and l. 4485.

nebeid
authored and
pennyannn
committed
Cipher-stealing: case tail != 0, loop invariant: Subgoal 5, proved subgoals of previous commit.

nebeid
authored and
pennyannn
committed
Cipher-stealing: complete.

nebeid
authored and
pennyannn
committed
Less than 2 blocks: with the late W19 setting bug, assumptions are erased in symbolic simulation and cannot match them in TWEAK_TAC.

nebeid
authored and
pennyannn
committed
Less than 2 blocks: with the fix setting W19 before branching, no assumptions are erased in symbolic simulation and TWEAK_TAC succeeds.

nebeid
authored and
pennyannn
committed
Less than 2 blocks: proof done.

nebeid
authored and
pennyannn
committed
Less than 3 blocks: proof done.

nebeid
authored and
pennyannn
committed
Less than 4 blocks, less than 5 blocks: proofs done.

nebeid
authored and
pennyannn
committed
AES256-XTS encrypt proof: complete.

nebeid
authored and
pennyannn
committed
AES256-XTS encrypt proof including stack management: complete.

nebeid
authored and
pennyannn
committed
Adjust 1-block proof to the code after the W19 fix.

nebeid
authored and
pennyannn
committed
Use the updated tactic name.

nebeid
authored and
pennyannn
committed
Clean up Makefiles and rename files to keep consistency
pennyannn
committed
Refactor the structure of files
pennyannn
committed
Put AES encrypt and decrypt proofs in tutorial
pennyannn
committed
Integrate assembly
pennyannn
committed
Fix issue in collect-signatures
pennyannn
committed
Add benchmark for AES-XTS
pennyannn
committed
Fix missing sematest for ldrb shifted register variant
pennyannn
committed
Rename AES_KEY as s2n_bignum_AES_KEY
pennyannn
committed
Fix benchmark platform check
pennyannn
committed
Add sematest for strb shifted register no shift
pennyannn
committed
Update signature
pennyannn
committed
Rename aes_hw_xts_encrypt to aes_xts_encrypt and similarly for decrypt
pennyannn
committed

Commits on Jan 16, 2026

Commits on Jan 20, 2026

Commits on Jan 26, 2026

Commits on Feb 18, 2026

Merge branch 'main' into aes-xts
nebeid
authored

Commits on Feb 21, 2026

Prove CIPHER_STEALING_SAFE of aes-xts decrypt
aqjune-aws
committed

Commits on Mar 10, 2026

Prove CIPHER_STEALING_SAFE of aes-xts encrypt
nebeid
committed

Commits

Commits on Dec 23, 2025

Commits on Jan 16, 2026

Commits on Jan 20, 2026

Commits on Jan 21, 2026

Commits on Jan 22, 2026

Commits on Jan 23, 2026

Commits on Jan 26, 2026

Commits on Feb 18, 2026