Merge branch 'certora/integration' into 'master'

Resolve "Integrating the certora formal verification rules in the CI"

Closes #59

See merge request aave-tech/protocol-v2!67
This commit is contained in:
Ernesto Boado 2020-10-30 13:48:25 +00:00
commit 4e56df7d56
11 changed files with 702 additions and 2 deletions

View File

@ -695,7 +695,7 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
* @param asset the address of the reserve
* @return the reserve normalized income
*/
function getReserveNormalizedIncome(address asset) external override view returns (uint256) {
function getReserveNormalizedIncome(address asset) external virtual override view returns (uint256) {
return _reserves[asset].getNormalizedIncome();
}

View File

@ -288,7 +288,7 @@ contract StableDebtToken is IStableDebtToken, DebtTokenBase {
* @param avgRate the average rate at which calculate the total supply
* @return The debt balance of the user since the last burn/mint action
**/
function _calcTotalSupply(uint256 avgRate) internal view returns (uint256) {
function _calcTotalSupply(uint256 avgRate) internal virtual view returns (uint256) {
uint256 principalSupply = super.totalSupply();
if (principalSupply == 0) {

1
runStableTokenCLI.sh Normal file
View File

@ -0,0 +1 @@
certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond --cache StableDebtToken --staging master

1
runUserConfigCLI.sh Normal file
View File

@ -0,0 +1 @@
certoraRun specs/harness/UserConfigurationHarness.sol --solc solc6.8 --verify UserConfigurationHarness:specs/UserConfiguration.spec --settings -useBitVectorTheory --staging master

1
runVariableTokenCLI.sh Normal file
View File

@ -0,0 +1 @@
certoraRun contracts/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc solc6.8 --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -assumeUnwindCond,-useNonLinearArithmetic --cache VariableDebtToken --staging

155
specs/StableDebtToken.spec Normal file
View File

@ -0,0 +1,155 @@
methods {
getUserLastUpdated(address) returns uint40 envfree
}
rule integrityTimeStamp(address user, method f) {
env e;
require sinvoke getIncentivesController(e) == 0;
require getUserLastUpdated(user) <= e.block.timestamp;
calldataarg arg;
sinvoke f(e,arg);
assert getUserLastUpdated(user) <= e.block.timestamp;
}
/**
TotalSupply is the sum of all users balances
totalSupply(t) = Σaddress u. balanceOf(u,t)
Check that each possible opertaion changes the balance of at most one user
*/
rule balanceOfChange(address a, address b, method f )
{
env e;
require a!=b;
require sinvoke getIncentivesController(e) == 0;
uint256 balanceABefore = sinvoke balanceOf(e,a);
uint256 balanceBBefore = sinvoke balanceOf(e,b);
calldataarg arg;
sinvoke f(e, arg);
uint256 balanceAAfter = sinvoke balanceOf(e,a);
uint256 balanceBAfter = sinvoke balanceOf(e,b);
assert ( balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter );
}
/**
Check that the change to total supply is coherent with the changes to balance
*/
rule integirtyBalanceOfTotalSupply(address a, method f )
{
env e;
require sinvoke getIncentivesController(e) == 0;
uint256 balanceABefore = sinvoke balanceOf(e,a);
uint256 totalSupplyBefore = sinvoke totalSupply(e);
calldataarg arg;
sinvoke f(e, arg);
require (f.selector != burn(address,uint256).selector );
uint256 balanceAAfter = sinvoke balanceOf(e,a);
uint256 totalSupplyAfter = sinvoke totalSupply(e);
assert (balanceAAfter != balanceABefore => ( balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
}
/* Burn behaves differently and due to accumulation errors might have less total supply than the balance
*/
rule integirtyBalanceOfTotalSupplyOnBurn(address a, method f)
{
env e;
require sinvoke getIncentivesController(e) == 0;
uint256 balanceABefore = sinvoke balanceOf(e,a);
uint256 totalSupplyBefore = sinvoke totalSupply(e);
uint256 x;
sinvoke burn(e, a, x);
uint256 balanceAAfter = sinvoke balanceOf(e,a);
uint256 totalSupplyAfter = sinvoke totalSupply(e);
if (totalSupplyBefore > x)
assert (balanceAAfter != balanceABefore => ( balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
else
assert (totalSupplyAfter == 0 );
}
/**
Mint inceases the balanceOf user a as expected
*/
rule integrityMint(address a, uint256 x) {
env e;
require sinvoke getIncentivesController(e) == 0;
uint256 index;
uint256 balancebefore = sinvoke balanceOf(e,a);
sinvoke mint(e,a,x,index);
uint256 balanceAfter = sinvoke balanceOf(e,a);
assert balanceAfter == balancebefore+x;
}
/**
Mint is additive, can performed either all at once or gradually
mint(u,x); mint(u,y) ~ mint(u,x+y) at the same timestamp
Note: We assume that the stable rate of the user is 0.
The case where the rate is non-zero takes much more time to prove,
and therefore it is currently excluded from the CI.
*/
rule additiveMint(address a, uint256 x, uint256 y) {
env e;
require sinvoke getIncentivesController(e) == 0;
require getUserStableRate(e,a) == 0;
uint256 index;
storage initialStorage = lastStorage;
sinvoke mint(e,a,x,index);
sinvoke mint(e,a,y,index);
uint256 balanceScenario1 = sinvoke balanceOf(e,a);
uint256 t = x + y;
sinvoke mint(e,a, t ,index) at initialStorage;
uint256 balanceScenario2 = sinvoke balanceOf(e,a);
assert balanceScenario1 == balanceScenario2, "mint is not additive";
}
rule integrityBurn(address a, uint256 x) {
env e;
require sinvoke getIncentivesController(e) == 0;
uint256 index;
uint256 balancebefore = sinvoke balanceOf(e,a);
sinvoke burn(e,a,x);
uint256 balanceAfter = sinvoke balanceOf(e,a);
assert balanceAfter == balancebefore - x;
}
rule additiveBurn(address a, uint256 x, uint256 y) {
env e;
require sinvoke getIncentivesController(e) == 0;
storage initialStorage = lastStorage;
sinvoke burn(e, a, x);
sinvoke burn(e, a, y);
uint256 balanceScenario1 = balanceOf(e, a);
uint256 t = x + y;
sinvoke burn(e, a, t) at initialStorage;
uint256 balanceScenario2 = balanceOf(e, a);
assert balanceScenario1 == balanceScenario2, "burn is not additive";
}
/**
mint and burn are inverse operations
Thus, totalSupply is back to initial state
BalanceOf user is back to initial state */
rule inverseMintBurn(address a, uint256 x) {
env e;
require sinvoke getIncentivesController(e) == 0;
uint256 index;
uint256 balancebefore = sinvoke balanceOf(e,a);
sinvoke mint(e,a,x,index);
sinvoke burn(e,a,x);
uint256 balanceAfter = sinvoke balanceOf(e,a);
assert balancebefore == balanceAfter, "burn is not inverse of mint";
}

View File

@ -0,0 +1,66 @@
methods {
setBorrowing(address, uint256, bool) envfree
setUsingAsCollateral(address, uint256, bool) envfree
isUsingAsCollateralOrBorrowing(address, uint256) returns bool envfree
isBorrowing(address, uint256) returns bool envfree
isUsingAsCollateral(address, uint256) returns bool envfree
isBorrowingAny(address ) returns bool envfree
isEmpty(address ) returns bool envfree
}
invariant empty(address user, uint256 reserveIndex )
isEmpty(user) => !isBorrowingAny(user) && !isUsingAsCollateralOrBorrowing(user, reserveIndex)
invariant notEmpty(address user, uint256 reserveIndex )
( isBorrowingAny(user) || isUsingAsCollateral(user, reserveIndex)) => !isEmpty(user)
invariant borrowing(address user, uint256 reserveIndex )
isBorrowing(user, reserveIndex) => isBorrowingAny(user)
invariant collateralOrBorrowing(address user, uint256 reserveIndex )
( isUsingAsCollateral(user, reserveIndex) || isBorrowing(user, reserveIndex) ) <=> isUsingAsCollateralOrBorrowing(user, reserveIndex)
rule setBorrowing(address user, uint256 reserveIndex, bool borrowing)
{
require reserveIndex < 128;
setBorrowing(user, reserveIndex, borrowing);
assert isBorrowing(user, reserveIndex) == borrowing, "unexpected result";
}
rule setBorrowingNoChangeToOther(address user, uint256 reserveIndex, uint256 reserveIndexOther, bool borrowing)
{
require reserveIndexOther != reserveIndex;
require reserveIndexOther < 128 && reserveIndex < 128;
bool otherReserveBorrowing = isBorrowing(user, reserveIndexOther);
bool otherReserveCollateral = isUsingAsCollateral(user,reserveIndexOther);
setBorrowing(user, reserveIndex, borrowing);
assert otherReserveBorrowing == isBorrowing(user, reserveIndexOther) &&
otherReserveCollateral == isUsingAsCollateral(user,reserveIndexOther), "changed to other reserve";
}
rule setUsingAsCollateral(address user, uint256 reserveIndex, bool usingAsCollateral)
{
require reserveIndex < 128;
setUsingAsCollateral(user, reserveIndex, usingAsCollateral);
assert isUsingAsCollateral(user, reserveIndex) == usingAsCollateral, "unexpected result";
}
rule setUsingAsCollateralNoChangeToOther(address user, uint256 reserveIndex, uint256 reserveIndexOther, bool usingAsCollateral)
{
require reserveIndexOther != reserveIndex;
require reserveIndexOther < 128 && reserveIndex < 128;
bool otherReserveBorrowing = isBorrowing(user, reserveIndexOther);
bool otherReserveCollateral = isUsingAsCollateral(user,reserveIndexOther);
setUsingAsCollateral(user, reserveIndex, usingAsCollateral);
assert otherReserveBorrowing == isBorrowing(user, reserveIndexOther) &&
otherReserveCollateral == isUsingAsCollateral(user,reserveIndexOther), "changed to other reserve";
}

View File

@ -0,0 +1,173 @@
using LendingPoolHarnessForVariableDebtToken as POOL
/**
TotalSupply is the sum of all users balances
totalSupply(t) = Σaddress u. balanceOf(u,t)
Check that each possible opertaion changes the balance of at most one user
*/
rule balanceOfChange(address a, address b, method f)
{
env e;
require a!=b ;
uint256 balanceABefore = sinvoke balanceOf(e, a);
uint256 balanceBBefore = sinvoke balanceOf(e, b);
calldataarg arg;
sinvoke f(e, arg);
uint256 balanceAAfter = sinvoke balanceOf(e, a);
uint256 balanceBAfter = sinvoke balanceOf(e, b);
assert ( balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter );
}
/*
Check that the changed to total supply is coherent with the changes to balance
*/
rule integirtyBalanceOfTotalSupply(address a, method f )
{
env e;
uint256 balanceABefore = balanceOf(e, a);
uint256 totalSupplyBefore = totalSupply(e);
calldataarg arg;
sinvoke f(e, arg);
require (f.selector != burn(address, uint256, uint256).selector &&
f.selector != mint(address, uint256, uint256).selector ) ;
uint256 balanceAAfter = balanceOf(e, a);
uint256 totalSupplyAfter = totalSupply(e);
assert (balanceAAfter != balanceABefore => ( balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
}
/* Burn behaves deferently and due to accumulation errors might hace less total supply then the balance
*/
rule integirtyBalanceOfTotalSupplyOnBurn(address a, method f )
{
env e;
uint256 balanceABefore = balanceOf(e, a);
uint256 totalSupplyBefore = totalSupply(e);
uint256 x;
address asset;
uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
sinvoke burn(e, a, x, index);
uint256 balanceAAfter = balanceOf(e, a);
uint256 totalSupplyAfter = totalSupply(e);
assert (balanceAAfter != balanceABefore => ( balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
}
rule integirtyBalanceOfTotalSupplyOnMint(address a, method f )
{
env e;
uint256 balanceABefore = balanceOf(e, a);
uint256 totalSupplyBefore = totalSupply(e);
uint256 x;
address asset;
uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
sinvoke mint(e, a, x, index);
uint256 balanceAAfter = balanceOf(e, a);
uint256 totalSupplyAfter = totalSupply(e);
assert (balanceAAfter != balanceABefore => ( balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
}
/**
Minting an amount of x tokens for user u increases their balance by x, up to rounding errors.
{ b= balanceOf(u,t) }
mint(u,x,index)
{ balanceOf(u,t) = b + x }
*/
rule integrityMint(address a, uint256 x) {
env e;
address asset;
uint256 index = POOL.getReserveNormalizedVariableDebt(e,asset);
uint256 balancebefore = balanceOf(e, a);
sinvoke mint(e, a, x, index);
uint256 balanceAfter = balanceOf(e, a);
assert balanceAfter == balancebefore+x;
}
/**
Mint is additive, can performed either all at once or gradually
mint(u,x); mint(u,y) ~ mint(u,x+y) at the same timestamp
*/
rule additiveMint(address a, uint256 x, uint256 y) {
env e;
address asset;
uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
storage initialStorage = lastStorage;
sinvoke mint(e, a, x, index);
sinvoke mint(e, a, y, index);
uint256 balanceScenario1 = balanceOf(e, a);
uint t = x + y;
sinvoke mint(e, a, t ,index) at initialStorage;
uint256 balanceScenario2 = balanceOf(e, a);
assert balanceScenario1 == balanceScenario2, "mint is not additive";
}
/**
Transfer of x amount of tokens from user u where receiver is user u
{bu = balanceOf(u) }
burn(u, u, x)
{balanceOf(u) = bu - x }
*/
rule integrityBurn(address a, uint256 x) {
env e;
address asset;
uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
uint256 balancebefore = balanceOf(e, a);
sinvoke burn(e, a, x, index);
uint256 balanceAfter = balanceOf(e, a);
assert balanceAfter == balancebefore - x;
}
/**
Minting is additive, i.e., it can be performed either all at once or in steps.
burn(u, u, x); burn(u, u, y) ~ burn(u, u, x+y)
*/
rule additiveBurn(address a, uint256 x, uint256 y) {
env e;
address asset;
uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
storage initialStorage = lastStorage;
sinvoke burn(e, a, x, index);
sinvoke burn(e, a, y, index);
uint256 balanceScenario1 = balanceOf(e, a);
uint t = x + y;
sinvoke burn(e, a, t ,index) at initialStorage;
uint256 balanceScenario2 = balanceOf(e, a);
assert balanceScenario1 == balanceScenario2, "burn is not additive";
}
/**
Minting and burning are inverse operations.
{bu = balanceOf(u) }
mint(u,x); burn(u, u, x)
{balanceOf(u) = bu }
*/
rule inverseMintBurn(address a, uint256 x) {
env e;
address asset;
uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
uint256 balancebefore = balanceOf(e, a);
sinvoke mint(e, a, x, index);
sinvoke burn(e, a, x, index);
uint256 balanceAfter = balanceOf(e, a);
assert balancebefore == balanceAfter, "burn is not inverse of mint";
}

View File

@ -0,0 +1,198 @@
pragma solidity ^0.6.8;
pragma experimental ABIEncoderV2;
import {ReserveConfiguration} from '../../contracts/libraries/configuration/ReserveConfiguration.sol';
import {UserConfiguration} from '../../contracts/libraries/configuration/UserConfiguration.sol';
import {ReserveLogic} from '../../contracts/libraries/logic/ReserveLogic.sol';
import {ILendingPool} from '../../contracts/interfaces/ILendingPool.sol';
import {LendingPool} from '../../contracts/lendingpool/LendingPool.sol';
/*
Certora: Harness that delegates calls to the original LendingPool.
Used for the verification of the VariableDebtToken contract.
*/
contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
LendingPool private originalPool;
function deposit(
address asset,
uint256 amount,
address onBehalfOf,
uint16 referralCode
) external override {
originalPool.deposit(asset, amount, onBehalfOf, referralCode);
}
function withdraw(address asset, uint256 amount) external override {
originalPool.withdraw(asset, amount);
}
function getBorrowAllowance(
address fromUser,
address toUser,
address asset,
uint256 interestRateMode
) external override view returns (uint256) {
return originalPool.getBorrowAllowance(fromUser, toUser, asset, interestRateMode);
}
function delegateBorrowAllowance(
address asset,
address user,
uint256 interestRateMode,
uint256 amount
) external override {
originalPool.delegateBorrowAllowance(asset, user, interestRateMode, amount);
}
function borrow(
address asset,
uint256 amount,
uint256 interestRateMode,
uint16 referralCode,
address onBehalfOf
) external override {
originalPool.borrow(asset, amount, interestRateMode, referralCode, onBehalfOf);
}
function repay(
address asset,
uint256 amount,
uint256 rateMode,
address onBehalfOf
) external override {
originalPool.repay(asset, amount, rateMode, onBehalfOf);
}
function swapBorrowRateMode(address asset, uint256 rateMode) external override {
originalPool.swapBorrowRateMode(asset, rateMode);
}
function rebalanceStableBorrowRate(address asset, address user) external override {
originalPool.rebalanceStableBorrowRate(asset, user);
}
function setUserUseReserveAsCollateral(address asset, bool useAsCollateral) external override {
originalPool.setUserUseReserveAsCollateral(asset, useAsCollateral);
}
function liquidationCall(
address collateral,
address asset,
address user,
uint256 purchaseAmount,
bool receiveAToken
) external override {
originalPool.liquidationCall(collateral, asset, user, purchaseAmount, receiveAToken);
}
function getReservesList() external override view returns (address[] memory) {
return originalPool.getReservesList();
}
function getReserveData(address asset) external override view returns (ReserveLogic.ReserveData memory) {
return originalPool.getReserveData(asset);
}
function getUserConfiguration(address user) external override view returns (UserConfiguration.Map memory) {
return originalPool.getUserConfiguration(user);
}
function getUserAccountData(address user)
external
override
view
returns (
uint256 totalCollateralETH,
uint256 totalBorrowsETH,
uint256 availableBorrowsETH,
uint256 currentLiquidationThreshold,
uint256 ltv,
uint256 healthFactor
)
{
return originalPool.getUserAccountData(user);
}
function initReserve(
address asset,
address aTokenAddress,
address stableDebtAddress,
address variableDebtAddress,
address interestRateStrategyAddress
) external override {
originalPool.initReserve(asset, aTokenAddress, stableDebtAddress, variableDebtAddress, interestRateStrategyAddress);
}
function setReserveInterestRateStrategyAddress(address asset, address rateStrategyAddress)
external
override
{
originalPool.setReserveInterestRateStrategyAddress(asset, rateStrategyAddress);
}
function setConfiguration(address asset, uint256 configuration) external override {
originalPool.setConfiguration(asset, configuration);
}
function getConfiguration(address asset)
external
override
view
returns (ReserveConfiguration.Map memory)
{
return originalPool.getConfiguration(asset);
}
mapping(uint256 => uint256) private reserveNormalizedIncome;
function getReserveNormalizedIncome(address asset) external override view returns (uint256) {
require(reserveNormalizedIncome[block.timestamp] == 1e27);
return reserveNormalizedIncome[block.timestamp];
}
mapping(uint256 => uint256) private reserveNormalizedVariableDebt;
function getReserveNormalizedVariableDebt(address asset)
external
override
view
returns (uint256)
{
require(reserveNormalizedVariableDebt[block.timestamp] == 1e27);
return reserveNormalizedVariableDebt[block.timestamp];
}
function setPause(bool val) external override {
originalPool.setPause(val);
}
function paused() external override view returns (bool) {
return originalPool.paused();
}
function flashLoan(
address receiver,
address[] calldata assets,
uint256[] calldata amounts,
uint256 mode,
address onBehalfOf,
bytes calldata params,
uint16 referralCode
) external override {
originalPool.flashLoan(receiver, assets, amounts, mode, onBehalfOf, params, referralCode);
}
function finalizeTransfer(
address asset,
address from,
address to,
uint256 amount,
uint256 balanceFromAfter,
uint256 balanceToBefore
) external override {
originalPool.finalizeTransfer(asset, from, to, amount, balanceFromAfter, balanceToBefore);
}
}

View File

@ -0,0 +1,28 @@
pragma solidity ^0.6.8;
import {StableDebtToken} from '../../contracts/tokenization/StableDebtToken.sol';
import {IncentivizedERC20} from '../../contracts/tokenization/IncentivizedERC20.sol';
contract StableDebtTokenHarness is StableDebtToken {
constructor(
address pool,
address underlyingAsset,
string memory name,
string memory symbol,
address incentivesController
) public StableDebtToken(pool, underlyingAsset, name, symbol, incentivesController) {}
function balanceOf(address account) public override view returns (uint256) {
return IncentivizedERC20.balanceOf(account);
}
function _calcTotalSupply(uint256 avgRate) internal override view returns (uint256) {
return IncentivizedERC20.totalSupply();
}
function getIncentivesController() public view returns (address) {
return address(_incentivesController);
}
}

View File

@ -0,0 +1,77 @@
pragma solidity ^0.6.8;
pragma experimental ABIEncoderV2;
import {UserConfiguration} from '../../contracts/libraries/configuration/UserConfiguration.sol';
/*
A wrapper contract for calling functions from the library UserConfiguration.
*/
contract UserConfigurationHarness {
UserConfiguration.Map internal usersConfig;
function setBorrowing(
address user,
uint256 reserveIndex,
bool borrowing
) public {
UserConfiguration.setBorrowing(usersConfig, reserveIndex, borrowing);
}
function setUsingAsCollateral(
address user,
uint256 reserveIndex,
bool _usingAsCollateral
) public {
UserConfiguration.setUsingAsCollateral(usersConfig, reserveIndex, _usingAsCollateral);
}
function isUsingAsCollateralOrBorrowing(
address user,
uint256 reserveIndex)
public
view
returns (bool) {
return UserConfiguration.isUsingAsCollateralOrBorrowing(usersConfig, reserveIndex);
}
function isBorrowing(
address user,
uint256 reserveIndex)
public
view
returns (bool) {
return UserConfiguration.isBorrowing(usersConfig, reserveIndex);
}
function isUsingAsCollateral(
address user,
uint256 reserveIndex)
public
view
returns (bool) {
return UserConfiguration.isUsingAsCollateral(usersConfig, reserveIndex);
}
function isBorrowingAny(
address user)
public
view
returns (bool) {
return UserConfiguration.isBorrowingAny(usersConfig);
}
function isEmpty(
address user)
public
view
returns (bool) {
return UserConfiguration.isEmpty(usersConfig);
}
/*
Mimics the original constructor of the contract.
*/
function init_state() public { }
}