Function redeem(ERC20Bondtoken token_, uint256 amount_)

1. Intended behavior.

   The function should enable users to redeem matured bond tokens issued by Bond Protocol for the vested underlying tokens. Acts like redeeming the rewards basically.

2. Negative behavior.

   • Don’t redeem bonds which have not reached maturity

   • Don’t redeem “counterfeit” bonds that aren’t issued by Bond Protocol

   • Do not give out too many or too little underlying tokens

   • Don’t give out the wrong underlying token

   • Don’t give or take tokens from the wrong user

3. Preconditions.

   • The user has locked underlying tokens with the teller and received bond tokens in return.

   • The bonds have reached maturity.

4. Postconditions.

   • The user is now greater N underlying tokens.

   • The user is now less N bond tokens.

5. Inputs.

   • token_: Full control (!). checked such that a bondToken exists for it.

   • amount_: Full control (!). no checks (!). However, invalid values will cause a revert (proven with unit test)

   • msg.sender: Can be any external sender, contract or EOA, no checks (!). Not an issue if msg.sender is external, but may be weird if msg.sender is the Teller itself

   • block.timestamp: Could be any time in the future (overapproximation). checked against token_.expiry()

6. Examine all function calls the function makes.

   a. Call to token_.expiry()

   • What is controllable: Fully controllable (callee is attacker supplied, can be any contract)

   • If return value controllable, how is it used and how can it go wrong: Bypasses block.timestamp maturity check.

   • What happens if it reverts or tries to reenter: No problem.

   b. Call to token_.burn()

   • What is controllable: Fully controllable (callee is attacker supplied, can be any contract)

   • If return value controllable, how is it used and how can it go wrong: N/A, return value is discarded.

   • What happens if it reverts or tries to reenter: No problem.

   c. Call to token_.underlying()

   • What is controllable: Fully controllable (callee is attacker supplied, can be any contract)

   • If return value controllable, how is it used and how can it go wrong: Attacker will control what underlying token is transferred.

   • What happens if it reverts or tries to reenter: No problem.

   d. Call to token_.underlying().transfer()

   • What is controllable: Fully controllable (callee is attacker supplied, can be any contract)

   • If return value controllable, how is it used and how can it go wrong: N/A, return value is discarded.

   • What happens if it reverts or tries to reenter: No problem.