Methodology

[lucasmt]

_audits_lidofinance_dual-governance_fork/test/kontrol/report/DualGovernanceFormalVerificationReport.md

Lines 23 to 69 in dfe0fce

	Formal verification of the Lido Dual Governance protocol was conducted using Kontrol, Runtime Verification's tool for symbolic execution of Solidity smart contracts.
	Kontrol's functionality is integrated with the Forge testing framework, a component of the Foundry toolkit for smart contract development. Kontrol tests are written in the same way as Forge parameterized tests, but instead of using fuzzing to run each test on randomly-generated inputs, Kontrol executes the tests symbolically. This means that test parameters are interpreted as symbolic variables with no concrete value associated with them. Kontrol then uses symbolic execution to step through the test exploring all possible execution paths, employing logical and mathematical reasoning to determine if the assertions are satisfied on every path.
	A typical Kontrol test often takes the following form:
	1. Initialize the storage of the relevant contracts with symbolic variables with an unspecified value, in order to represent that the contracts can be in an arbitrary state. This can be done using Kontrol-specific cheatcodes such as `kevm.symbolicStorage` and `kevm.freshUInt`.
	2. Use the `vm.assume` cheatcode to impose restrictions on the values to be considered for the symbolic variables (test inputs and symbolic storage variables).
	3. If the function being tested can only be called by a specific address, use the `vm.prank` cheatcode to impersonate that address.
	4. Call the function being verified.
	5. Use `assert`s to check that certain properties hold after the function returns.
	Other tests can also use cheatcodes to verify other properties, such as that a function reverts under certain conditions, or that external calls are only made to certain contracts.
	In order to make symbolic execution of the tests practical, it's occasionally necessary to make simplifying assumptions. The following are examples that apply to many of the tests below:
	* Rather than a fully symbolic address, several of the property tests below use an arbitrary concrete address to represent a random user of the protocol. This is done to make symbolic execution easier, since reasoning about symbolic values is harder than reasoning about concrete ones. However, since the exact value of an address is usually not important for contract execution, we can generally assume that results for one arbitrary address can generalize to other arbitrary addresses.
	* Most of the symbolic variables representing ETH amounts are assumed to have a value under `2 ** 96`. This is done so that Kontrol can ensure that there won't be an overflow when multiple of these variables are added and multiplied. Similarly, many symbolic variables representing timestamps are assumed to be under `2 ** 35`.
	Other simplifying assumptions specific to certain tests are described in the "Tests and Properties" section.
	## Kontrol Project Structure
	In addition to the test files, a number of auxiliary files are included in the repository:
	* **`kontrol.toml` file:** This file works similarly to the `foundry.toml` file, specifying the configurations for Kontrol to use when running the tests. See the [Kontrol documentation](https://docs.runtimeverification.com/kontrol) for the meaning of different options.
	* **`kontrol-cheatcodes` library:** This submodule, included in the `lib` folder, is necessary in order to import the signature of the Kontrol-specific cheatcodes to the tests.
	* **`model` folder:** This folder contains simplified models of external contracts that the Dual Governance protocol interacts with, in particular the `StETH` token and the `WithdrawalQueue`. These models aim to reproduce the behavior of these contracts in enough detail to simulate their interactions with the Dual Governance contracts, while abstracting away some details that are not necessary to complete verification of the Dual Governance functions.
	* **`...StorageSetup.sol` files:** These files include functions to initialize the storage of important contracts, such as `DualGovernance` and `Escrow`, with symbolic variables. These functions are called by the `setUp` function implemented in the `DualGovernanceSetUp` file. By initializing storage variables with symbolic values before each test, we can execute the tests as if the contracts are in an arbitrary state.
	* **`storage` folder:** This folder contains a shell script `storage_setup.sh` that automatically generates a set of Solidity files of the form `...StorageConstants.sol` for different Dual Governance contracts. Each file contains constants indicating the storage slots and offsets for the storage variables of the corresponding contract. These constants are imported by the `...StorageSetup.sol` files, which use them to determine the storage location of each variable when initializing them symbolically. Therefore, if the storage layout of a contract changes, the `storage_setup.sh` script must be re-run in order to update the constants with the correct storage locations.
	* **`lido-lemmas.k` file:** This file contains auxiliary lemmas written in the K specification language, which are added to help Kontrol simplify challenging expressions.
	## Reproducibility Instructions
	The results of the tests can be reproduced using the Kontrol tool by running the following commands from the top-level directory of the repository.
	First, if storage locations in the contracts have changed, run the `storage_setup.sh` script described above in order to update the constants for each storage slot:
	```
	bash test/kontrol/storage/storage_setup.sh
	```
	Then, build the project and run the proofs symbolically using Kontrol:
	```
	export FOUNDRY_PROFILE=kprove # set the Foundry profile to compile the Kontrol tests
	kontrol build
	kontrol prove
	```
	Be aware that the execution time of the entire test suite may take over 24h. See the KaaS reports linked in the Introduction for more detailed timing information for each test, but note that running time may vary depending on the machine.