3 ms·

> People are learning though. See Cardano and their choice of Haskell and emphasis on formal verification. Formal verification absolutely would not have helped

• CuriousCosmic 5y ago
  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.
• mint2 5y ago
  Things formal verification will not do: fix Poorly conceived business rules, prevent confusing UI, quickly modify code to adapt to rapidly changing circumstances, etc… One could formally verify that if the account number is set in the wash account (plus like six other places) then the loan won’t be repaid due to programming errors. But formal verification doesn’t tell one that the UI is garbage and hard to know that the account number needs entered in six places to get the correct formally verified action to occur instead of the other formally verified action that repays the loan in full.