Thoughts about Yuncong's Attack

[aszepieniec]

Yuncong's (@yczhangsjtu's) attack may apply whenever the correct sorting of memory tables is not enforced. It reads an inconsistent value from memory even though the memory table's AIR is satisfied and even though the permutation argument checks out. This is possible in general because jumps in memory address or clock cycle are are not verified to be increasing jumps. Specifically, jumps that decrease one of these values are allowed (but shouldn't be), and thus it may be possible to rearrange rows between contiguous regions of the memory table.

Without loss of generality, we use mp to denote the memory address, mv to denote the value, and clk to denote the cycle counter. Bear in mind that the same problem (and solutions) apply to three memory structures in Triton: RAM, OpStack, and JumpStack.

Ferdinand's Intuition

1. mp partitions the memory table; the induced regions should be contiguous.
2. clk should increase monotonically within each region.

Intuitively, these rules are necessary and sufficient for integral memory access. However, it's not quite clear how to prove this.

Theorem

What do we even mean by integral memory access? Here is a suggestion:

An execution trace $T$ is has integral memory access iff:

• for all $i$ in {0, . . . , height( $T$ )}, if $T$[ $i$ ][ci] = mem_read then there is a $j$ in {0, . . ., $i-1$} for which all of the following hold:
  • $T$[ $i+1$ ][st0] = $T$[ $j$ ][st0];
  • $T$[ $j$ ][ci] = mem_write;
  • for all $k$ in { $j+1$ , . . ., $i - 1$} either $T$[ $k$ ][ci] =/= mem_write or $T$[ $k$ ][st0] =/= $T$[ $j$ ][st0].

Analogous propositions should be considered for OpStack and JumpStack.

Sequential Addressing

For the RAM specifically, the memory pointer can be any field element. As a result, the jumps can be arbitrarily big, and no sorting can be enforced.

A solution is to use a lookup table into a map that sends random memory addresses to sequential memory addresses and back. This memory address bijection (MAB) maps into the range {0, . . . , k} where k+1 is the number of unique memory addresses. The column ramp comes with a counterpart samp (s for sequential). A set equality argument establishes that the pairs (ramp, samp) that appear in the Ram Table constitute the same set as the pairs in the Mab Table. The Ram Table is then sorted by samp and this sorting can be verified because samp can never increase by more than one.

How do we establish that the Mab Table defines a bijection? In particular, it can't include two-to-one relations or one-to-two relations. This is an open question.

• answer

Lazy ramp

In the current architecture, ramp and st1 are the same register. As a result, st1 takes all sorts of values and thus implicitly points to memory cells located there.

It is desirable to split ramp and st1 back into two separate registers. This split does not induce a change in the instruction set architecture: ramp only has to assume the value of st1 when the current instruction is mem_read or mem_write.

Solutions

Whenever there is a jump in clk, the difference between the next and the current values must be small but positive. There are various strategies to prove that this is the case.

Solution 1: U32 Lookups

Since we do not expect the cycle counter to rise above $2^{32}$, we can require that this difference is a u32 integer. A table lookup argument to the U32 Table can establish this fact.

Solution 2: Add Bit Columns

We add k columns whose values are constrained to bits, for some k – say, k = 32. Whenever there is a jump, the jump is exactly equal to the integer represented by the bit columns.

Solution 3: Add Dummy Rows

Add 1 column that indicates whether rows are dummy rows or not. Whenever there is a jump, insert dummy rows that increase clk by one in each row.

Solution 4: Build Difference

This solution can be seen as a hybrid between solutions 2 and 3. Whenever there is a jump, we add logarithmically many dummy rows where we build a difference by adding one or multiplying by two in every row. When the sequence of dummy rows ends, the value at the end is added to clk.

[jan-ferdinand]

clk should increase contiguously within each region.

I think I mean “monotonically” instead of “contiguously.”

[jan-ferdinand]

As a reference: the alluded-to attack is described in greater detail in #12.

[jan-ferdinand]

I believe that a monotonically increasing mp and the additional limitation that mp lies in range [0, $2^{32}$[ achieves contiguous regions. Thus, any of the solutions {1, 2, 4} should be applicable to ramp in the same way it is proposed to apply to clk. Crucially, this would not require samp or the MAB.

(Solution 3 is applicable in much the same way but most probably prohibitively expensive.)

[jan-ferdinand]

Superseded by #77 and #78.