The risk of events like this one is fundamental to DeFi right? How can people still think that it's the future? Or even remotely better than the banking system we currently have?
DeFi allows for a lot of unique and flexible things...and people are re-discovering that writing bullet proof code in such an environment is really really hard. i.e. No training wheels and lots of footguns available
>How can people still think that it's the future?
I'd view these events more as growing pains of a complex technology rather than an indication that it has no future.
People are learning though. See Cardano and their choice of Haskell and emphasis on formal verification.
If someone steals from my credit account, I Trust my financial institution to undo it.
Trustless systems are overrated when you have trustworthy institutions.
Quite. But what if you don't have access to trustworthy institutions? Or what if you need to coordinate between trustworthy institutions that either don't work together or don't share mutual trust? What if you distrust the very currency the institution does business with?
Your point is correct. If you trust the institutions all the way down, trustless is complicated and unnecessary. If you don't trust the institutions, what are your other options?
It sounds like people trusted CREAM with their money, and shouldn't have. Not as trustless as you might hope.
If the devs have written formal models for the system and verified that with a proof solver, you have a reasonable assurance the code matches the spec and that the spec is at least consistent with itself.
If the devs have Property Based Testing suites and fuzzing tools to automatically search for vulnerabilities in the code/spec or introduced via changes, you have reasonable assurances that the development process is thorough and likely won't haphazardly introduce a vulnerability in a change (and actively squash potential vulns that are discovered).
If open source security auditors (who's reputation is core to their business) regularly and publicly auditing the platform, you have reasonable assurances that on top of the code being reasonably secure, the spec itself doesn't have any glaring flaws in it.
If bug bounties have red teams regularly trying to discover exploits, you have additional assurance that if a bug exists, it'll likely be discovered, ethically reported, and resolved before being exploited.
Point being, zero trust isn't about not having trust, it's about not having blind trust. These should be the expectation for all high value software. We should be able to trust in the engineering of software systems like we trust in the engineering behind buildings and bridges.
---
Now with regard to this specific hack, CreamFi failed to do 2 out of the 4 of those things mentioned above and their security auditor only provided a very cursory/high level audit. Their report was not confidence inspiring and should have been a red flag to users to not use the service.
Now compare this with the org they forked their code off of. Compound Finance maintains a formal spec, uses formal methods, has a bug bounty, and receives regular, in depth security audits. CreamFi chose to make changes to a codebase after abandoning the security tooling (formal spec was no longer maintained) and protections that were in place with Compound Finance's code.
Any moderately competent technical user should have been able to tell that CreamFi was (like many other knock-off DeFi platforms) a ticking time bomb. We as a software engineering community however still have a long way to go in making these qualities/flags accessible to normal users.
I understand the practical argument (code is easier to audit and more reliable), I'm just not sure how the sum total of the ecosystem is better when, as a practical matter, crappy smart contracts keep losing depositors' money, and depositors keep trusting the wrong contracts.
For developed nations, we'll see Central Bank Digital Currencies slowly replace the existing financial network. You can still get your flexible monetary policy, regulatory compliance, and reversible transactions with a CBDC. The additional benefit is that now instead of having a bunch of centralised, discontiguous, and opaque services for transferring funds, now you have a decentralised, unified, and transparent network for doing this. Additionally, smart contract or smart validator functionality allows you to move some of the traditionally centralised financial logic up into this transparent & decentralised space while still maintaining all the legal protections you'd have otherwise.
Side note: I say decentralised here because ideally CBDCs will use some Proof of Authority system with the various states/provinces/counties/parishes/districts/etc each running validators. The idea here being that you still retain full control by the nation however it now becomes exceedingly difficult for any one person to manipulate the network without the consent/awareness of many other officials.
Now how about developing nations? Many of these nations lack a stable or trusted financial sector. Their people don't trust the officials, the offices, or the policies. These people are the main users of the truly decentralised networks. Of course the risk of crappy smart contracts losing your money is a risk (and assurance/accreditation programs are working to improve the visibility of well designed & operated contracts). The question however is whether that risk is greater or lesser than the risks or costs of using traditional financial institutions in these regions (if the people can even get access to them).
That said I just don't see a lot of the value in a lot of "DeFi" at the moment. A lot of it exists solely as vehicles to allow people to move more money around at a time so that they can take bigger leveraged risks on the market. Now there are useful applications in the space however many are still small and finding their footing.
The majority of supply chain/production traceability solutions and identity solutions in the space are really just two sides of the same coin and serve the purpose of providing a decentralised (or at minimum federated) source of reputation for people and businesses where the local government fails to. Identity solutions provide a means for people in these nations to "prove" their credentials/reputation to gain access to low-to-reasonable interest rate loans or prove their credentials to potential employers. Likewise they provide a means for businesses to provide a history for their products which helps them sell their products at closer to the international market rate (compared to being forced to sell to the big corporation in their region that turns around and resells to the rest of the world).
Lending and Micro-lending platforms provide a means for people in these regions to get access to loans (denominated in their local currency) at rates they would otherwise not be able to get access to. People or organisations in higher QoL/CoL nations/regions can provide liquidity to these services and users in these developing regions can slowly get access to larger & lower interest loans over time by building up their "credit history"/reputation tied to their identity. In developed nations we have systems for this already but many developing nations lack such a service that is accessible to many of their people (and that is trusted). These services still have a long way to go but as the previously mentioned digital identity solutions become more available, this space should start to see some significant improvements in usability & trust.
I'll stop at that because I've already gone way past what I intended to write up (I was also considering going into detail about decentralised good & services marketplaces) but my point being that while there's a lot of issues with smart contracts, the systems provide a means for institutions to rebuild trust by using systems that prevent or at least greatly reduce the potential for abuse or lying by those institutions (or other individuals).
TL;DR: In developed nations CBDCs unify the financial space without compromising on any features of the existing system and at the same time reduce the surface area for illicit activity or attacks on financial institutions. In developing nations however fully decentralised cryptocurrencies provide a fabric for existing institutions to rebuild the trust of their people and international trust therefore increasing their people's and businesses' access to economic opportunities both domestically and internationally.
* https://rekt.news/compound-rekt/
* HN discussion: https://news.ycombinator.com/item?id=28716979
The Compound Finance paper spec essentially just lists "this subsystem does these things" and then each function/operation is a list of preconditions, what actions are taken in what conditions, and the expected result. This isn't bad per se but it's not great either. Instead the paper spec really should be showing what transformation is being applied to the state, why we want that transformation applied, what properties must hold throughout the transformation, and then demonstrating that those properties hold.
Compare this (Compound):
https://github.com/compound-finance/compound-protocol/blob/m... https://github.com/compound-finance/compound-protocol/tree/m...
to this (Uniswap):
https://github.com/runtimeverification/verified-smart-contra... https://github.com/runtimeverification/verified-smart-contra...
or this (Djed):
https://eprint.iacr.org/2021/1069.pdf
The first just describes the system and then asserts preconditions hold which works well enough for verifying that the code matches the spec but the other actually verify that the spec is doing what the user & developer expect it to by formalising the system and analysing the properties of that system.
Compound's project wouldn't have been vulnerable to any of the attacks executed on CreamFi however they are vulnerable to the class of spec errors. Uniswap and Djed on the other hand would be protected from the majority of that class of issue that Compound experienced. This isn't to say that they are invulnerable but I'd be willing to say that they are approaching "cryptography-grade" security where you can trust these protocols just like you can trust AES, RSA, and ECC encryption & signing.
---
This of course isn't to say that what Compound does is bad but as that incident shows, there is still room for their improvement in the security space. Cryptocurrency and "Decentralised Finance" are finally starting to grow up into proper subsets of the cryptocurrency and game theory communities. Now this might be a bit of general commentary on the SW space but hopefully long term this trend causes some of this security minded design to bleed over into the greater software engineering community.
Formal verification absolutely would not have helped in this case.
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.
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.
The risk of investing in stocks is always that the underlying companies could have their business ruined overnight for any reason. The risk of swaps is always that the counterparty could go bust and be unable to pay you even if your bet pays off (see Lehman Brothers). The risk of leveraged futures positions is you can get liquidated on fat finger trades or flash crashes. The risk of structured credit products like CLOs or mortgage backed securities is that the pool is fraudulent. The risk of many quant strategies is that the correlations go to one and your capital gets wiped out as your hedges fail to protect you.
Do any of these risks mean those asset classes are doomed? No, all of the above asset classes are bigger than ever. Markets can and do live with disastrous risk looming over their heads all the time. Unless your name is Nassim Taleb, the reality is that you mitigate the risks you can, model out the risks that you cannot, then price the asset accordingly. The foundation of modern finance is “we don’t have to live in mortal fear of risk if we’re smart about it”
If inherent risk was an insurmountable barrier to the existence of a financial product, then I guarantee you the financial system would just be the old-timely community bankers like in It’s a Wonderful Life.
All of these systems are complex black boxes, for which the full risk profile can never be fully known let alone eliminated. Yet all of these asset classes continue to reach record size. For the foreseeable future, risk is not a meaningful constraint on financial activity or the growth of any otherwise profitable sector.
Global capital is insanely hungry for yield. It’s willing to accept very large, outsized risks as long as returns are attractive. DeFi continues to grow because it offers significantly higher top-line returns than traditional products. As long as that continues to be true, investors will stomach, and in many cases outright ignore, the risks.
Do they "truly" believe it themselves, or are they just rational actors well aware that they lose a lot of money if people stop listening to them? No way to know.
If I have a balance on a DeFi platform, it's vulnerable to attacks like the one in the original article. If I have a balance in a bank, this isn't the case. The risks aren't the same at all. Not the same type of risk, not the same magnitude of risk.