Core contracts - add & group invariant checks #64

loredanacirstea · 2018-05-09T08:43:09Z

fixes #45 (overflow and underflow checks)
fixes #32 (fix nonce check in closeChannel)
fixes #47 (group invariants)
fixes #53 (unlock_amount can be 0)

Mostly groups and adds invariant checks + some tests to make sure they work as assumed.

LefterisJP · 2018-05-09T19:10:19Z

Reviewing this PR.

LefterisJP

Tests look good. But the use of require() and assert() needs some work.

LefterisJP · 2018-05-09T19:19:38Z

raiden_contracts/contracts/SecretRegistry.sol

@@ -23,7 +23,7 @@ contract SecretRegistry {
    /// @return true if secret was registered, false if the secret was already registered.
    function registerSecret(bytes32 secret) public returns (bool) {
        bytes32 secrethash = keccak256(secret);
-        if (secrethash_to_block[secrethash] > 0) {
+        if (secret == 0x0 || secrethash_to_block[secrethash] > 0) {


even though this is not part of this PR, just wanna mention we should make this fail with a revert as per this issue.

LefterisJP · 2018-05-09T19:22:09Z

raiden_contracts/contracts/TokenNetwork.sol

        // Do the transfer
-        require(token.transferFrom(msg.sender, address(this), added_deposit));
+        assert(token.transferFrom(msg.sender, address(this), added_deposit));


This should be a require(), not an assert. As per solidity's docs:

The require function should be used to ensure valid conditions, such as inputs, or contract state variables are met, or to validate return values from calls to external contracts.

Specifically note the validate return values from calls to external contracts

LefterisJP · 2018-05-09T19:23:21Z

raiden_contracts/contracts/TokenNetwork.sol


-        emit ChannelNewDeposit(channel_identifier, participant, participant_state.deposit);
+        assert(participant_state.deposit >= added_deposit);


also a require() here, not an assert. In general assert should be for something that should never ever happen under any circumstances, i.e.: internal errors.

LefterisJP · 2018-05-09T19:24:39Z

raiden_contracts/contracts/TokenNetwork.sol

-        // Signature must be from the channel partner
-        assert(partner == recovered_partner_address);
+            // Signature must be from the channel partner
+            assert(partner == recovered_partner_address);


this should be a require(), it depends on external input.

LefterisJP · 2018-05-09T19:25:07Z

raiden_contracts/contracts/TokenNetwork.sol

        // Update the balance proof data for the closing_participant
        updateBalanceProofData(channel, closing_participant, nonce, balance_hash);

        emit NonClosingBalanceProofUpdated(channel_identifier, closing_participant);

+        // Channel must be closed
+        assert(channel.state == 2);


should be a require(), depends on external input (time of call of the function)

LefterisJP · 2018-05-09T19:30:52Z

raiden_contracts/contracts/TokenNetwork.sol

        }

-        emit ChannelSettled(channel_identifier);
+        // The channel must be open
+        assert(initial_state == 1);


should be a require() as it depends on external input (time of call of the function)

LefterisJP · 2018-05-09T19:31:08Z

raiden_contracts/contracts/TokenNetwork.sol

+        assert(initial_state == 1);
+
+        // The provided addresses must be the same as the recovered ones
+        assert(participant1 == participant1_address);


should be a require() as it depends on external input (provided address)

LefterisJP · 2018-05-09T19:31:12Z

raiden_contracts/contracts/TokenNetwork.sol

+
+        // The provided addresses must be the same as the recovered ones
+        assert(participant1 == participant1_address);
+        assert(participant2 == participant2_address);


should be a require() as it depends on external input (provided address)

LefterisJP · 2018-05-09T19:33:36Z

raiden_contracts/tests/fixtures/channel.py

+        create_balance_proof,
+        create_balance_proof_update_signature
+):
+    def get(participant1, locked_amount1, locksroot1, participant2, locked_amount2, locksroot2, settle_timeout=SETTLE_TIMEOUT_MIN):


line too long, should split it

LefterisJP · 2018-05-09T19:39:12Z

raiden_contracts/tests/test_channel_unlock.py

+
+    # This should pass, even though the locked amount in storage is bigger.
+    # But those locked tokens will remain locked in the contract
+    token_network.transact().unlock(


perhaps here (and in the next test) also add a check for the token balance of the contract to check they are still locked there?

LefterisJP · 2018-05-09T19:41:23Z

Also added a tiny commit fixing a style thing and wording of a comment (make sure to pull)

LefterisJP

Some more requires vs asserts info

LefterisJP · 2018-05-10T21:54:31Z

raiden_contracts/contracts/TokenNetwork.sol

        secret_registry = SecretRegistry(_secret_registry);
        chain_id = _chain_id;
+
+        // Make sure the contract is indeed a token contract
+        assert(token.totalSupply() > 0);


This should also be a require as it depends on external input (token contract not having a total supply function).

LefterisJP · 2018-05-10T22:00:19Z

raiden_contracts/contracts/TokenNetwork.sol

@@ -478,6 +472,15 @@ contract TokenNetwork is Utils {
        participant1_amount = max(participant1_amount - participant1_locked_amount, 0);
        participant2_amount = max(participant2_amount - participant2_locked_amount, 0);

+        assert(participant1_amount <= total_deposit);


Until this morning I would have left those as asserts as it "should not happen". But I had a talk with Christian today and showed him these lines.

He said these should still be require(). Overflow here can happen if the appropriate input is given to this function. The only way this should be an assert is if we actually somehow in the code path that leads here have already checked that no overflow can happen. Iff we already did then this should be an assert here. If not a require.

The thinking is that there will be automatic tools that could be testing the program for correctness, feeding it with random input. Or trying to verify correctness through formal proofing tools. Asserts should never ever be reached under any input or conditions.

LefterisJP · 2018-05-10T22:42:56Z

raiden_contracts/contracts/TokenNetwork.sol

+
+        require(computed_locksroot != 0);
+        require(locked_amount > 0);
+        assert(locked_amount >= unlocked_amount);


Just let me see if I understand correctly. This here can be an assert since at this line we already make sure that unlocked_amount is the min of unlocked_amount and locked_amount so this should always hold true.

LefterisJP · 2018-05-10T22:44:50Z

raiden_contracts/contracts/TokenNetwork.sol

+        require(computed_locksroot != 0);
+        require(locked_amount > 0);
+        assert(locked_amount >= unlocked_amount);
+        assert(locked_amount >= returned_tokens);


If this is an overflow check for this line: returned_tokens = locked_amount - unlocked_amount;, then with the logic explained above it should still be a require()

LefterisJP · 2018-05-10T22:46:44Z

raiden_contracts/contracts/TokenNetwork.sol

+        require(participant2 == participant2_address);
+
+        // The sum of the provided balances must be equal to the total deposit
+        assert(total_deposit == (participant1_balance + participant2_balance));


With the same logic as above, this overflow check should be a require()

LefterisJP

Looks good to me now

loredanacirstea added the dev: Work In Progress label May 9, 2018

loredanacirstea added 7 commits May 9, 2018 18:46

Add check for empty secret registering

abd10f5

TokenNetwork - assert instead of require for deposit invariants

4050e40

Fix channel close with no balance proof & tests

4a52592

updateNonClosingBalanceProof invariant checks & tests

88234ab

TokenNetwork - invariant checks for unlock & settle

e8998ca

Remove registerSecret from TokenNetwork - redundant

ebc3ddc

TokenNetwork - check cooperativeSettle invariants

032a093

loredanacirstea force-pushed the contract-checks branch from ae334b4 to 032a093 Compare May 9, 2018 16:46

loredanacirstea added dev: Please Review and removed dev: Work In Progress labels May 9, 2018

loredanacirstea requested review from LefterisJP and hackaugusto May 9, 2018 16:51

loredanacirstea mentioned this pull request May 9, 2018

unlocked_amount may be 0 too. #53

Closed

loredanacirstea changed the title ~~Contract checks~~ Core contracts - add & group invariant checks May 9, 2018

LefterisJP mentioned this pull request May 9, 2018

Assess keeping invariants grouped #47

Closed

Style and wording

bb814af

LefterisJP suggested changes May 9, 2018

View reviewed changes

Fix asserts and unlock tests

d0dced7

LefterisJP suggested changes May 10, 2018

View reviewed changes

Use require instead of assert - TokenNetwork

e5a265e

LefterisJP approved these changes May 11, 2018

View reviewed changes

LefterisJP merged commit 6a20b95 into raiden-network:master May 11, 2018

loredanacirstea mentioned this pull request May 14, 2018

Add proper tests for unlock and updateTransfer #18

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Core contracts - add & group invariant checks #64

Core contracts - add & group invariant checks #64

loredanacirstea commented May 9, 2018 •

edited

Loading

LefterisJP commented May 9, 2018 •

edited

Loading

LefterisJP left a comment

LefterisJP May 9, 2018

LefterisJP May 9, 2018

LefterisJP May 9, 2018

LefterisJP May 9, 2018

LefterisJP May 9, 2018

LefterisJP May 9, 2018

LefterisJP May 9, 2018

LefterisJP May 9, 2018

LefterisJP May 9, 2018

LefterisJP May 9, 2018

LefterisJP commented May 9, 2018

LefterisJP left a comment

LefterisJP May 10, 2018 •

edited

Loading

LefterisJP May 10, 2018

LefterisJP May 10, 2018

LefterisJP May 10, 2018

LefterisJP May 10, 2018

LefterisJP left a comment


		emit ChannelNewDeposit(channel_identifier, participant, participant_state.deposit);
		assert(participant_state.deposit >= added_deposit);

Core contracts - add & group invariant checks #64

Core contracts - add & group invariant checks #64

Conversation

loredanacirstea commented May 9, 2018 • edited Loading

LefterisJP commented May 9, 2018 • edited Loading

LefterisJP left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LefterisJP commented May 9, 2018

LefterisJP left a comment

Choose a reason for hiding this comment

LefterisJP May 10, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LefterisJP left a comment

Choose a reason for hiding this comment

loredanacirstea commented May 9, 2018 •

edited

Loading

LefterisJP commented May 9, 2018 •

edited

Loading

LefterisJP May 10, 2018 •

edited

Loading