[IOTX Verification] Add CertiK Formal Verification Smart labels

iotexproject · May 6, 2018 · 80982ac · 80982ac
1 parent b45f6e1
commit 80982ac
Show file tree

Hide file tree

Showing 6 changed files with 171 additions and 5 deletions.
diff --git a/contracts/IoTeXNetwork.sol b/contracts/IoTeXNetwork.sol
@@ -24,28 +24,80 @@ contract IoTeXNetwork is StandardToken, Pausable {
         emit Transfer(address(0x0), msg.sender, tokenTotalAmount);
     }
 
+    /*@CTK CtkTransferNoEffect
+      @post (_to == address(0)) \/ (paused == true) -> __reverted == true
+     */
+    /*@CTK CtkTransferEffect
+      @pre __reverted == false
+      @pre balances[msg.sender] >= _value
+      @pre paused == false
+      @pre __return == true
+      @pre msg.sender != _to
+      @post __post.balances[_to] == balances[_to] + _value
+      @post __has_overflow == false
+     */
+    /* CertiK Smart Labelling, for more details visit: https://certik.org */
     function transfer(address _to, uint _value) whenNotPaused
         validDestination(_to)
         returns (bool) {
         return super.transfer(_to, _value);
     }
 
+    /*@CTK CtkTransferFromNoEffect
+      @post (_to == address(0)) \/ (paused == true) -> __reverted == true
+     */
+    /*@CTK CtkTransferFromEffect
+      @tag assume_completion
+      @pre _from != _to
+      @post __post.balances[_to] == balances[_to] + _value
+      @post __post.balances[_from] == balances[_from] - _value
+      @post __has_overflow == false
+     */
+    /* CertiK Smart Labelling, for more details visit: https://certik.org */
     function transferFrom(address _from, address _to, uint _value) whenNotPaused
         validDestination(_to)
         returns (bool) {
         return super.transferFrom(_from, _to, _value);
     }
 
+    /*@CTK CtkApproveNoEffect
+      @post (paused == true) -> __post == this
+     */
+    /*@CTK CtkApprove
+      @tag assume_completion
+      @post __post.allowed[msg.sender][_spender] == _value
+     */
+    /* CertiK Smart Labelling, for more details visit: https://certik.org */
     function approve(address _spender, uint256 _value) public whenNotPaused
       returns (bool) {
       return super.approve(_spender, _value);
     }
 
+    /*@CTK CtkIncreaseApprovalNoEffect
+      @post (paused == true) -> __reverted == true
+     */
+    /*@CTK CtkIncreaseApprovalEffect
+      @pre paused == false
+      @tag assume_completion
+      @post __post.allowed[msg.sender][_spender] == allowed[msg.sender][_spender] + _addedValue
+      @post __has_overflow == false
+     */
+    /* CertiK Smart Labelling, for more details visit: https://certik.org */
     function increaseApproval(address _spender, uint _addedValue) public whenNotPaused
       returns (bool success) {
       return super.increaseApproval(_spender, _addedValue);
     }
 
+    /*@CTK CtkDecreaseApprovalNoEffect
+      @post (paused == true) -> __reverted == true
+     */
+    /*@CTK CtkDecreaseApprovalEffect
+      @pre allowed[msg.sender][_spender] >= _subtractedValue
+      @tag assume_completion
+      @post __post.allowed[msg.sender][_spender] == allowed[msg.sender][_spender] - _subtractedValue
+      @post __has_overflow == false
+     */
+    /* CertiK Smart Labelling, for more details visit: https://certik.org */
     function decreaseApproval(address _spender, uint _subtractedValue) public whenNotPaused
       returns (bool success) {
       return super.decreaseApproval(_spender, _subtractedValue);

diff --git a/contracts/Migrations.sol b/contracts/Migrations.sol
@@ -8,10 +8,19 @@ contract Migrations {
     if (msg.sender == owner) _;
   }
 
+  /*@CTK init_migrations
+    @post __post.owner == msg.sender
+   */
+  /* CertiK Smart Labelling, for more details visit: https://certik.org */
   function Migrations() public {
     owner = msg.sender;
   }
 
+  /*@CTK set_complete
+    @pre msg.sender == owner
+    @post __post.last_completed_migration == completed
+   */
+  /* CertiK Smart Labelling, for more details visit: https://certik.org */
   function setCompleted(uint completed) public restricted {
     last_completed_migration = completed;
   }
@@ -20,4 +29,4 @@ contract Migrations {
     Migrations upgraded = Migrations(new_address);
     upgraded.setCompleted(last_completed_migration);
   }
-}
+}
diff --git a/contracts/math/SafeMath.sol b/contracts/math/SafeMath.sol
@@ -10,6 +10,15 @@ library SafeMath {
   /**
   * @dev Multiplies two numbers, throws on overflow.
   */
+
+  /*@CTK SafeMath_mul
+    @tag spec
+    @post __reverted == __has_assertion_failure
+    @post __has_assertion_failure == __has_overflow
+    @post __reverted == false -> c == a * b
+    @post msg == msg__post
+   */
+  /* CertiK Smart Labelling, for more details visit: https://certik.org */
   function mul(uint256 a, uint256 b) internal pure returns (uint256 c) {
     if (a == 0) {
       return 0;
@@ -22,6 +31,15 @@ library SafeMath {
   /**
   * @dev Integer division of two numbers, truncating the quotient.
   */
+  /*@CTK SafeMath_div
+    @tag spec
+    @pre b != 0
+    @post __reverted == __has_assertion_failure
+    @post __has_overflow == true -> __has_assertion_failure == true
+    @post __reverted == false -> __return == a / b
+    @post msg == msg__post
+   */
+  /* CertiK Smart Labelling, for more details visit: https://certik.org */
   function div(uint256 a, uint256 b) internal pure returns (uint256) {
     // assert(b > 0); // Solidity automatically throws when dividing by 0
     // uint256 c = a / b;
@@ -32,6 +50,14 @@ library SafeMath {
   /**
   * @dev Subtracts two numbers, throws on overflow (i.e. if subtrahend is greater than minuend).
   */
+  /*@CTK SafeMath_sub
+    @tag spec
+    @post __reverted == __has_assertion_failure
+    @post __has_overflow == true -> __has_assertion_failure == true
+    @post __reverted == false -> __return == a - b
+    @post msg == msg__post
+   */
+  /* CertiK Smart Labelling, for more details visit: https://certik.org */
   function sub(uint256 a, uint256 b) internal pure returns (uint256) {
     assert(b <= a);
     return a - b;
@@ -40,9 +66,17 @@ library SafeMath {
   /**
   * @dev Adds two numbers, throws on overflow.
   */
+  /*@CTK SafeMath_add
+    @tag spec
+    @post __reverted == __has_assertion_failure
+    @post __has_assertion_failure == __has_overflow
+    @post __reverted == false -> c == a + b
+    @post msg == msg__post
+   */
+  /* CertiK Smart Labelling, for more details visit: https://certik.org */
   function add(uint256 a, uint256 b) internal pure returns (uint256 c) {
     c = a + b;
     assert(c >= a);
     return c;
   }
-}
+}
diff --git a/contracts/ownership/Ownable.sol b/contracts/ownership/Ownable.sol
@@ -17,6 +17,10 @@ contract Ownable {
    * @dev The Ownable constructor sets the original `owner` of the contract to the sender
    * account.
    */
+  /*@CTK owner_set_on_success
+    @pre __reverted == false -> __post.owner == owner
+   */
+  /* CertiK Smart Labelling, for more details visit: https://certik.org */
   function Ownable() public {
     owner = msg.sender;
   }
@@ -33,10 +37,16 @@ contract Ownable {
    * @dev Allows the current owner to transfer control of the contract to a newOwner.
    * @param newOwner The address to transfer ownership to.
    */
+  /*@CTK transferOwnership
+    @post __reverted == false -> (msg.sender == owner -> __post.owner == newOwner)
+    @post (owner != msg.sender) -> (__reverted == true)
+    @post (newOwner == address(0)) -> (__reverted == true)
+   */
+  /* CertiK Smart Labelling, for more details visit: https://certik.org */
   function transferOwnership(address newOwner) public onlyOwner {
     require(newOwner != address(0));
     emit OwnershipTransferred(owner, newOwner);
     owner = newOwner;
   }
 
-}
+}
diff --git a/contracts/token/BasicToken.sol b/contracts/token/BasicToken.sol
@@ -28,6 +28,25 @@ contract BasicToken is ERC20Basic {
   * @param _to The address to transfer to.
   * @param _value The amount to be transferred.
   */
+  /*@CTK transfer_success
+    @pre _to != address(0)
+    @pre balances[msg.sender] >= _value
+    @pre __reverted == false
+    @post __reverted == false
+    @post __return == true
+   */
+  /*@CTK transfer_same_address
+    @tag no_overflow
+    @pre _to == msg.sender
+    @post this == __post
+   */
+  /*@CTK transfer_conditions
+    @tag assume_completion
+    @pre _to != msg.sender
+    @post __post.balances[_to] == balances[_to] + _value
+    @post __post.balances[msg.sender] == balances[msg.sender] - _value
+   */
+  /* CertiK Smart Labelling, for more details visit: https://certik.org */
   function transfer(address _to, uint256 _value) public returns (bool) {
     require(_to != address(0));
     require(_value <= balances[msg.sender]);
@@ -43,8 +62,13 @@ contract BasicToken is ERC20Basic {
   * @param _owner The address to query the the balance of.
   * @return An uint256 representing the amount owned by the passed address.
   */
+  /*@CTK balanceOf
+    @post __reverted == false
+    @post __return == balances[_owner]
+   */
+  /* CertiK Smart Labelling, for more details visit: https://certik.org */
   function balanceOf(address _owner) public view returns (uint256) {
     return balances[_owner];
   }
 
-}
+}
diff --git a/contracts/token/StandardToken.sol b/contracts/token/StandardToken.sol
@@ -22,6 +22,15 @@ contract StandardToken is ERC20, BasicToken {
    * @param _to address The address which you want to transfer to
    * @param _value uint256 the amount of tokens to be transferred
    */
+  /*@CTK transferFrom
+    @tag assume_completion
+    @pre _from != _to
+    @post __return == true
+    @post __post.balances[_to] == balances[_to] + _value
+    @post __post.balances[_from] == balances[_from] - _value
+    @post __has_overflow == false
+   */
+  /* CertiK Smart Labelling, for more details visit: https://certik.org */
   function transferFrom(address _from, address _to, uint256 _value) public returns (bool) {
     require(_to != address(0));
     require(_value <= balances[_from]);
@@ -44,6 +53,15 @@ contract StandardToken is ERC20, BasicToken {
    * @param _spender The address which will spend the funds.
    * @param _value The amount of tokens to be spent.
    */
+  /*@CTK approve_success
+    @post _value == 0 -> __reverted == false
+    @post allowed[msg.sender][_spender] == 0 -> __reverted == false
+   */
+  /*@CTK approve
+    @tag assume_completion
+    @post __post.allowed[msg.sender][_spender] == _value
+   */
+  /* CertiK Smart Labelling, for more details visit: https://certik.org */
   function approve(address _spender, uint256 _value) public returns (bool) {
     allowed[msg.sender][_spender] = _value;
     emit Approval(msg.sender, _spender, _value);
@@ -70,6 +88,12 @@ contract StandardToken is ERC20, BasicToken {
    * @param _spender The address which will spend the funds.
    * @param _addedValue The amount of tokens to increase the allowance by.
    */
+  /*@CTK CtkIncreaseApprovalEffect
+    @tag assume_completion
+    @post __post.allowed[msg.sender][_spender] == allowed[msg.sender][_spender] + _addedValue
+    @post __has_overflow == false
+   */
+  /* CertiK Smart Labelling, for more details visit: https://certik.org */
   function increaseApproval(address _spender, uint _addedValue) public returns (bool) {
     allowed[msg.sender][_spender] = allowed[msg.sender][_spender].add(_addedValue);
     emit Approval(msg.sender, _spender, allowed[msg.sender][_spender]);
@@ -86,6 +110,19 @@ contract StandardToken is ERC20, BasicToken {
    * @param _spender The address which will spend the funds.
    * @param _subtractedValue The amount of tokens to decrease the allowance by.
    */
+  /*@CTK CtkDecreaseApprovalEffect_1
+    @pre allowed[msg.sender][_spender] >= _subtractedValue
+    @tag assume_completion
+    @post __post.allowed[msg.sender][_spender] == allowed[msg.sender][_spender] - _subtractedValue
+    @post __has_overflow == false
+   */
+   /*@CTK CtkDecreaseApprovalEffect_2
+    @pre allowed[msg.sender][_spender] < _subtractedValue
+    @tag assume_completion
+    @post __post.allowed[msg.sender][_spender] == 0
+    @post __has_overflow == false
+   */
+  /* CertiK Smart Labelling, for more details visit: https://certik.org */
   function decreaseApproval(address _spender, uint _subtractedValue) public returns (bool) {
     uint oldValue = allowed[msg.sender][_spender];
     if (_subtractedValue > oldValue) {
@@ -97,4 +134,4 @@ contract StandardToken is ERC20, BasicToken {
     return true;
   }
 
-}
+}