Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)).
Expand Down
28 changes: 14 additions & 14 deletions crates/lib/core/asm/crypto/aead.masm
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion crates/lib/core/docs/crypto/aead.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.<br /><br />This procedure encrypts plaintext and automatically includes a padding block at the end.<br />The padding block [1, 0, 0, 0, 0, 0, 0, 0] is encrypted without requiring the caller<br />to write padding into the plaintext buffer manually.<br />This, however, requires the plaintext length to be a multiple of 8. This assumption is made<br />both in this procedure as well as in the decryption procedure.<br /><br />Input: [key(4), nonce(4), src_ptr, dst_ptr, num_blocks, ...]<br />Output: [tag(4), ...]<br /><br />Where:<br />- key is the encryption key (4 elements)<br />- nonce is the initialization vector (4 elements)<br />- src_ptr points to plaintext in memory (must be word-aligned)<br />- dst_ptr points to where ciphertext will be written (must be word-aligned)<br />- num_blocks is the number of 8-element plaintext data blocks (NO padding included)<br />- tag is the authentication tag returned on stack (4 elements)<br /><br />Memory Layout:<br />- Input at src_ptr: [plaintext_block_0(8), ..., plaintext_block_n(8)]<br />Length: num_blocks * 8 elements (must be multiple of 8)<br /><br />- Output at dst_ptr: [ciphertext_block_0(8), ..., ciphertext_block_n(8), encrypted_padding(8)]<br />Length: (num_blocks + 1) * 8 elements<br />The padding block is automatically added and encrypted<br /><br />- Standard format: the tag is stored right after ciphertext to create:<br />[ciphertext_blocks(num_blocks * 8), encrypted_padding(8), tag(4)]<br />Tag location: dst_ptr + (num_blocks + 1) * 8<br /><br />Memory Requirements:<br />- Plaintext must be at word-aligned addresses (addr % 4 == 0)<br />- Each block is 8 field elements (2 words)<br />- Blocks must be stored contiguously in memory<br /><br /># Panics<br /><br />Panics if the source and destination memory ranges overlap<br />(in-place encryption not supported).<br /><br />Padding:<br />- Padding is AUTOMATIC - caller should NOT pad the plaintext<br />- The procedure writes encrypted padding to dst_ptr + (num_blocks * 8)<br />- The plaintext buffer is not modified<br />- For empty plaintext (num_blocks = 0), only the padding block is encrypted<br /><br />Cycles (estimate): 77 + 2 * n<br />Where:<br />- n = number of field elements encrypted (includes the final padding block)<br />- For num_blocks data blocks: n = 8 * (num_blocks + 1)<br /> |
| decrypt | Decrypts and authenticates ciphertext using non-deterministic advice.<br /><br />This procedure implements AEAD decryption with automatic tag verification. It mirrors<br />the encrypt procedure's padding behavior while leaving the plaintext output unpadded.<br /><br />Decryption Flow:<br />1. Computes tag location: src_ptr + (num_blocks + 1) * 8<br />2. Emits event for host to decrypt ciphertext (data blocks + padding block)<br />3. Loads plaintext data blocks from advice into dst_ptr (num_blocks * 8 elements)<br />4. Calls encrypt which reads data blocks and adds padding automatically<br />5. Re-encrypts data + padding to compute authentication tag<br />6. Compares computed tag with tag from memory at src_ptr + (num_blocks + 1) * 8<br />7. Halts execution with assertion failure if tags don't match<br /><br />Input: [key(4), nonce(4), src_ptr, dst_ptr, num_blocks, ...]<br />Output: [] (empty stack on success, halts on failure)<br /><br />Where:<br />- key is the decryption key (4 elements)<br />- nonce is the initialization vector (4 elements)<br />- src_ptr points to ciphertext + encrypted_padding + tag in memory (word-aligned)<br />- dst_ptr points to where plaintext will be written (word-aligned)<br />- num_blocks is the number of 8-element plaintext data blocks (NO padding)<br /><br />Memory Layout:<br />- Input at src_ptr: [ciphertext_blocks(num_blocks * 8), encrypted_padding(8), tag(4)]<br />The encrypted padding is at: src_ptr + (num_blocks * 8)<br />The tag is at: src_ptr + (num_blocks + 1) * 8<br /><br />- Output at dst_ptr: [plaintext_block_0(8), ..., plaintext_block_n(8)]<br />Length: num_blocks * 8 elements<br />The padding block is authenticated but not written to the plaintext output.<br /><br />Event: Emits AEAD_DECRYPT event with (nonce, key, src_ptr, dst_ptr, num_blocks)<br />The host event handler must:<br />- Read full ciphertext from memory at src_ptr ((num_blocks + 1) * 8 elements)<br />- Read authentication tag from memory at src_ptr + (num_blocks + 1) * 8<br />- Decrypt and verify tag using reference implementation<br />- Extract only data blocks (first num_blocks * 8 elements) from decrypted plaintext<br />- Insert data blocks (WITHOUT padding) into advice map (keyed by nonce)<br /><br />Memory Requirements:<br />- Same as encrypt: word-aligned addresses, contiguous blocks<br /><br /># Panics<br /><br />Panics if the source and destination memory ranges overlap<br />(in-place decryption not supported).<br /><br />Security:<br />- Tag verification happens in the MASM procedure via re-encryption<br />- Execution halts with assertion failure if tag verification fails<br />- If execution completes successfully, the plaintext at dst_ptr is authenticated<br /><br />Non-Determinism Soundness:<br />This procedure uses non-deterministic advice to obtain the plaintext, which is sound<br />because:<br />1. The prover provides claimed plaintext via advice (untrusted input)<br />2. This procedure re-encrypts the claimed plaintext with the same (key, nonce)<br />3. Due to deterministic encryption, the same plaintext produces the same ciphertext<br />4. The computed tag cryptographically commits to both plaintext and ciphertext<br />5. Comparing tags verifies that the claimed plaintext is the unique plaintext that<br />encrypts to the given ciphertext under the given (key, nonce)<br /><br />This approach is secure because:<br />- The MASM procedure verifies the tag when calling the encryption procedure<br />- The tag acts as a cryptographic commitment<br />- The deterministic keystream creates a bijection between plaintext and ciphertext<br />- Any deviation from correct plaintext causes assertion failure<br /><br />Note: This procedure does not write the padding block to the plaintext output.<br /><br />Cycles (estimate): 177 + 3.5 * n<br />Where:<br />- n = number of field elements in the plaintext (excludes the padding block)<br />- For num_blocks data blocks: n = 8 * num_blocks<br /> |
| decrypt | Decrypts and authenticates ciphertext using non-deterministic advice.<br /><br />This procedure implements AEAD decryption with automatic tag verification. It mirrors<br />the encrypt procedure's padding behavior while leaving the plaintext output unpadded.<br /><br />Decryption Flow:<br />1. Computes tag location: src_ptr + (num_blocks + 1) * 8<br />2. Emits event for host to decrypt ciphertext (data blocks + padding block)<br />3. Loads plaintext data blocks from advice into dst_ptr (num_blocks * 8 elements)<br />4. Calls encrypt which reads data blocks and adds padding automatically<br />5. Re-encrypts data + padding to compute authentication tag<br />6. Compares computed tag with tag from memory at src_ptr + (num_blocks + 1) * 8<br />7. Halts execution with assertion failure if tags don't match<br /><br />Input: [key(4), nonce(4), src_ptr, dst_ptr, num_blocks, ...]<br />Output: [] (empty stack on success, halts on failure)<br /><br />Where:<br />- key is the decryption key (4 elements)<br />- nonce is the initialization vector (4 elements)<br />- src_ptr points to ciphertext + encrypted_padding + tag in memory (word-aligned)<br />- dst_ptr points to where plaintext will be written (word-aligned)<br />- num_blocks is the number of 8-element plaintext data blocks (NO padding)<br /><br />Memory Layout:<br />- Input at src_ptr: [ciphertext_blocks(num_blocks * 8), encrypted_padding(8), tag(4)]<br />The encrypted padding is at: src_ptr + (num_blocks * 8)<br />The tag is at: src_ptr + (num_blocks + 1) * 8<br /><br />- Output at dst_ptr: [plaintext_block_0(8), ..., plaintext_block_n(8)]<br />Length: num_blocks * 8 elements<br />The padding block is authenticated but not written to the plaintext output.<br /><br />Event: Emits AEAD_DECRYPT event with (key, nonce, src_ptr, dst_ptr, num_blocks)<br />The host event handler must:<br />- Read full ciphertext from memory at src_ptr ((num_blocks + 1) * 8 elements)<br />- Read authentication tag from memory at src_ptr + (num_blocks + 1) * 8<br />- Decrypt and verify tag using reference implementation<br />- Extract only data blocks (first num_blocks * 8 elements) from decrypted plaintext<br />- Insert data blocks (WITHOUT padding) into advice map (keyed by nonce)<br /><br />Memory Requirements:<br />- Same as encrypt: word-aligned addresses, contiguous blocks<br /><br /># Panics<br /><br />Panics if the source and destination memory ranges overlap<br />(in-place decryption not supported).<br /><br />Security:<br />- Tag verification happens in the MASM procedure via re-encryption<br />- Execution halts with assertion failure if tag verification fails<br />- If execution completes successfully, the plaintext at dst_ptr is authenticated<br /><br />Non-Determinism Soundness:<br />This procedure uses non-deterministic advice to obtain the plaintext, which is sound<br />because:<br />1. The prover provides claimed plaintext via advice (untrusted input)<br />2. This procedure re-encrypts the claimed plaintext with the same (key, nonce)<br />3. Due to deterministic encryption, the same plaintext produces the same ciphertext<br />4. The computed tag cryptographically commits to both plaintext and ciphertext<br />5. Comparing tags verifies that the claimed plaintext is the unique plaintext that<br />encrypts to the given ciphertext under the given (key, nonce)<br /><br />This approach is secure because:<br />- The MASM procedure verifies the tag when calling the encryption procedure<br />- The tag acts as a cryptographic commitment<br />- The deterministic keystream creates a bijection between plaintext and ciphertext<br />- Any deviation from correct plaintext causes assertion failure<br /><br />Note: This procedure does not write the padding block to the plaintext output.<br /><br />Cycles (estimate): 177 + 3.5 * n<br />Where:<br />- n = number of field elements in the plaintext (excludes the padding block)<br />- For num_blocks data blocks: n = 8 * num_blocks<br /> |
5 changes: 4 additions & 1 deletion crates/lib/core/src/handlers/aead_decrypt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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<Vec<AdviceMutation>, 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)
Expand Down
8 changes: 4 additions & 4 deletions docs/src/user_docs/core_lib/crypto/aead.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down
Loading