From 17aeacf768f90f54f5706f1d0662322b7e51f2da Mon Sep 17 00:00:00 2001 From: Junkil Park Date: Wed, 14 Sep 2022 02:55:53 -0700 Subject: [PATCH] Limit the upper bound of `rewards_rate` This commit adds assertions and a spec to ensure `rewards_rate <= 10000`, and `rewards_rate <= rewards_rate_denominator`. --- Cargo.lock | 2 +- .../sources/configs/staking_config.move | 20 ++++++++++++++++++- .../sources/configs/staking_config.spec.move | 8 ++++++++ .../aptos-framework/sources/stake.move | 12 +++++++++++ .../aptos-framework/sources/stake.spec.move | 17 +++++++++++----- 5 files changed, 52 insertions(+), 7 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 15eeabb18ded4..8150588ebe6d7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -6454,7 +6454,7 @@ dependencies = [ "aptos-infallible", "aptos-logger", "aptos-metrics-core", - "cfg-if 1.0.0", + "cfg-if", "once_cell", "procfs", "prometheus", diff --git a/aptos-move/framework/aptos-framework/sources/configs/staking_config.move b/aptos-move/framework/aptos-framework/sources/configs/staking_config.move index 7479430012928..a069a1be2e8ae 100644 --- a/aptos-move/framework/aptos-framework/sources/configs/staking_config.move +++ b/aptos-move/framework/aptos-framework/sources/configs/staking_config.move @@ -14,9 +14,11 @@ module aptos_framework::staking_config { const EINVALID_STAKE_RANGE: u64 = 3; /// The voting power increase limit percentage must be within (0, 50]. const EINVALID_VOTING_POWER_INCREASE_LIMIT: u64 = 4; - /// Specified rewards rate is invalid, which must be within [0, 100). + /// Specified rewards rate is invalid, which must be within [0, MAX_REWARDS_RATE]. const EINVALID_REWARDS_RATE: u64 = 5; + /// Limit the maximum value of `rewards_rate` in order to avoid any arithmetic overflow. + const MAX_REWARDS_RATE: u64 = 10000; /// Validator set configurations that will be stored with the @aptos_framework account. struct StakingConfig has copy, drop, key { @@ -68,6 +70,14 @@ module aptos_framework::staking_config { error::invalid_argument(EINVALID_VOTING_POWER_INCREASE_LIMIT), ); + // `rewards_rate` which is the numerator is limited to be `<= MAX_REWARDS_RATE` in order to avoid the arithmetic + // overflow in the rewards calculation. `rewards_rate_denominator` can be adjusted to get the desired rewards + // rate (i.e., rewards_rate / rewards_rate_denominator). + assert!(rewards_rate <= MAX_REWARDS_RATE, error::invalid_argument(EINVALID_REWARDS_RATE)); + + // We assert that (rewards_rate / rewards_rate_denominator <= 1). + assert!(rewards_rate <= rewards_rate_denominator, error::invalid_argument(EINVALID_REWARDS_RATE)); + move_to(aptos_framework, StakingConfig { minimum_stake, maximum_stake, @@ -149,6 +159,14 @@ module aptos_framework::staking_config { new_rewards_rate_denominator > 0, error::invalid_argument(EZERO_REWARDS_RATE_DENOMINATOR), ); + // `rewards_rate` which is the numerator is limited to be `<= MAX_REWARDS_RATE` in order to avoid the arithmetic + // overflow in the rewards calculation. `rewards_rate_denominator` can be adjusted to get the desired rewards + // rate (i.e., rewards_rate / rewards_rate_denominator). + assert!(new_rewards_rate <= MAX_REWARDS_RATE, error::invalid_argument(EINVALID_REWARDS_RATE)); + + // We assert that (rewards_rate / rewards_rate_denominator <= 1). + assert!(new_rewards_rate <= new_rewards_rate_denominator, error::invalid_argument(EINVALID_REWARDS_RATE)); + let staking_config = borrow_global_mut(@aptos_framework); staking_config.rewards_rate = new_rewards_rate; staking_config.rewards_rate_denominator = new_rewards_rate_denominator; diff --git a/aptos-move/framework/aptos-framework/sources/configs/staking_config.spec.move b/aptos-move/framework/aptos-framework/sources/configs/staking_config.spec.move index 374a0bdafc6fa..f0ad3e908317b 100644 --- a/aptos-move/framework/aptos-framework/sources/configs/staking_config.spec.move +++ b/aptos-move/framework/aptos-framework/sources/configs/staking_config.spec.move @@ -3,4 +3,12 @@ spec aptos_framework::staking_config { use aptos_framework::chain_status; invariant chain_status::is_operating() ==> exists(@aptos_framework); } + spec StakingConfig { + // `rewards_rate` which is the numerator is limited to be `<= MAX_REWARDS_RATE` in order to avoid the arithmetic + // overflow in the rewards calculation. `rewards_rate_denominator` can be adjusted to get the desired rewards + // rate (i.e., rewards_rate / rewards_rate_denominator). + invariant rewards_rate <= MAX_REWARDS_RATE; + invariant rewards_rate_denominator > 0; + invariant rewards_rate <= rewards_rate_denominator; + } } diff --git a/aptos-move/framework/aptos-framework/sources/stake.move b/aptos-move/framework/aptos-framework/sources/stake.move index 2a688633412a3..593b52852d259 100644 --- a/aptos-move/framework/aptos-framework/sources/stake.move +++ b/aptos-move/framework/aptos-framework/sources/stake.move @@ -83,6 +83,12 @@ module aptos_framework::stake { /// https://github.com/aptos-labs/aptos-core/blob/main/crates/aptos-bitvec/src/lib.rs#L20 const MAX_VALIDATOR_SET_SIZE: u64 = 65536; + /// Limit the maximum value of `rewards_rate` in order to avoid any arithmetic overflow. + const MAX_REWARDS_RATE: u64 = 10000; + + /// The maximum value of u64 as u128. + const MAX_U64: u128 = 18446744073709551615; + /// Capability that represents ownership and can be used to control the validator and the associated stake pool. /// Having this be separate from the signer for the account that the validator resources are hosted at allows /// modules to have control over a validator. @@ -1158,6 +1164,12 @@ module aptos_framework::stake { rewards_rate: u64, rewards_rate_denominator: u64, ): u64 { + spec { + assume num_successful_proposals <= num_total_proposals; + // We assume that num_successful_proposals < 86400 (1 proposal per second in a day). + // Even in the worst case, the following condition must hold. + assume num_successful_proposals * MAX_REWARDS_RATE <= MAX_U64; + }; // The rewards amount is equal to (stake amount * rewards rate * performance multiplier). // We do multiplication in u128 before division to avoid the overflow and minimize the rounding error. let rewards_numerator = (stake_amount as u128) * (rewards_rate as u128) * (num_successful_proposals as u128); diff --git a/aptos-move/framework/aptos-framework/sources/stake.spec.move b/aptos-move/framework/aptos-framework/sources/stake.spec.move index eecdf47f20473..9271a98beaa69 100644 --- a/aptos-move/framework/aptos-framework/sources/stake.spec.move +++ b/aptos-move/framework/aptos-framework/sources/stake.spec.move @@ -53,6 +53,9 @@ spec aptos_framework::stake { spec distribute_rewards { include ResourceRequirement; + requires rewards_rate <= MAX_REWARDS_RATE; + requires rewards_rate_denominator > 0; + requires rewards_rate <= rewards_rate_denominator; aborts_if false; ensures old(stake.value) > 0 ==> result == spec_rewards_amount( @@ -74,13 +77,17 @@ spec aptos_framework::stake { spec calculate_rewards_amount { pragma opaque; + requires rewards_rate <= MAX_REWARDS_RATE; + requires rewards_rate_denominator > 0; + requires rewards_rate <= rewards_rate_denominator; ensures [concrete] (rewards_rate_denominator * num_total_proposals == 0) ==> result == 0; - ensures [concrete] (rewards_rate_denominator * num_total_proposals > 0) ==> - result == ((stake_amount * rewards_rate * num_successful_proposals) / + ensures [concrete] (rewards_rate_denominator * num_total_proposals > 0) ==> { + let amount = ((stake_amount * rewards_rate * num_successful_proposals) / (rewards_rate_denominator * num_total_proposals)); - // We assume that rewards_rate < 100 and num_successful_proposals < 86400 (1 proposal per second in a day). - // So, the multiplication in the reward formula should not overflow. - aborts_if [abstract] false; + result == amount + }; + aborts_if false; + // Used an uninterpreted spec function to avoid dealing with the arithmetic overflow and non-linear arithmetic. ensures [abstract] result == spec_rewards_amount( stake_amount,