Skip to content

Latest commit

 

History

History
63 lines (34 loc) · 3.45 KB

isa.md

File metadata and controls

63 lines (34 loc) · 3.45 KB

Instruction Set Architecture

Author: Xinding Wei

1. Introduction

Scope: https://github.com/openvm-org/openvm Commit: 336f1a475e5aa3513c4c5a266399f4128c119bba

2. Findings

Classify by severity according to cantina criteria in terms of likelihood and impact.

Findings include anything that could warrant change or unexpected behavior that should be brought to light. They range from severe to informational.

2.1 Rv32LoadStoreChip could break address space invariants

Severity: Informational/Impact: Low/Likelihood: Low

Context: link

Description: Rv32LoadStoreChip chip doesn't assert supoprted address spaces. An valid instruction could read from an address space which requires elements larger than 1 byte or write into an address space which requires elements smaller than 1 byte. This could break address space invariants which other chips take.

This could only happen when users intend to add some invalid instruction.

Proof of concept: N/A

Recommendation: Add address space assertions in the chip implementation.

Resolution: https://github.com/openvm-org/openvm/commit/171ec20ffea9fed8c67292d4d91dfb9236029ef1

Added constraints for mem_as in Rv32LoadStoreAdapterChip to avoid breaking invariants of each address space.

  • mem_as for LOAD instructions should be in 0/1/2
  • mem_as for STORE instructions should be in 2/3/4

Added constraints for is_load and is_valid in LoadSignExtendCoreChip and LoadStoreCoreChip.

2.2 Hosts allow access out-of-bound memory

Severity: Informational

Context: link1 link2

Description: The current implementation only asserts the start pointer is less than 2^pointer_max_bits. When N > 1, it doesn't check the entire range is in bounds.

However it is not possible to access an address greater than 2^pointer_max_bits in this way. The lower level Memory uses PagedVec, which will do array indexing checks. Array out of bounds will still panic.

Proof of concept: N/A

Recommendation: Fix assertion condition to ptr_u32 + N < (1 << self.mem_config.pointer_max_bits).

3. Discussion

This report checks if all existing instructions follow all invariants. Basically the instructions need to consider:

  • pc stuff. Most opcodes just move DEFAULT_STEP_OFFSET. For branch opcodes, only to_pc of JALR_RV32 is based on memory and that instruction also constraints that there is no overflow.

  • Address space specific constraints. Currently only address space 1/2 have constraints. Only opcodes in Rv32LoadStoreChip use address spaces from operands and the found issue has already been listed above.

  • Hint stuff. The only variable hint opcode is HINT_BUFFER_RV32. If an exploit wants to make HINT_BUFFER_RV32 overflow, it must write into a address > 2^max_pointer_bits. So HINT_BUFFER_RV32 is safe.

  • Public values. There are just PUBLISH for non-continuation and REVEAL for continuation. Nothing needs special discussion.