4 ms·

Formal Verification absolutely would have helped in this case. CreamFi abandoned the formal spec that Compound Finance used when they forked their code base. Ha

Formal Verification absolutely would have helped in this case. CreamFi abandoned the formal spec that Compound Finance used when they forked their code base. Had they maintained the spec and paid attention to the constraints that this spec imposes, the devs would have been aware that some of the tokens added to the platform would open them up to this attack. Had they maintained the standard, they would have been aware of this and could have notified the listing committee about this prior to the listing of these tokens. Doubly so because both currently and in the previous governance epoch the committee had members of the CreamFi team on it. https://mudit.blog/cream-hack-analysis/ https://mudit.blog/cream-hack-analysis/.

Closi 5y ago
"Paying attention to the constraints of the spec" doesn't sound like benefits of formal proof - it sounds like benefits of documentation.
- CuriousCosmic 5y ago
  Well the limitation of a spec ultimately is that they are only correct provided you follow the constraints the spec itself puts on the system. In that sense a formal spec is three parts. 1. A definition of the constraints of the system. These constraints are "outside" the system and if they are violated, the properties of the system will not hold. This part boils down to clear and dis-ambiguous documentation on the constraints of the system as well as some tooling to help verify the constraints are held (not always possible). 2. A definition of the system itself. This defines the rules and operations within the system as well as formal methods to prove the correctness of this system. Provided this definition is shown to be consistent, as long as the constraints (part 1) are held true, the system is secure. 3. The code itself. Projects have to choose between either writing the code and using formal methods to verify functional equivalence between the code and the system (faster but harder) or using a code generator to produce a runtime directly generated from the system definition. --- The code (part 3) is only secure if there's a full one to one map between it and the system definition(part 2). The system definition (part 2) is only secure if all the constraints (part 1) are upheld. You can verify parts 2 and 3 automatically but in many cases you won't be able to verify all of part 1 automatically. This attack relied on the fact that one of the tokens was atomically volatile (allowing the attacker to manipulate funds in a single atomic step increasing the price up to whatever price and risking nothing if they are unsuccessful). The previous exploit was due to the listing of another liquidity pool token that allowed reentrancy. This allowed the two pools to repeatedly interact with each other inside of each other's code bypassing various state checks. CreamFi failed in two places. One the devs stopped maintaining the spec after forking the protocol off the original Compound Finance protocol so even if they had held the constraints, they had added features that haven't been considered with regard to the formal security of the system. Two (and more importantly) the listing committee (responsible for introducing new tokens) wasn't aware of the constraints of the system.

Closi 5y ago

"Paying attention to the constraints of the spec" doesn't sound like benefits of formal proof - it sounds like benefits of documentation.

CuriousCosmic 5y ago
Well the limitation of a spec ultimately is that they are only correct provided you follow the constraints the spec itself puts on the system. In that sense a formal spec is three parts. 1. A definition of the constraints of the system. These constraints are "outside" the system and if they are violated, the properties of the system will not hold. This part boils down to clear and dis-ambiguous documentation on the constraints of the system as well as some tooling to help verify the constraints are held (not always possible). 2. A definition of the system itself. This defines the rules and operations within the system as well as formal methods to prove the correctness of this system. Provided this definition is shown to be consistent, as long as the constraints (part 1) are held true, the system is secure. 3. The code itself. Projects have to choose between either writing the code and using formal methods to verify functional equivalence between the code and the system (faster but harder) or using a code generator to produce a runtime directly generated from the system definition. --- The code (part 3) is only secure if there's a full one to one map between it and the system definition(part 2). The system definition (part 2) is only secure if all the constraints (part 1) are upheld. You can verify parts 2 and 3 automatically but in many cases you won't be able to verify all of part 1 automatically. This attack relied on the fact that one of the tokens was atomically volatile (allowing the attacker to manipulate funds in a single atomic step increasing the price up to whatever price and risking nothing if they are unsuccessful). The previous exploit was due to the listing of another liquidity pool token that allowed reentrancy. This allowed the two pools to repeatedly interact with each other inside of each other's code bypassing various state checks. CreamFi failed in two places. One the devs stopped maintaining the spec after forking the protocol off the original Compound Finance protocol so even if they had held the constraints, they had added features that haven't been considered with regard to the formal security of the system. Two (and more importantly) the listing committee (responsible for introducing new tokens) wasn't aware of the constraints of the system.