Consistency of RAM Table

[aszepieniec]

There is an attack whereby the malicious prover can read a zero from a given memory location when the last time he wrote to it, the written value wasn't zero. Here is an example trace that illustrates the attack:

clk	ramp	ramv
0	0	0
1	0	7
2	1	0
3	1	-
4	2	0
5	2	-
6	0	0

The boundary constraints are satisfied, because they state that the first row should consist of all zeros. The hv6 column is omitted because it is not relevant for the attack, but there is a valid assignment to this column. The remaining transition constraints are

1. if ramp changes then ramv is zero – this constraint is satisfied;
2. If ramp does not change and ramv does change then clk increases by one – this constraint is also satisfied.

Therefore the above trace is a valid trace. But the problem is that the memory cell at location 0 is accessed again in cycle 6. At this point it should have the value that it was set to in cycle 1, but it has the value 0 instead.

We came up with the following solution: we disallow reads from uninitialized memory. Specifically:

• Include the current instruction ci in the RAM table. This adds one column.
• Include a new column init which contains only 0 or 1, adding a second column.
• Whenever the ramp changes, init is set to zero.
• Whenever ci is write_mem, init is set to one.
• Whenever ci is read_mem, init has to be one.

Tasks

• Verify solution
• Update arithmetization
• Implement in VM's simulate: add columns
• Implement in RamTable: add constraints and update permutation argument.

[aszepieniec]

Credit for the attack goes to @yczhangsjtu.

[yczhangsjtu]

This solution looks like a patch specific to this very attack. However, I’m afraid that there are potentially more attacks beyond this, if the clk and ramp columns are not ensured to be sorted.

For example, still in the example processor table provided in arithemtization.md, the attack may change the value read by mem_read at clk=12 from 6 to 7, and move the corresponding row in the RAM table after the row where clk=30 or clk=31. The resulting table still satisfies the constraints even after the solution is applied.

The Processor Table:

clk	ci	nia	st0	st1	st2	st3	ramv
0	push	5	0	0	0	0	0
1	push	6	5	0	0	0	0
2	write_mem	pop	6	5	0	0	0
3	pop	pop	6	5	0	0	6
4	pop	push	5	0	0	0	0
5	push	15	0	0	0	0	0
6	push	16	15	0	0	0	0
7	write_mem	pop	16	15	0	0	0
8	pop	pop	16	15	0	0	16
9	pop	push	15	0	0	0	0
10	push	5	0	0	0	0	0
11	push	0	5	0	0	0	0
12	read_mem	pop	0	5	0	0	6 -> 7
13	pop	pop	6	5	0	0	6
14	pop	push	5	0	0	0	0
15	push	15	0	0	0	0	0
16	push	0	15	0	0	0	0
17	read_mem	pop	0	15	0	0	16
18	pop	pop	16	15	0	0	16
19	pop	push	15	0	0	0	0
20	push	5	0	0	0	0	0
21	push	7	5	0	0	0	0
22	write_mem	pop	7	5	0	0	6
23	pop	pop	7	5	0	0	7
24	pop	push	5	0	0	0	0
25	push	15	0	0	0	0	0
26	push	0	15	0	0	0	0
27	read_mem	push	0	15	0	0	16
28	push	5	16	15	0	0	16
29	push	0	5	16	15	0	0
30	read_mem	halt	0	5	16	15	7
31	halt	halt	7	5	16	15	7

The RAM table:

clk	ramp (≘st1)	ramv	hv6
0	0	0	0
1	0	0	0
4	0	0	0
5	0	0	0
6	0	0	0
9	0	0	0
10	0	0	0
11	0	0	0
14	0	0	0
15	0	0	0
16	0	0	0
19	0	0	0
20	0	0	0
21	0	0	0
24	0	0	0
25	0	0	0
26	0	0	$5^{-1}$
2	5	0	0
3	5	6	0
Remove this 12	5	6	0
13	5	6	0
22	5	6	0
23	5	7	0
30	5	7	0
Add here 12	5	7	0
31	5	7	$10^{-1}$
7	15	0	0
8	15	16	0
17	15	16	0
18	15	16	0
27	15	16	0
28	15	16	1
29	16	0	0

I can’t say for sure that the sorting is really unavoidable. It might be possible to add more patches to avoid all such attacks, but I would suggest rigorous security proof for the soundness of the constraints (and I believe that trying to prove the soundness will reveal more attacks).

[aszepieniec]

Looks like this attack works 👏

[jan-ferdinand]

I would suggest rigorous security proof for the soundness of the constraints

yes!

(and I believe that trying to prove the soundness will reveal more attacks).

hopefully not, but probably: yes.

[jan-ferdinand]

Sparked by your attacks, @aszepieniec and I have revisited Triton VM's RAM design. Summarizing, all attacks that we can think of, including the two you present, can be thwarted if

1. ramp forms contiguous regions in the RAM Table, and
2. clk increases monotonically within any such region.

Having considered a few options, the easiest way to do this seems to be using the U32 Table's lt operation. More concretely:

1. if ramp = ramp', i.e., ramp does not change, then clk is less than clk', and
2. if ramp ≠ ramp', i.e., ramp does change, then ramp is less than ramp'.

Since this might grow said U32 Table a lot, we should definitely consider incorporating byte-wise lookups for the U32 Table, as suggested in #8.

[jan-ferdinand]

Superseded by #24.