Although neither of these things will actually help if your contract gets exploited before you can push a fix.
As we get proven/tested/formally verified code that implements governance protocols we can use that code to build system of allowing upgrades while allowing those who disagree to exit the system.
For example, one of the ZKRollup chains has a mechanism for upgrading that requires a small number of approvers for the “break glass” scenario. When an upgrade is approved, anyone can exit the network before the upgrade takes affect and move to a system with rules they support.
Governance models will evolve as we figure out what works and what doesn’t. Some people may be ok with a super majority being able to revert the state of a contract in response to a bug while others will want immutability at all costs.
Blockchain/cryptocurrency is about each participant deciding how much trust they are ok with, and having an open ecosystem where assets can be moved to systems that people want to use.
https://www.forbes.com/sites/kevindowd/2021/06/06/private-eq...
You can make powerful systems with simple correct independent components. You can not make complex secure monolithic systems. It gets even worse when you look at contracts with delegation.
The problem with most "smart" contracts is they have abstractions, delegation and scope creep.
You'll potentially have less of a chance for contracts to be exploited (at least compared to what we have now).
That said, you can't protect against infrastructure exploits as easily, mathematically flawless program or not.
My former professor (RIP) oversaw the formal verification of the F-16 computer software and it still had significant bugs in the end where the specification itself was incomplete or in error. And that was a multi-year, team-scale effort. No one is doing that for smart contracts.
TLS 1.3 has been formally proven (not an implementation, but the standard itself). To the extent the mathematicians correctly explained what the TLS 1.3 RFC says, and correctly told the machine what TLS 1.3 is supposed to do, the machine proof says this protocol does what we intended.
That work assumes a bunch of components are black boxes, they must work. If we ever lose confidence that they work, we've got to throw those out. So for example SHA-256, AES GCM, X25519, the proof doesn't say "We prove these work" it says "Assuming you're right that these do what they're designed to do the rest of your proof holds"
Anyway, one of the assumptions in that proof is a surprise to a human implementing TLS 1.3, it isn't explicitly mentioned in the TLS 1.3 document as written. And so the result is, if you didn't obey that assumption, the proof doesn't hold and sure enough you're vulnerable to an attack.
The assumption is for Pre-shared Keys (e.g. IoT devices A and B don't want to bother with certificates, so they just use pre-agreed random keys) each device pairing has its own PSK.
A person looking at the design figures hey, got two devices Alice and Bob, I can just have a single key K known to both devices, and everything is secure. But that's wrong - and the TLS 1.3 proof doesn't say this will work. Here's what bad guys can do, it's called the Selfie Attack:
Alice sends a message to Bob, maybe "Did you feed the cat?" and it's encrypted with key K. Normally Bob receives the message, maybe answers "Yes I fed the cat" also encrypted with key K and all is well.
But now Mallory is on a network able to intercept and re-route messages. Alice sends to Bob, "Did you feed the cat?" encrypted with key K. Mallory can't read or tamper with this message, it's encrypted with key K and TLS 1.3 works as designed, but Mallory just re-directs the message back to Alice, "Did you feed the cat?". The message is encrypted with key K, Alice assumes Bob sent it, and replies "No, I didn't feed the cat" also encrypted with key K, which Mallory re-directs again back to Alice, who now mistakenly believes that Bob has told her he hasn't fed the cat.
There are obviously a bunch of things you could do to fix this. First of all you could just have more PSKs. If Alice's message to Bob is always encrypted using the Alice->Bob shared key, when Alice actually receives it instead she knows something is wrong immediately. Or you could just prefix each message with To/From information, like an old-fashioned email and that works too so long as you check it.
But the important observation is that this is an assumption in a proof that nobody really surfaced until it was too late. If researchers had told the proof system "No, the PSKs can be the same" the proof fails. Or if they'd carefully explained to the TLS Working Group, "We had to spell out that the PSKs must be different" then today RFC 8446 would likely explain that you need to do that or you've got a security problem. But neither happened and this attack slipped between the cracks.
1. a non-verified approach can have many problems in the (informal) specification + implementation errors
2. the verified approach is likely to have less specification errors (because the specification had to be formally written out and matched against an implementation) and implementation errors with respect to the specification will be almost impossible (minus faults in the compiler, OS and hardware).
There's a huge jump in security guarantees between 1 and 2.
I'm saying you should define a ceiling for your smart contract so in case of a bug, no transactions over that ceiling go forward.
So if you have a stupid bug that causes you to transfer 1BTC instead of 0.001BTC you don't lose all your money.
The key is that the contracts need to be minimal and analyzable, so its ~100 lines of code you can manually analyze. Documented separately all the edge cases, or ideally removed through good design so they simply don't exist. A bunch of problems I've seen in the real world of crypto are annoying edge cases that you can fix with an if statement, or ideally change the design to remove them completely. It's actually a surprisingly hard space because you're trying to make terse, complete and secure code.
In normal web/systems programming you have layers of security; internal services, external services, firewalls, access controls, vpns, security by obscurity, etc etc etc. In crypto you have none of that. Everything is 100% public, the code probably should be published, or else it is trivially decompiled. If there is a problem someone will find it if there is value in finding it.
> In normal web/systems programming you have layers of security; In crypto you have none of that.
Yes, that's what I mean. Why not?
> The key is that the contracts need to be minimal and analyzable
Agree, but even short contracts might have bugs. Betting on "self-paying bug bounts" is not a good bet.
What I'm proposing is that every smart contract double-checks its expected results
I have a lot more trust in that kind of product than in a product where contracts are subject to interpretations by humans which may or may not be reliable. It's one of the reasons why people incorporate their companies in Delaware, there are well known case law, so you know in advance what to expect from the justice system. Predictability is an important part of a contract, I trust a well inspected and battle tested smart contract much more than a human enforced contract. That said, not everything is suited to smart contracts, but many financial applications are.
Would you rather win $100 and have to make a phone call to claim it, or find a $100 bill on the street?
Not quite the same. Those codebases are much larger, often include legacy spaghetti code, or are closed source. This makes it more difficult to find exploits, not to mention there's not as clear of path of financial incentive.
It's a fair point that any easy-to-find bugs in large, time-tested contracts will have been found. Any medium- or hard-to-find bugs also will probably have been found. But there might still be a very-hard-to-find bug lurking; and given the value of finding such a bug, people might look hard enough to find it.
In other words, the same scale that ensures there is no low-hanging fruit, also provides the incentive to pick high-hanging fruit.
> I have a lot more trust in that kind of product than in a product where contracts are subject to interpretations by humans which may or may not be reliable.
This is a valid concern, but it's also extremely well-understood at this point; we have centuries of global-scale experience with traditional financial and legal systems. They're certainly not flawless, but it's rare for gigantic new flaws to emerge. An important point is the existence of mechanisms for rolling back bad transactions and challenging / appealing flawed decisions.
There are countless instances of rouge traders, high level financial crime and corruption.
Wirecard is one recent example costing billions. The Libor scandal another that comes to mind.
They faked the numbers, but they didn't manage people's money.
Eg. Their clients switched payment processor.
When a btc exchange frauds or a coin hacked or a smart contract is bugged, they get away with all your money. Which is the actual fraud.
In some cases they post a postmortem on medium and call it a day.
I don't think wirecard's fraud is comparable with all the crap in crypto town.
The core issue is the inherent asymmetry where 1 person finding 1 bug can destabilize giant systems. Even if these systems where hundreds of years old that doesn’t actually mean much.
https://github.com/openethereum/parity-ethereum/issues/6995#...
https://www.cnbc.com/2017/11/08/accidental-bug-may-have-froz...
*very large being required for significant money to be at stake, making say 10k illegally from a short is hardly going to inspire a lot of effort.
It's an incredibly simple algorithm and still got missed. Smart contracts have no chance.
With smart contracts the liability upside is orders of magnitude higher.
From https://en.wikipedia.org/wiki/Confusion_of_the_inverse:
> Confusion of the inverse, also called the conditional probability fallacy or the inverse fallacy, is a logical fallacy whereupon a conditional probability is equated with its inverse; that is, given two events A and B, the probability of A happening given that B has happened is assumed to be about the same as the probability of B given A, when there is actually no evidence for this assumption.[1][2] More formally, P(A|B) is assumed to be approximately equal to P(B|A).
I think this is what OP meant. If something has been around for a long time it does probably mean it's less likely there is a really obvious security flaw, but it doesn't necessarily mean it is 'rock-solid' as plenty of things that have been seen to be 'rock-solid' in the past have turned out to be insecure.
𝐏(𝐀) = 𝐏(contract has been hacked)
𝐏(¬𝐀) = 𝐏(contract has not been hacked)
𝐏(𝐁) = 𝐏(contract is hack resistant)
𝐏(𝐁|¬𝐀) =
𝐏(contract is hack-resistant given that it has not been hacked)
𝐏(¬𝐀|𝐁) =
𝐏(contract has not been hacked given that it is hack-resistant)
> The probability that a contract is hack-resistant, given that it has not been hacked, is approximately equal to the probability that it has not been hacked, given that it's hack resistant.
More succinctly:
𝐏(𝐁|¬𝐀) ≅ 𝐏(¬𝐀|𝐁)
¬(¬𝐀 → 𝐁)
𝐏(𝐁|¬𝐀) ≅ 𝐏(¬𝐀|𝐁) => the fallacy of the inverse
and
¬(¬𝐀 → 𝐁) => statement in comment
Note that the first statement is a comparison of probabilities, and the second is not. They're not the same. There might be another fallacy at play here, but it's not the fallacy of the inverse.
> If P, then Q.
> Therefore, if not P, then not Q.
In this case, we could plug in the below values:
P = Contract Hacked Q = Insecure
I.e. if the contract has been hacked the code was insecure. Therefore if the contract has not been hacked, it is not insecure.
Certain systems may have proven themselves somewhat over time but for this I say there is always the possibility for some extremely sophisticated attack and for any other new system they by definition wont have even this proven track record.
They all are until they aren't.
There is a large amount of money at stake with these exploits and it doesn't make economic sense to let one sit around.
I'm doing ICO next week, if anyone wants in.
The collective is incentivized to continue being fair because if they weren't, nobody would use their coin, and the rewards issued to fair lawyers would be worthless.
Some kinds of groupthink are bad (like making an anti-vaccine subreddit that only ever shows articles about vaccine-related industrial accidents, instead of a vaccine subreddit that shows people a truly representative sampling of vaccine knowledge), but other kinds are arguably good (not seeing 4chan nasty stuff on /r/reallycutekittensandpuppies.) Only some group content coordination is filter bubbling, while other times it's filtering.
In this design, determining the threshold for similarity may require the participation of a third-party "oracle" or "judge" component.
This is incentivizing what they think will be the most popular verdict vs what they think is the proper verdict. That's a very big difference and failures will be inevitable.
Everything involving code has bugs. Bugs aren’t a reason not to use code. Bitcoin isn’t a problem for the very small fraction of the population that use it. Bitcoin users are super rich tech workers and finance guys, by and large.
The people hurt most by Bitcoin are all the people who don’t use it. It benefits the ultra-rich at great expense to the other 99% of humanity.
Unless you don't believe the narrative that Bitcoin stores/grows wealth very well, in that case...poor people can simply not use it.
Perhaps you mean to say that the distribution of coins is uneven. That's true, but not a problem Bitcoin aims to solve or can solve. Bitcoin is fair, the same rules apply to everyone. If a billionaire has a 1,000 Bitcoin and I have 0.1 Bitcoin, we both win or lose based on price action equally, relatively speaking. That's as fair as it gets. With Bitcoin, having lots of coins doesn't give you any new free coins, unlike fiat money.
The environmental destruction is overstated and rapidly changing as we speak. Soon the vast majority of mining happens based on renewables with a specific focus on stranded energy. And this isn't a vague promise, some 60/70% of the hashrate from China, which include most coal-based mining, is being wiped out in just a few weeks.
Fiat money doesn't give your free money either. You have to invest in something - and there's plenty of fee-limited options in the cryptocurrency world as well.
> And this isn't a vague promise, some 60/70% of the hashrate from China, which include most coal-based mining, is being wiped out in just a few weeks.
Because the price is so low, not because they want to help the environment. At the next peak everyone will be happy to burn whatever fuel is cheaper than the payout again.
Nobody wants to help the environment. The typical US lifestyle would require 8 planets if it was rolled out across the world's population. Just leaving your phone plugged in uses more energy than all of crypto mining combined.
So don't preach about caring, nobody cares. They say they do, but don't. So yes, miners seek out cheap renewables, which is motivated by profit, not helping the environment. As said, none of us are better. We don't care. But if a profit-based incentive leads to renewable energy usage and helping the environment as a side-effect, I'm all for it.
But the same applies to BTC with BlockFi / BIA.
Not true for Bitcoin. Neither owning your coins in a wallet nor leaving them on an exchange grows your amount of Bitcoin.
Can you give away your Bitcoin to some rogue, fully unregulated party claiming you get back more Bitcoin? Yes, in the same way I can give my fiat to some shady character in the streets. I may get back more fiat. Or I may be permanently parted from my coins.
These things are not the same. Bitcoin does not have interest built in. Not at bank level nor at central bank level. This is radically different from fiat.
Into an interest paying account - yes. A savings account like that may be the "don't even mention it" default for you and me. But not for:
- unbanked people in the US (~6%)
- and in the world (much larger https://www.motherjones.com/kevin-drum/2019/06/raw-data-unba...)
- people with non-interest-paying accounts for religious reasons
- people in countries where interest is ~0% or negative (https://dqydj.com/negative-savings-accounts/)
Ever heard of the African Bitcoin community, a transnational initiative running for years now that resulted in Africa growing fastest in addresses of all continents?
Or what about El Salvador, 70% unbanked, where every single citizen will get a first small BTC deposit from the government, thereby becoming banked by the millions?
And what about Libya? You know, that country with a crashing currency that next blocked access to bank accounts for months, it all going up in smoke? Looked into the BTC numbers there?
So tell me, were you completely unaware of this at all, or do you find these people not important enough to count as more than zero?
The impacts of climate change, which Bitcoin unquestionably contributes to, skew significantly towards poorer countries.
And the consumer protections built into the regulations around fiat currencies are there to protect people who can't afford teams of accountants and lawyers.
Ethereum is working on moving to proof-of-stake within the next year, which completely removes its need for energy-intensive proof-of-work mining.
> “One of the biggest problems I’ve found with our project is not the technical problems, it’s problems related with people”. - Buterin
https://tokenist.com/buterin-explains-why-ethereum-2-0-upgra...
Given that the reasons are political rather than engineering in nature, there's no way to put a timeline on them.
Edit: might have the details confused about above point, but the general thrust of things is pretty clear. https://foreignpolicy.com/2019/03/19/neo-nazis-banked-on-bit...
They didn't all agree, though. Now there's Ethereum (the people who agreed with the fork) and Ethereum Classic (the people who didn't agree).
Your first comment [1]
> As long as everyone agrees i see absolutely no problem
and now
> Some agreed, others didn't...Consensus doesn't require everyone to agree, just the majority
So you literally just said there is a problem.
The DAO was a very extraordinary event that occurred under very unique and unrepeatable circumstances.
1. Ethereum had just launched. There was a sense of everything being in beta.
2. The Ethereum stakeholder set was very small, so obtaining consensus for such a controversial hard fork was much easier to accomplish than it would be today.
3. The economy on Ethereum was very small, so
a) a hard fork was far less disruptive than it would be today.
b) an undermining of Ethereum's commitment to neutrality/immutability jeapardized far fewer decentralized application projects than it would today.
4. Smart contracts were completely new, so there was a sense that people could be forgiven for their mistakes.
5. The Ethereum Foundation had promoted the idea of a DAO on their website, and several Ethereum founders had promoted the specific DAO that ended up being hacked. These facts made the DAO appear to be more than a completely third party app.
Ethereum is very different today than it was in 2016, and a DAO-scale mishap would never lead to a hard fork again.
I also don't think it matters and there is no consensus to do the same thing any longer.
The explanation for why they did it was because the transaction would have a very large percentage of Ether in the hands of one actor who would eventually be able to alter control of the future Proof of Stake network. If it was any other asset they wouldn't have bothered, and now much larger $ values are captured from people without any notice or fanfare. They didn't know it would be 7-9 years before Sharded Proof of Stake or the Beacon Chain would exist, and its likely that the means did justify the ends at that point in time as many of their supporters and institutional supporters had their funds in that contract.
Without that I think the best you could do is model your program in some other formal verification system and then convince yourself that your model matches the actual contract.
With such a language you can write proofs about the behavior of the runtime using some proof checker and then programs in it should be simple enough to reason about in a rigorous way.
What I have not seen and what I am curious about is a smart contract language more in the spirit of Idris. That is to say a more complex language design with full dependent types, which would be a lot more difficult to formalize, but would allow you to do really nice things like treat proofs as first class citizens in your actual smart contracts.
The idea about having proofs as values in smart contracts is interesting though. I could see a few neat applications of that.
It's massively more expensive, so you'll see it used in aerospace, railway signalling, some vehicles (trains, components of some cars), power generation and distribution, industrial processes.
Sometimes also in consumer products that have long warranties and are extremely expensive to recall/repair, like washing machines.
Just yesterday was a post on a formally-verified C compiler, used by Airbus (and others) [2]
This may interest you: https://en.wikipedia.org/wiki/Rice's_theorem
Sure. And if you look at sufficiently small-scale pieces of software, there is probably a lot. As scope of a software system increases, the probability of bugs rapidly approaches unity, though.
Ensuring your requirements are correct is possible, but often hard. Ensuring your software meets the requirements is possible, but often hard, especially if you need to consider hardware failure or defects.
Only in academia
The mechanics of stable coins is really trivial and thusly should be trivial to implement and validate. Unfortunately it is not, and it is sad that the hype and investment rush inside the broader crypto field does not foster languages and platforms that actually are suitable for the few realworld use cases that exists inside crypto.
But in practice they can work for a while.
They work by taking a collateral and splitting in two. The first part has some fixed value in an external currency. The other part is the rest. And that works as long as the rest has some value.
However here we are talking about programming errors in the implementation. And Solidity/Ethereum is really at fault.
How do you implement a contract in Ethereum where a certain thing happens the price of Ethereum drops below XXXX dollars? You can (as this is what MakerDAO and others are doing) only it is silly complex to do.
It really should not be.
Ethereum is pretty unstoppable, but unless you use a contract proxy, your contracts are immutable and bugs that can be exploited will be exploited.
I think he was going to college for computer science and then switched to law. Last I heard from him, he was running for a judgeship.
Tezos is often referred to as the first “self-amending” blockchain, which routinely adapts and adopts new features natively and automatically via its unique on-chain governance mechanism. This protocol functionality allows the system to coordinate the selection of new updates though popular voting, integrate the new updates that are selected, and compensate the developers who proposed them. [1]
[1] https://www.gemini.com/cryptopedia/what-is-tezos-xtz-governa...
Although the article is talking about the SafeDollar contract, there were some general points about crypto / blockchain in this thread that I was responding to. Tezos is one example that has on-chain governance, which is why I mentioned it.
If you want to provide more info about how the on-chain governance is really just done through soft forks, and why you think that's not innovative, I'd be curious to hear. I'm not huge on Tezos but I think they do some interesting things.
2. We have a general AI exception handler called a pilot.
3. Many of those systems have hardware redundancies, so even if there is a bug, hardware can stop it. A fuse might blow instead.
And you get a refund for your plane ticket if you reach your destination, but if you don't, whoever figured out the trick to crash the internet-connected plane gets to keep all the ticket money. And that could be the same person who wrote the plane's software.
The incentives to break those other pieces of software are different.
Very few people are incentivized to hack planes to crash and kill people. Even fewer are incentivized to hack the space shuttle. Not to mention those pieces are rarely exposed on the public internet, or have connectivity at all.
But massive amounts of nigh-untraceable free money? Ton's of people are incentivized to go for that.
It's hardware with no joysticks for humans to adjust. It just happens to be hardware that's implemented in code.
The trade offs in functional languages seem to well suited for the world of smart contracts, that I almost think of smart contracts as the retro-active problem that functional programming solves. Granted, I appreciate functional programming and good code enough where I wish all code met the standards required for FP, but the real world is much messier; when large amounts of money are so directly on the line though I think its obvious the compromise is worth it.
Smart contracts are like launching a rocket - you don't optimize for development time. FP forces a bit more safety.
What you do get in contract disputes where specific wording matters is in edge cases where you might reasonably assert that both parties wanted (and agreed) A or not-A for some specific situation as part of the negotiation, disputing where exactly some boundary lies - but not for the core parts or complete reversal. On the other hand, automatically enforced "smart contracts" don't make such a distinction and any typo can reverse the core meaning of the contract as well.
And all of that is a kind of technology that many "technology" people are far too eager to throw away for spurious reasons (often because they just plain don't understand it).
It's like if someone was working on autopilot program and rewrote it in a "modern" language, and "simplified" it in the process by dropping a bunch of "unnecessary" use cases...then it turns out that at least some of those cases were there for good reason and a bunch of planes crash. A lot of cryptocurrency and blockchain stuff is half-baked because it seems focus on faddish technology for its own sake rather than trying to actually build someone that works.
Contracts have always had a healthy dose of manual debugging that have allowed them to function.
[1] The idea of "a reasonable person" is used heavily in the US legal system and has problems but it also has upsides.
Not a lawyer here but I’m guessing.
Not all legal loopholes automatically deprive you of all your savings. Intentional loop holes only go so far before consumer protection or other entities overwrite it. And if both parties are in agreement and in good standing you can figure out a way to find a reasonable compromise.
*Not a lawyer either, but I've read some introductory contract law stuff. All I know is this: you don't want to rely on the courts to save you, since they generally err on the side of the literal contract, but I don't spend much time worrying about accidentally agreeing to a contract that will sell myself into slavery.
With a smart contract, there can be no negotiation and attempt at reconciliation. The price here will never recover from $0, so at a single point in time $248,000 was transferred from bag holders to beneficiaries.
I agree, but think it's fixable. I believe we have missed a natural platform in between binary notation and computer languages.
I believe there is a 2-D dimensional binary. Simply using a grid (with an array of cells forming a line, and lines stacked on top of each other—a spreadsheet basically), we can drop *all* syntax characters. The only thing you have is your cells and your semantic words.
Not only does this make tooling and languages much simpler (which will have big network effects), but you gain new fundamental complexity metrics which may turn out to be incredibly important in designing simple, bug free systems.
I personally really like crypto but it's not one of my main interests. I have been working with some folks in the space on using these ideas to build a new type of blockchain from the ground up. I bet that the biggest blockchain in the future will be a higher dimensional one, based on Tree Notation or derivatives of the core ideas.
I fail to see how this helps.
The reason why bugs crop up all the time in software isn't because syntax is confusing. It's also not because semantics is confusing--plenty of bugs have perfectly clear, well-understood bugs. The problem is that we as programmers don't think about how our software could fail. We don't ask ourselves "could this multiplication overflow?" frequently enough. We don't look at code and ask "who made sure this pointer points to valid data?" We believe that there's no way the price of an affiliated token could ever reach exactly $0, so we assert that it can't happen.
The way you avoid these bugs is to just simply make it impossible for the system to get into certain states. It's already the case with statically-typed languages that it's impossible to pass a string to a function that expected an int. If you design your API right, you can make it impossible to get an index into an array that is out-of-range (although this is way too rarely done). But, even then, you will still find people who will confidently use the escape hatch to say "this string is clearly UTF-8, I know it is from outside experience, so don't bother checking."
> v
v ,,,,,"OH NO! "@
I simply don't think it's possible for human beings to write good enough software for smart contracts.