diff --git a/CHANGELOG.md b/CHANGELOG.md index 08809a98c8..fc9d73f3cb 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -34,6 +34,7 @@ - Documented that enum variants are module-level constants and must be unique within a module ([#2932]((https://github.com/0xMiden/miden-vm/pull/2932)). - Refactor trace generation to row-major format ([#2937](https://github.com/0xMiden/miden-vm/pull/2937)). - Documented non-overlap requirement for `memcopy_words`, `memcopy_elements`, and AEAD encrypt/decrypt procedures ([#2941](https://github.com/0xMiden/miden-vm/pull/2941)). +- Aligned AEAD key/nonce stack-order documentation and handler comments with the runtime contract ([#3036](https://github.com/0xMiden/miden-vm/pull/3036)). - Added chainable `Test` builders for common test setup in `miden-utils-testing` ([#2957](https://github.com/0xMiden/miden-vm/pull/2957)). - Added fuzz coverage for package semantic deserialization and project parsing, loading, and assembly ([#3015](https://github.com/0xMiden/miden-vm/pull/3015)). - Speed-up AUX range check trace generation by changing divisors to a flat Vec layout ([#2966](https://github.com/0xMiden/miden-vm/pull/2966)). diff --git a/crates/lib/core/asm/crypto/aead.masm b/crates/lib/core/asm/crypto/aead.masm index 040c4cd6bd..7673f98cbb 100644 --- a/crates/lib/core/asm/crypto/aead.masm +++ b/crates/lib/core/asm/crypto/aead.masm @@ -34,14 +34,14 @@ const AEAD_DECRYPT_EVENT=event("miden::core::crypto::aead::decrypt") #! - rate(8) will contain the initial keystream #! - capacity(4) constains the capacity portion of the state proc init_state - # Stack: [nonce(4), key(4), ...] + # Stack: [key(4), nonce(4), ...] # Initialize capacity with all zeros padw - # => [cap(4), nonce(4), key(4), ...] + # => [cap(4), key(4), nonce(4), ...] movdnw.2 - # => [nonce(4), key(4), cap(4), ...] + # => [key(4), nonce(4), cap(4), ...] # Apply initial permutation to mix key and nonce hperm @@ -254,7 +254,7 @@ end #! Length: num_blocks * 8 elements #! The padding block is authenticated but not written to the plaintext output. #! -#! Event: Emits AEAD_DECRYPT event with (nonce, key, src_ptr, dst_ptr, num_blocks) +#! Event: Emits AEAD_DECRYPT event with (key, nonce, src_ptr, dst_ptr, num_blocks) #! The host event handler must: #! - Read full ciphertext from memory at src_ptr ((num_blocks + 1) * 8 elements) #! - Read authentication tag from memory at src_ptr + (num_blocks + 1) * 8 @@ -298,7 +298,7 @@ end #! - n = number of field elements in the plaintext (excludes the padding block) #! - For num_blocks data blocks: n = 8 * num_blocks pub proc decrypt - # Stack: [nonce(4), key(4), src_ptr, dst_ptr, num_blocks, ...] + # Stack: [key(4), nonce(4), src_ptr, dst_ptr, num_blocks, ...] # Input validation note: This procedure does not validate num_blocks or alignment. # Alignment errors are caught by the VM memory subsystem. Incorrect num_blocks @@ -319,31 +319,31 @@ pub proc decrypt dup.9 add movdn.11 - # => [nonce(4), key(4), src_ptr, dst_ptr, num_blocks, tag_ptr, ...] + # => [key(4), nonce(4), src_ptr, dst_ptr, num_blocks, tag_ptr, ...] # emit event to trigger host-side decryption # the event handler will push plaintext data blocks onto the advice stack emit.AEAD_DECRYPT_EVENT - # => [nonce(4), key(4), src_ptr, dst_ptr, num_blocks, tag_ptr, ...] + # => [key(4), nonce(4), src_ptr, dst_ptr, num_blocks, tag_ptr, ...] # advice stack now contains: plaintext data blocks (no padding) in reverse order compatible # with adv_pipe # prepare to load plaintext data blocks from advice stack dup.10 # num_blocks dup.10 # dst_ptr - # => [dst_ptr, num_blocks, nonce(4), key(4), src_ptr, dst_ptr, num_blocks, tag_ptr, ...] + # => [dst_ptr, num_blocks, key(4), nonce(4), src_ptr, dst_ptr, num_blocks, tag_ptr, ...] # setup for adv_pipe loop padw padw padw - # => [0(4), 0(4), 0(4), dst_ptr, num_blocks, nonce(4), key(4), src_ptr, dst_ptr, num_blocks, tag_ptr, ...] + # => [0(4), 0(4), 0(4), dst_ptr, num_blocks, key(4), nonce(4), src_ptr, dst_ptr, num_blocks, tag_ptr, ...] dup.13 neq.0 - # => [continue?, 0(4), 0(4), 0(4), dst_ptr, num_blocks, nonce(4), ...] + # => [continue?, 0(4), 0(4), 0(4), dst_ptr, num_blocks, key(4), ...] # load plaintext data blocks from advice stack while.true adv_pipe # reads 8 elements from advice, writes to dst_ptr, increments dst_ptr by 8 - # => [DATA1(4), DATA0(4), 0(4), dst_ptr+8, num_blocks, nonce(4), key(4), src_ptr, dst_ptr, num_blocks, tag_ptr, ...] + # => [DATA1(4), DATA0(4), 0(4), dst_ptr+8, num_blocks, key(4), nonce(4), src_ptr, dst_ptr, num_blocks, tag_ptr, ...] movup.13 sub.1 # duplicate counter, decrement it dup movdn.14 # duplicate and move decremented value down to overwrite old counter @@ -352,14 +352,14 @@ pub proc decrypt # clean up adv_pipe working area dropw dropw dropw - # => [dst_ptr_final, 0, nonce(4), key(4), src_ptr, dst_ptr, num_blocks, tag_ptr, ...] + # => [dst_ptr_final, 0, key(4), nonce(4), src_ptr, dst_ptr, num_blocks, tag_ptr, ...] drop drop - # => [nonce(4), key(4), src_ptr, dst_ptr, num_blocks, tag_ptr, ...] + # => [key(4), nonce(4), src_ptr, dst_ptr, num_blocks, tag_ptr, ...] # swap src_ptr and dst_ptr to call encrypt on the plaintext # this will re-encrypt the data blocks (adding padding automatically) to compute tag movup.9 movup.9 swap movdn.9 movdn.9 - # => [nonce(4), key(4), dst_ptr, src_ptr, num_blocks, tag_ptr, ...] + # => [key(4), nonce(4), dst_ptr, src_ptr, num_blocks, tag_ptr, ...] # re-encrypt plaintext to compute authentication tag exec.encrypt diff --git a/crates/lib/core/docs/crypto/aead.md b/crates/lib/core/docs/crypto/aead.md index e23d27e6ec..1dcc6bbfa0 100644 --- a/crates/lib/core/docs/crypto/aead.md +++ b/crates/lib/core/docs/crypto/aead.md @@ -5,4 +5,4 @@ AEAD (Authenticated Encryption with Associated Data) implementation using Poseid | Procedure | Description | | ----------- | ------------- | | encrypt | Encrypts plaintext data from memory using the `crypto_stream` instruction.

This procedure encrypts plaintext and automatically includes a padding block at the end.
The padding block [1, 0, 0, 0, 0, 0, 0, 0] is encrypted without requiring the caller
to write padding into the plaintext buffer manually.
This, however, requires the plaintext length to be a multiple of 8. This assumption is made
both in this procedure as well as in the decryption procedure.

Input: [key(4), nonce(4), src_ptr, dst_ptr, num_blocks, ...]
Output: [tag(4), ...]

Where:
- key is the encryption key (4 elements)
- nonce is the initialization vector (4 elements)
- src_ptr points to plaintext in memory (must be word-aligned)
- dst_ptr points to where ciphertext will be written (must be word-aligned)
- num_blocks is the number of 8-element plaintext data blocks (NO padding included)
- tag is the authentication tag returned on stack (4 elements)

Memory Layout:
- Input at src_ptr: [plaintext_block_0(8), ..., plaintext_block_n(8)]
Length: num_blocks * 8 elements (must be multiple of 8)

- Output at dst_ptr: [ciphertext_block_0(8), ..., ciphertext_block_n(8), encrypted_padding(8)]
Length: (num_blocks + 1) * 8 elements
The padding block is automatically added and encrypted

- Standard format: the tag is stored right after ciphertext to create:
[ciphertext_blocks(num_blocks * 8), encrypted_padding(8), tag(4)]
Tag location: dst_ptr + (num_blocks + 1) * 8

Memory Requirements:
- Plaintext must be at word-aligned addresses (addr % 4 == 0)
- Each block is 8 field elements (2 words)
- Blocks must be stored contiguously in memory

# Panics

Panics if the source and destination memory ranges overlap
(in-place encryption not supported).

Padding:
- Padding is AUTOMATIC - caller should NOT pad the plaintext
- The procedure writes encrypted padding to dst_ptr + (num_blocks * 8)
- The plaintext buffer is not modified
- For empty plaintext (num_blocks = 0), only the padding block is encrypted

Cycles (estimate): 77 + 2 * n
Where:
- n = number of field elements encrypted (includes the final padding block)
- For num_blocks data blocks: n = 8 * (num_blocks + 1)
| -| decrypt | Decrypts and authenticates ciphertext using non-deterministic advice.

This procedure implements AEAD decryption with automatic tag verification. It mirrors
the encrypt procedure's padding behavior while leaving the plaintext output unpadded.

Decryption Flow:
1. Computes tag location: src_ptr + (num_blocks + 1) * 8
2. Emits event for host to decrypt ciphertext (data blocks + padding block)
3. Loads plaintext data blocks from advice into dst_ptr (num_blocks * 8 elements)
4. Calls encrypt which reads data blocks and adds padding automatically
5. Re-encrypts data + padding to compute authentication tag
6. Compares computed tag with tag from memory at src_ptr + (num_blocks + 1) * 8
7. Halts execution with assertion failure if tags don't match

Input: [key(4), nonce(4), src_ptr, dst_ptr, num_blocks, ...]
Output: [] (empty stack on success, halts on failure)

Where:
- key is the decryption key (4 elements)
- nonce is the initialization vector (4 elements)
- src_ptr points to ciphertext + encrypted_padding + tag in memory (word-aligned)
- dst_ptr points to where plaintext will be written (word-aligned)
- num_blocks is the number of 8-element plaintext data blocks (NO padding)

Memory Layout:
- Input at src_ptr: [ciphertext_blocks(num_blocks * 8), encrypted_padding(8), tag(4)]
The encrypted padding is at: src_ptr + (num_blocks * 8)
The tag is at: src_ptr + (num_blocks + 1) * 8

- Output at dst_ptr: [plaintext_block_0(8), ..., plaintext_block_n(8)]
Length: num_blocks * 8 elements
The padding block is authenticated but not written to the plaintext output.

Event: Emits AEAD_DECRYPT event with (nonce, key, src_ptr, dst_ptr, num_blocks)
The host event handler must:
- Read full ciphertext from memory at src_ptr ((num_blocks + 1) * 8 elements)
- Read authentication tag from memory at src_ptr + (num_blocks + 1) * 8
- Decrypt and verify tag using reference implementation
- Extract only data blocks (first num_blocks * 8 elements) from decrypted plaintext
- Insert data blocks (WITHOUT padding) into advice map (keyed by nonce)

Memory Requirements:
- Same as encrypt: word-aligned addresses, contiguous blocks

# Panics

Panics if the source and destination memory ranges overlap
(in-place decryption not supported).

Security:
- Tag verification happens in the MASM procedure via re-encryption
- Execution halts with assertion failure if tag verification fails
- If execution completes successfully, the plaintext at dst_ptr is authenticated

Non-Determinism Soundness:
This procedure uses non-deterministic advice to obtain the plaintext, which is sound
because:
1. The prover provides claimed plaintext via advice (untrusted input)
2. This procedure re-encrypts the claimed plaintext with the same (key, nonce)
3. Due to deterministic encryption, the same plaintext produces the same ciphertext
4. The computed tag cryptographically commits to both plaintext and ciphertext
5. Comparing tags verifies that the claimed plaintext is the unique plaintext that
encrypts to the given ciphertext under the given (key, nonce)

This approach is secure because:
- The MASM procedure verifies the tag when calling the encryption procedure
- The tag acts as a cryptographic commitment
- The deterministic keystream creates a bijection between plaintext and ciphertext
- Any deviation from correct plaintext causes assertion failure

Note: This procedure does not write the padding block to the plaintext output.

Cycles (estimate): 177 + 3.5 * n
Where:
- n = number of field elements in the plaintext (excludes the padding block)
- For num_blocks data blocks: n = 8 * num_blocks
| +| decrypt | Decrypts and authenticates ciphertext using non-deterministic advice.

This procedure implements AEAD decryption with automatic tag verification. It mirrors
the encrypt procedure's padding behavior while leaving the plaintext output unpadded.

Decryption Flow:
1. Computes tag location: src_ptr + (num_blocks + 1) * 8
2. Emits event for host to decrypt ciphertext (data blocks + padding block)
3. Loads plaintext data blocks from advice into dst_ptr (num_blocks * 8 elements)
4. Calls encrypt which reads data blocks and adds padding automatically
5. Re-encrypts data + padding to compute authentication tag
6. Compares computed tag with tag from memory at src_ptr + (num_blocks + 1) * 8
7. Halts execution with assertion failure if tags don't match

Input: [key(4), nonce(4), src_ptr, dst_ptr, num_blocks, ...]
Output: [] (empty stack on success, halts on failure)

Where:
- key is the decryption key (4 elements)
- nonce is the initialization vector (4 elements)
- src_ptr points to ciphertext + encrypted_padding + tag in memory (word-aligned)
- dst_ptr points to where plaintext will be written (word-aligned)
- num_blocks is the number of 8-element plaintext data blocks (NO padding)

Memory Layout:
- Input at src_ptr: [ciphertext_blocks(num_blocks * 8), encrypted_padding(8), tag(4)]
The encrypted padding is at: src_ptr + (num_blocks * 8)
The tag is at: src_ptr + (num_blocks + 1) * 8

- Output at dst_ptr: [plaintext_block_0(8), ..., plaintext_block_n(8)]
Length: num_blocks * 8 elements
The padding block is authenticated but not written to the plaintext output.

Event: Emits AEAD_DECRYPT event with (key, nonce, src_ptr, dst_ptr, num_blocks)
The host event handler must:
- Read full ciphertext from memory at src_ptr ((num_blocks + 1) * 8 elements)
- Read authentication tag from memory at src_ptr + (num_blocks + 1) * 8
- Decrypt and verify tag using reference implementation
- Extract only data blocks (first num_blocks * 8 elements) from decrypted plaintext
- Insert data blocks (WITHOUT padding) into advice map (keyed by nonce)

Memory Requirements:
- Same as encrypt: word-aligned addresses, contiguous blocks

# Panics

Panics if the source and destination memory ranges overlap
(in-place decryption not supported).

Security:
- Tag verification happens in the MASM procedure via re-encryption
- Execution halts with assertion failure if tag verification fails
- If execution completes successfully, the plaintext at dst_ptr is authenticated

Non-Determinism Soundness:
This procedure uses non-deterministic advice to obtain the plaintext, which is sound
because:
1. The prover provides claimed plaintext via advice (untrusted input)
2. This procedure re-encrypts the claimed plaintext with the same (key, nonce)
3. Due to deterministic encryption, the same plaintext produces the same ciphertext
4. The computed tag cryptographically commits to both plaintext and ciphertext
5. Comparing tags verifies that the claimed plaintext is the unique plaintext that
encrypts to the given ciphertext under the given (key, nonce)

This approach is secure because:
- The MASM procedure verifies the tag when calling the encryption procedure
- The tag acts as a cryptographic commitment
- The deterministic keystream creates a bijection between plaintext and ciphertext
- Any deviation from correct plaintext causes assertion failure

Note: This procedure does not write the padding block to the plaintext output.

Cycles (estimate): 177 + 3.5 * n
Where:
- n = number of field elements in the plaintext (excludes the padding block)
- For num_blocks data blocks: n = 8 * num_blocks
| diff --git a/crates/lib/core/src/handlers/aead_decrypt.rs b/crates/lib/core/src/handlers/aead_decrypt.rs index 39480215a4..242954845b 100644 --- a/crates/lib/core/src/handlers/aead_decrypt.rs +++ b/crates/lib/core/src/handlers/aead_decrypt.rs @@ -32,6 +32,9 @@ pub const AEAD_DECRYPT_EVENT_NAME: EventName = EventName::new("miden::core::cryp /// 4. Extracts only the data blocks (first num_blocks * 8 elements) from plaintext /// 5. Pushes the data blocks (WITHOUT padding) onto the advice stack in reverse order /// +/// Expected event payload order (excluding event id): +/// `(key: Word, nonce: Word, src_ptr, dst_ptr, num_blocks)`. +/// /// Memory layout at src_ptr: /// - [ciphertext_blocks(num_blocks * 8), encrypted_padding(8), tag(4)] /// - This handler reads ALL elements: data blocks + padding + tag @@ -48,7 +51,7 @@ pub const AEAD_DECRYPT_EVENT_NAME: EventName = EventName::new("miden::core::cryp /// 2. The deterministic encryption creates a bijection between plaintext and ciphertext /// 3. A malicious prover cannot provide incorrect plaintext without causing tag mismatch pub fn handle_aead_decrypt(process: &ProcessorState) -> Result, EventError> { - // Stack: [event_id, key(4), nonce(4), src_ptr, dst_ptr, num_blocks, ...] + // Stack: [event_id, key:Word(4), nonce:Word(4), src_ptr, dst_ptr, num_blocks, ...] // where: // src_ptr = ciphertext + encrypted_padding + tag location (input) // dst_ptr = plaintext destination (output) diff --git a/docs/src/user_docs/core_lib/crypto/aead.md b/docs/src/user_docs/core_lib/crypto/aead.md index c21606cb19..587222d312 100644 --- a/docs/src/user_docs/core_lib/crypto/aead.md +++ b/docs/src/user_docs/core_lib/crypto/aead.md @@ -29,14 +29,14 @@ Associated data (AD) is currently **not supported**. Only empty AD is handled, w Encrypts plaintext data from memory using the `crypto_stream` instruction. This procedure encrypts plaintext and automatically adds a padding block at the end. **Inputs:** -- Operand stack: `[nonce(4), key(4), src_ptr, dst_ptr, num_blocks, ...]` +- Operand stack: `[key(4), nonce(4), src_ptr, dst_ptr, num_blocks, ...]` **Outputs:** - Operand stack: `[tag(4), ...]` Where: -- `nonce` is the initialization vector (4 elements / 1 word) - `key` is the encryption key (4 elements / 1 word) +- `nonce` is the initialization vector (4 elements / 1 word) - `src_ptr` points to plaintext in memory (must be word-aligned) - `dst_ptr` points to where ciphertext will be written (must be word-aligned) - `num_blocks` is the number of 8-element plaintext data blocks (padding is NOT included) @@ -71,14 +71,14 @@ The padding block is automatically added and encrypted. The tag is stored right Decrypts and authenticates ciphertext using non-deterministic advice. This procedure implements AEAD decryption with automatic tag verification and automatic padding handling. **Inputs:** -- Operand stack: `[nonce(4), key(4), src_ptr, dst_ptr, num_blocks, ...]` +- Operand stack: `[key(4), nonce(4), src_ptr, dst_ptr, num_blocks, ...]` **Outputs:** - Operand stack: `[]` (empty stack on success, halts on failure) Where: -- `nonce` is the initialization vector (4 elements) - `key` is the decryption key (4 elements) +- `nonce` is the initialization vector (4 elements) - `src_ptr` points to ciphertext + encrypted_padding + tag in memory (word-aligned) - `dst_ptr` points to where plaintext will be written (word-aligned) - `num_blocks` is the number of 8-element plaintext data blocks (padding is NOT included)