From 992df6bf62f4ab1f6181bd07cae2b55e3ba0b577 Mon Sep 17 00:00:00 2001 From: smartcontracts Date: Mon, 12 Aug 2024 09:47:29 -0400 Subject: [PATCH] feat: add Cannon compiler assumptions (#322) Adds a new section to the Cannon page that describes some security model things related to the assumptions that Cannon makes about compilers that users are using. --- specs/fault-proof/cannon-fault-proof-vm.md | 44 ++++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/specs/fault-proof/cannon-fault-proof-vm.md b/specs/fault-proof/cannon-fault-proof-vm.md index 37266a56e..7ea2e47af 100644 --- a/specs/fault-proof/cannon-fault-proof-vm.md +++ b/specs/fault-proof/cannon-fault-proof-vm.md @@ -17,6 +17,9 @@ - [Pre-image Communication](#pre-image-communication) - [Pre-image I/O Alignment](#pre-image-io-alignment) - [Exceptions](#exceptions) +- [Security Model](#security-model) + - [Compiler Correctness](#compiler-correctness) + - [Compiler Assumptions](#compiler-assumptions) @@ -218,3 +221,44 @@ transition. Nominally, the FPVM must raise an exception in at least the followin VM implementations may raise an exception in other cases that is specific to the implementation. For example, an on-chain FPVM that relies on pre-supplied merkle proofs for memory access may raise an exception if the supplied merkle proof does not match the pre-state `memRoot`. + +## Security Model + +### Compiler Correctness + +Cannon is designed to prove the correctness of a particular state transition that emulates a MIPS32 machine. +Cannon does not guarantee that the MIPS32 instructions correctly implement the program that the user intends to prove. +As a result, Cannon's use as a Fault Proof system inherently depends on some extent on the correctness of the compiler +used to generate the MIPS32 instructions over which Cannon operates. + +To illustrate this concept, suppose that a user intends to prove simple program `input + 1 = output`. +Suppose then that the user's compiler for this program contains a bug and errantly generates the MIPS instructions for a +slightly different program `input + 2 = output`. Although Cannon would correctly prove the operation of this compiled program, +the result proven would differ from the user's intent. Cannon proves the MIPS state transition but makes no assertion about +the correctness of the translation between the user's high-level code and the resulting MIPS program. + +As a consequence of the above, it is the responsibility of a program developer to develop tests that demonstrate that Cannon +is capable of proving their intended program correctly over a large number of possible inputs. Such tests defend against +bugs in the user's compiler as well as ways in which the compiler may inadvertantly break one of Cannon's +[Compiler Assumptions](#compiler-assumptions). Users of Fault Proof systems are strongly encouraged to utilize multiple +proof systems and/or compilers to mitigate the impact of errant behavior in any one toolchain. + +### Compiler Assumptions + +Cannon makes the simplifying assumption that users are utilizing compilers that do not rely on MIPS exception states for +standard program behavior. In other words, Cannon generally assumes that the user's compiler generates spec-compliant +instructions that would not trigger an exception. Refer to [Exceptions](#exceptions) for a list of conditions that are +explicitly handled. + +Certain cases that would typically be asserted by a strict implementation of the MIPS32 specification are not handled by +Cannon as follows: + +- `add`, `addi`, and `sub` do not trigger an exception on signed integer overflow. +- Instruction encoding validation does not trigger an exception for fields that should be zero. +- Memory instructions do not trigger an exception when addresses are not naturally aligned. + +Many compilers, including the Golang compiler, will not generate code that would trigger these conditions under bug-free +operation. Given the inherent reliance on [Compiler Correctness](#compiler-correctness) in applications using Cannon, the +tests and defense mechanisms that must necessarily be employed by Cannon users to protect their particular programs +against compiler bugs should also suffice to surface bugs that would break these compiler assumptions. Stated simply, Cannon +can rely on specific compiler behaviors because users inherently must employ safety nets to guard against compiler bugs.