Live data from Hacker News

Missing line in a smart contract leads to $10M hack

rekt.news

151–160 of 333 posts

Re: Missing line in a smart contract leads to $10M hack

#151
post #124

Earlier quoted context omitted.

Theorem provers require code for defining what you want to prove and the method through which you reach said proof. Proofs and theorems can have bugs.

But aren't proofs exact in what they state? So it wouldn't be the proof that would be faulty. It'd be the interpretation of what somebody thinks the proof means to them, and that'd be something you could entirely objectively reason/work on.

But the human world is not exact and full of context. Even mathematical.proofs exist within a context of an axiomatic system, known proofs, and various domain assumptions.

I remember that in my computability theory class, defining the right proof was by far the most difficult task. And this was in very small, closed systems.

Re: Missing line in a smart contract leads to $10M hack

#153

Earlier quoted context omitted.

>Because the author(s) of this article forgot what makes hypertext so powerful. (In fact, I think a lot of people have forgotten that. Don't be afraid to link things, people. Linking to something literally saves you the trouble of explaining it yourself. LINK MORE, PLEASE. I will click.) This is a fine sentiment, but [you] [don't] [link] [every] [word] [in] [your] [sentence] to a dictionary website either, because yo…

This is actually a bit amusing, because one of my favorite reading features on iPad is being able to click and hold on an arbitrary word to look it up. Sure, the UI/UX of a traditional link isn't desirable, but I do want every word to be linkable to the dictionary.

Firefox has an option for this in the right-click menu after selecting text (e.g. by double-clicking).

Re: Missing line in a smart contract leads to $10M hack

#155

Earlier quoted context omitted.

Maybe it is, I don't know. But I do know that I'm not ever even going to dip a toe into cryptocurrency because of the personalities of the people who are heavily pushing it. I am not talking about you. Everyone I know who is into this is very strongly into it, and they can never really explain why. Lots of non-specific sentiments emerge, and rather quickly, but no real this-changes-things-because-of-X details or expl…

Which personalities are you referring to? I'm curious about what you've picked up as well. Like people not being able to explain why they're into it. Could you elaborate on those things a little bit?

The super "gung-ho about cryptocurrency" guys. They act a lot like they're selling you a car that they don't have any details about. It's great, it's awesome, it's everything you ever wanted, etc. It will make you look good, it will make you happier, it will make you more confident, and so on, but if you ask about anything other than what is printed on the sticker, they can't answer the question with any detail, and they deflect.

That's my (of course limited) experience with cryptocurrency advocates.

Re: Missing line in a smart contract leads to $10M hack

#156

Earlier quoted context omitted.

Yeah, that's my question with all this. I mean, ransomware is obviously illegal. Finding vulnerabilities in smart contracts - well, "the code is the contract", so the hacker is just executing the code as it was published. I mean, the whole reason Ethereum Classic exists is because a subset of Ether folks felt that restoring the funds in the original DAO hack was contrary to the whole "the code is the contract" ethos.

If Code is law then hard fork is also law. Otherwise those Ethereum classic people are saying that code is law but only the DSL of Solidity. Outside updatable Ethereum engine code is not law.

> If Code is law then hard fork is also law

Not at all. All crypto currency only has value because other people collectively choose to "believe" a certain chain. Usually there is global consensus of which chain is the "true" chain, but there have been many times in the past that one group has decided to follow a different fork for whatever reason. I mean, Bitcoin has Bitcoin, Bitcoin Cash and Bitcoin Gold. The value that gets allocated to a particular fork just depends on the number of other people that choose to follow that chain.

Re: Missing line in a smart contract leads to $10M hack

#157
post #118
post #112

Earlier quoted context omitted.

> because nobody likes to lose their live savings because they missed a semicolon. Yeah, but shouldn't it be possible that these things will be avoided by confirming the validity of the code with theorem provers such as Coq, Lean, or something similar, at some point in the not too distant future? That's what I've been wondering, without currently having any stakes in the game (and probably not until there's compellin…

That would cost an arm-and-leg, it would need to be done by someone who actually understands both the theory of proving algorithm corectness and the algo in question and systems like CoQ are from being able to prove large, complex systems. All the while traditional "non-distributed" finance simply uses sound engineering practices, such as code reviews, audits and sign-offs at much smaller cost and without requiring s…

>That would cost an arm-and-leg,

Without being able to provide any evidence, I'm quite sure (that is, I hypothesize) that if a theorem is clearly stated, such as in the case of formal proof assistants, we'll soon reach a point where we'll have a distributed network in which people are able to 1) provide economic incentive for somebody to provide a given proof, 2) somebody else to potentially offer a better proof which will computationally be accepted (verified by some algorithm that prefers one proof over another by some sort of metric), and therefore 3) have a system in which the validity of a computer algorithm, which has been stated as a conjecture, can be mathematically created and verified in a decentralized fashion.

>it would need to be done by someone who actually understands both the theory of proving algorithm corectness and the algo in question

If the theorem is stated clearly, no further understanding is needed. But of course they'd need the understanding of providing the right axioms and definitions, which are as limited as possible, to state their conjecture. That, I think, will be the point at which the purpose of the mathematician will shift from providing proofs, towards discovering interesting and coherent conjectures, as the proving of those will turn into a kind of rat-race, and ultimately merely a computational challenge.

Anyways, I'm just rambling about some things that have been on my mind recently. Don't take me too seriously.

Re: Missing line in a smart contract leads to $10M hack

#158
post #26

Earlier quoted context omitted.

You could argue all hacking is just doing something that is (accidentally) allowed by the target system.

Not really, because the entire premise of smart contracts is that the code IS the only representation of the contract. In normal software systems there’s an intent and then an implementation. There’s no explicit guarantee they are identical, which is exactly why there are subsystems to allow e.g. refunds or transaction invalidations.

That premise is clear, proponents of smart contracts would like it to become true, but as of now that premise is simply not true anywhere in the world.

There may be obvious practical difficulties in identifying the counterparty and enforcing a judgement in them, but if that becomes possible (and if $10m is at stake, perhaps it might become possible, bounties, etc) then the argument that "code is the only representation, and this is what the code said, so this was lawful" is not valid, as it contradicts both contract law and fraud statutes.

Re: Missing line in a smart contract leads to $10M hack

#159
post #104

After reading a bit, not knowing WTH is being talked about, I did some searching. Because the author(s) of this article forgot what makes hypertext so powerful. (In fact, I think a lot of people have forgotten that. Don't be afraid to link things, people. Linking to something literally saves you the trouble of explaining it yourself. LINK MORE, PLEASE. I will click.) So this is apparently about some stock market for…

I know this won't change your mind, but the reason you are seeing new terms is, because you're seeing the birth of new protocols. Pictures yourself in the early days of the internet and you want to learn about http and/or javascript (for example) - you would be overwhelmed with new terminology to concepts that didn't exist before like gui based web browsing. Crypto/Defi are this in many ways. Does that make it not a…

The Internet was something new that provided new capabilities and new abilities to humanity with extremely high reliability, and at a scale that didn't exist prior to that.

Cryptocurrency doesn't provide any new capabilities at all. Money and trading existed before. Price fluctuations existed before. Markets existed before. Buying and selling existed before. But now, because it's so new, and because it's not technically money, but a virtual good, this is all unregulated and fertile ground for people who want to take advantage of others.

This is why it seems to me so much like a sales pitch to me when people talk about it. It seems very much like they need you to commit money in order to get anything out of the arrangement themselves. This is "Jebediah's Miracle Snake Oil" with a new name.

Re: Missing line in a smart contract leads to $10M hack

#160
post #18

Earlier quoted context omitted.

Moreover the "hacker" is simply doing something that is allowed by the contract so it's hard to argue that these hacks are even unlawful.

Yeah, that's my question with all this. I mean, ransomware is obviously illegal. Finding vulnerabilities in smart contracts - well, "the code is the contract", so the hacker is just executing the code as it was published. I mean, the whole reason Ethereum Classic exists is because a subset of Ether folks felt that restoring the funds in the original DAO hack was contrary to the whole "the code is the contract" ethos.

Ignoring contract law (which would not blindly accept "the code is the contract", and people's ethos does not allow them to arbitrarily decide how contracts shall work in the country where they live), the fact that some action was explicitly written in a contract that was properly signed by everyone does not necessarily mean that the action was lawful.

For example, if you intentionally misrepresent what the contract means to deceive someone into signing a contract, then is fraud, and it also invalidates the contract. If the fraudster already got the money according to that (invalid) contract, no matter if it's cash or crypto, they possess it, but it's not lawfully theirs.

Post reply on HN