Shiva's role is to destroy the universe in order to re-create it.
(Shiva is a tool for verifying the correctness of software-assisted deterministic reset.)
yosys \ -p 'read_verilog picorv32.v' \ -p 'prep -top picorv32 -flatten -nordff' \ -p 'opt' \ -p 'write_smt2 picorv32.py'
If run as written above, the modified Yosys will produce a Z3Py-compatible file
using an uninterpreted function representation. To use datatypes instead, pass
-stdt argument to the
write_smt2 subcommand. The uninterpreted function
representation seems to be much faster for deep executions.
Then, write a driver for it: see
cores/picorv32_driver.py as a reference.
At a high level, our goal is to run process A and then run process B on a single CPU without processes interfering with each other: process B should not be able to steal process A's private data, and process A should not be able to corrupt process B's execution. This is the classic non-interference property. Achieving (and proving correct) non-interference is hard, so instead, let's use a simple (but heavyweight) mechanism to achieve it that will make the mechanism easy to implement and reason about.
We fully reset the system between task switches, ensuring that we reach a "clean state" after executing process A, so that process B cannot steal A's data and cannot be adversely affected by whatever A did on the system. If resetting a system always restores it to a deterministic state (i.e. independent of the state it was in beforehand), this implies our desired non-interference property. And because we're considering the complete internal state of the processor (not only architectural state but also micro-architectural state), this also implies the absence of architectural and micro-architectural side channels.
For more details on how (formally verified) deterministic reset can be used as a component in building secure systems, as applied to transaction authorization devices, see the DEFCON 27 talk (link coming soon) or our SOSP paper (link coming 8/30).
How do we know that reset actually resets? Reset is a non-trivial operation, and asserting a processor's reset line does not necessarily clear all internal state. The ISA specification is usually nondeterministic, and it says that that certain (often much) architectural state is undefined after reset. The ISA's reset specification does not talk about micro-architectural state at all, because it does not exist at the architectural level, it's an implementation detail.
Looking at the RISC-V ISA for example, Section 3.3 says:
Upon reset, a hart’s privilege mode is set to M. The mstatus fields MIE and MPRV are reset to 0, and the VM field is reset to Mbare. The pc is set to an implementation-defined reset vector. The mcause register is set to a value indicating the cause of the reset. All other hart state is undefined.
Even if the ISA specification is nondeterministic, at the RTL level, the processor is deterministic, so we can prove that a specific processor (or peripheral or entire SoC) can be reliably reset. In general, processors will not clear all internal state after asserting the reset line, so for that reason, we do a software-assisted reset: we assert the reset line, and we have reset software in a read-only region of memory where the processor begins execution upon reset.
Reasoning about architectural state of a processor is hard enough, but trying to reason about internal state (and clearing this state through software instructions) seems especially error-prone if done manually (missing a single register internal to the processor invalidates the noninterference proof). For this reason, we use formal verification to prove correct our software reset code.
At a high level, we want to prove the theorem that "the system can be reliably reset". We can show this by considering two worlds (that are allowed to have arbitrary state) and showing that executing the reset sequence (asserting the reset line, and then allowing the processor to execute for some number of cycles) on the worlds makes them indistinguishable.
See our paper (link coming 8/30) for a more detailed discussion and a formal description of the property being proven.
We perform this proof using an automated theorem prover (Z3). We handle the existential quantifiers by searching (running for increasing numbers of steps).
The general workflow is:
- Write some initialization code (or start with a
- Run the verifier. If it succeeds, you are done. Otherwise, see what processor-internal state is not reset (the verifier will point out at least one state sub-component that is not reset).
- Think about why that state isn't reset (maybe consulting the CPU design to help with this process) and update the code to reset that state component.
- GOTO 1
We have verified reset for the PicoRV32 processor, an simple open-source RISC-V CPU. To try out the demo, follow these steps:
- Install dependencies:
pip install z3-solver
- Get the extracted PicoRV32 core: either extract it yourself using Yosys (see above) or download it here and place it in
- Write some reset code (or get the "solution" here) and place it in
- Assemble the code with
riscv64-unknown-elf-gcc -march=rv32i -mabi=ilp32 -c picorv32.s
- Extract the binary image with
riscv64-unknown-elf-objcopy picorv32.o -O binary picorv32.bin
- Run the verifier with
python cores/picorv32_driver.py reset.bin 200(the last argument is the number of cycles to simulate)