Consistency checks for load()/store() of machines

[diegonehab]

Introduction

A machine is verifiable if all execution methods (run, run_uarch/reset_uarch, log_step_uarch/verify_step_uarch, log_step/verify_step) produce the same state transitions from the same initial state hash.
The list below contains a set of conditions that are necessary for verifiability:

1. Reproducible. is_unreproducible() checks three conditions: iunrep == 0 (otherwise run polls wall-clock time
   and VirtIO devices, diverging from other methods), config.processor.registers.iunrep == 0, and iconsole getchar is disabled (otherwise run returns real console input while other methods return -1, diverging htif_fromhost).

2. Uarch state pristine. cycle == 0, halt_flag == 0, pc == AR_UARCH_RAM_START, x[0-31] == 0, RAM == embedded uarch.bin (+ trailing zeros). run ignores uarch RAM; run_uarch executes it. When the program running inside the uarch is not uarch.bin, it can write to/read from memory without the same checks performed by run.

3. Hashtree consistency.* The hashtree state in stored machines has to be consistent with the rest of the state. Note that it does not have to be up to date, since it will be updated as needed on the fly. However, if the stored hashtree contains an incorrect hash in any node that is not marked dirty, the proofs generated by log_step and log_step_uarch and log_reset_uarch will be invalid.

4. Emulator version match. marchid, mvendorid, mimpid work like a kind of "magic number" for machines that have been stored to disk. This allow for quick rejections of stored machines that are incompatible with the emulator that is trying to load them.

5. Processor shadow integrity. x0 == 0, padding bytes pristine. During execution, the emulator will never break these invariants. Should they be broken, there is either a severe bug in the emulator, or the stored machine has been corrupted or tampered with.

6. PMA state matches config. In-memory PMA list must match host-side address ranges. During execution, the PMA list
   is never changed. run, run_uarch, log_step_uarch and log_step use host-side objects based on the config; verify_step_uarch and verify_step use the in-memory list.

The cost of checking

The most expensive test is the hashtree consistency.
The uarch state pristine test is a distant second.
All other tests are essentially free.
When the hashtree can be assumed to be consistent and up to date, then even the uarch state pristine test is essentially free.

Contextual checking

The emulator is used in three different contexts:
in deployment (which requires the emulator to be reproducible), in prototyping, and in tests.
In certain testing scenarios, it is desirable run the machine with all consistency checks disabled.
In prototyping, the machine may not be reproducible, but we should still prevent crashes.
In deployment, we should guarantee verifiability to the greatest extent practical.

Whether to run or not each of these checks is therefore a matter of context.

Proposal for deployment

In deployment, all checks should be performed, with the potential exception of the hashtree consistency check:

1. Before an application is first deployed, a full check must be performed (and the fresh root hash must be checked against the expected template hash).
2. Whenever an application is downloaded and installed, a full check must be performed (and the fresh root hash must be checked against the expected template hash).
3. Occasionally, an application shapshot is stored (e.g., at epoch boundaries). At these times, a full check should be performed.
4. Between inputs, when loading/storing the machine snapshot with up-to-date hash-tree, in a filesystem with error correction and ECC memory, the hashtree consistency check may be skipped.

Proposal for prototying

In prototyping, the machine will often not be reproducible.
Even so, when loading/storing, we should only skip the uarch state pristine and hashtree consistency.

Proposal for testing

There should be a way to skip any of these tests, so we can put the emulator in arbitraty conditions for testing.

Implementation requirements

Given this discussion, we need:

1. a runtime flag that disables the reproducibility check (though not when loading/storing).
2. a runtime flag that rebuilds the hash-tree from scratch
3. a runtime flag that disables all checks

When rebuilding the hashtree from scratch is set, the cost of checking uarch pristine is negligible.
When it is not set, presumably the user trusts what is on disk. Then, the machine can check that the node corresponding to the uarch state is clean and simply compare its hash with the pristine one, otherwise, it can check by content.