LeaVe is a tool for verifying that processor designs formalized in Verilog satisfy an ISA-level leakage contract capturing security guarantees in terms of timing leaks.
For more details on LeaVe's verification approach, see our paper "Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts" at ACM CCS 2023 (open access here).
For more details on leakage contracts, see our paper "Hardware-Software Contracts for Secure Speculation" at IEEE S&P 2021 (open access here).
To run LeaVe, you need the following dependencies:
- Python, version 3.8.10 or higher
- yices 2.6.4
- Yosys, version 0.26+50 or higher
- Icarus Verilog version 12.0
LeaVe relies on three Yosys custom passes to prepare the processor design for verification. These passes need to be compiled before using LeaVe. Follow the instructions in folder yosys-passes
to build the Yosys passes.
As a baseline example, we will use the running example from our CCS 2023 paper (see section 2 for a description of processor, ISA, and leakage contract). To run this baseline example and check that everything works correctly follow these steps:
-
In the configuration file
config/RE.yaml
, change the value of theyosysPath
option to point to the Yosys's executable in your machine. The leakage contract is encoded in thesrcObservations
option in the configuration file, whereas the attacker monitor is encoded in thetrgObservations
option. -
Run LeaVe with the command
python3 source/cli.py config/RE.yaml
. If everything is set-up properly, the output filetestout/logfile
should contain theVerification passed
message. This indicates that LeaVe successfully verified that the contract insrcObservations
is satisfied for the processor under verification and the attacker intrgObservations
. -
Now, remove the contract observations
MUL
fromsrcObservations
, so that thesrcObservations
is[]
. Run again LeaVe with the commandpython3 source/cli.py config/RE.yaml
. This time the output filetestout/logfile
should contain the messageVerification failed
, indicating that LeaVe cannot prove contract satisfaction.
These are the instructions for reproducing the results in Table 1 from our CCS 2023 paper. For each target, the instructions below describe how to verify that the processor satisfies the strongest contract in Table 1.
Below, $TARGET
is one of [DarkRISCV-2
,DarkRISCV-3
,Sodor-2
,ibex-small
,ibex-mult-div
,ibex-cache
]. To use LeaVe to verify $TARGET
, follow these steps:
-
In the configuration file
config/$TARGET.yaml
, change the value of theyosysPath
option to point to the Yosys's executable in your machine, e.g.,yosys-root-path/yosys
. -
Run LeaVe by executing
python3 source/cli.py config/$TARGET.yaml
. -
Inspect the results in the folder
testOut
. The output filelogfile
contains the information about the invariants discovered in each iteration of the invariant synthesis loop. The output filelogtimefile
reports timing statistics about the verification process.
Note that while the verification of DarkRISCV-2
,DarkRISCV-3
, and Sodor-2
is rather quick, verifying ibex-small
,ibex-mult-div
, and ibex-cache
required roughly 1 day in our experiments.
To run the 4way-LeaVe, follow the instruction in folder 4way
.
To verify a new processor design using LeaVe, you first need to prepare the following files:
-
A template of the product circuit. For an example of such template, see the file at
benchmarks/prod_example.v
. It should be placed in the same folder of the source code. -
A configuration file. For an example of such file, see
config/config_example.yaml
. It should be placed in the folder "config". -
Once both files, you can start the verification by executing the following command:
python3 source/cli.py config/config_example.yaml