> 2. Ethereum software has security hole, gets hacked

The last time this was discussed on Hacker News, I found this comment particularly instructive: https://news.ycombinator.com/item?id=14810008

It points out a great many fundamental issues with the Solidity contract language. Basically, the language design sounds extremely amateurish and it appears to have ignored everything we've learned about security in the last 30 years. Samples:

- "Operators have different semantics depending on whether the operands are literals or not. For example, 1/2 is 0.5, but x/y for x==1 and y==2 is 0."

- "All state is mutable by default (this includes struct fields, array elements, and locals). Functions can mutate state by default"

- "Order of evaluation is not defined for expressions. This in a language that has value-returning mutating operators like ++!"

I wouldn't trust a Solidity smart contract with $100.

Does Solidity really matter, though? "How's the VM" is the real question. I haven't spent more then 10 minutes looking into it, but it seemed reasonable to me. No heap and 256(?)-bit addressing seem like good ideas to keep execution complexity down.

The VM is also fucked (or, at least it was in the recent past) because it turns out that their semantics are a mess. For example, exception handling is either implicit or explicit depending on how a method is invoked!

https://eprint.iacr.org/2016/633

It does matter if the use of Solidity is being actively promoted. Sure, maybe you're smart and you'll pick safer options, but if a huge percentage of contracts are written in Solidity, it could still mean there are massive security holes everywhere.

This! ^^

Solidity code is horrible, especially after looking at concise, maintainable, provably correct code.

Ugh that's... disconcerting to say the least.

I hate immutable variables because I'm lazy but I would definitely use them as a feature in a system like this. Maybe I should reconsider using erlang or my position on immutble variables... Nope that's enough self discovery for today... Carry on.

Edit: And again erlang people can't take a joke. I'm literally making fun of myself for having an invalid bias and erlang folks take it as an attachment on the language.

It's also a commentary on how long it takes for devs to mind shift and incorporate new ideas.

There are two distinct features: immutability and single-assignment. Erlang is famous for single-assignment, and also happens to have largely immutable values, but they are not the same thing.

Immutability prevents things like in-place appending to an array, or in-place modification of a string.

Single-assigment means that the value bound to "someVariable" cannot be changed. E.g. `someVariable = new String("hello"); someVariable = new String("goodbye");` is illegal. But it still may be possible to mutate the value `someVariable.substitute("hello", "goodbye")` if the language allows mutation.

You wouldn't trust a bank with an SQL-injection vulnerability or a hospital running on an old version of Windows either but that doesn't mean all banks and hospitals are not trustworthy

A new monetary system created 3 years ago and is highly demanded might have some growing pains

You hold $0 of Ether but suggest on how to spend it, you wouldn't send ether to a contract that was coded poorly or vulnerable so the language is not as important as you make it seem.

Ethereum has a great bug bounty program so contracts that are vulnerable get exposed fast. Each new smart contract should learn lessons for previous contracts and the software will improve over time, imagine that...

> You wouldn't trust a bank with an SQL-injection vulnerability or a hospital running on an old version of Windows either but that doesn't mean all banks and hospitals are not trustworthy

I would and do, because that's the reality of things. You're discounting the fact that if my bank has a SQL-injection exploit used against it and my account is drained, the federal government will reimburse me up to $250,000.

That type of peace of mind does not come with Ethereum; in fact it's billed as a feature.

Don't worry, they'll just do a fork and magic your money back. So much for avoiding the problems of central banking.

it is because the federal government mints and controls the currency of dollars, with Ethereum you can create an arbitrary token and mint this token to any amount, essentially be your own federal reserve, Ethereum is an interesting software platform. Coinbase is fully insured all their digital currency is backed if a breach was to happen the customers will be refunded. So I suggest you keep your $250000 in there.

How often do you hear of someone loosing thousands of dollars perminantly because of a banking error? Almost never, because if a bank did not reimburse people who lost money, their reputation would be destroyed. How often do you hear of people losing thousands of dollars because of a cryptocurrency? All the time, because no one is responsible for the lost money, so no one will replace it or work extra hard to ensure it is safe. Security doesn't matter when you have a central authority dedicated to ensuring you don't loose your money, and which had been successfully doing so for decades.

What does this first sentence even mean?

I translated it as "if there is a market opportunity for there being a private, ethereum-backed federal reserve, one will emerge."

the federal government can reimburse the person I was replying to because they control and mint dollars. With Ethereum you can control and mint your own currency, I didn't want to use the word currency earlier, it is more of a digital asset or app credits.

The belief that Turing machines aren't amenable to formal verification is a hobgoblin that shows up in every thread like this, but it's not real.

Of course there are limited formalisms that make certain types of verification easier, but proving programs has been possible since, like, the 1960s.

A multisig, for example, has a finite number of states when considered under symbolic execution. A model checker can rip through it and prove whatever properties you want.

Is the Ethereum world right now full of buggy contracts that haven't been proven correct? Yes, absolutely. It's a disaster. But it's a disaster that points the way fairly straightforwardly.

Should Ethereum not have been launched until it had solid methods for auditing and proving? Maybe, but that's not how the world works, typically. Worse is better and all that.

Sure, you CAN verify Turing machines, but verifying languages that AREN'T Turing complete is sufficiently simpler. So why not make your verification work easier by using a total language? The only real argument against that would be "we can't do what we want in a total language".

I don't buy the argument that what people want to do with smart contracts requires Turing-completeness. In fact, as time goes on I become more and more convinced that Turing completeness is highly overrated. Almost all code wants to do finite and/or structurally inductive operations. The only case that doesn't fall in that are things like request loops where you want to "infinitely" wait, process request, loop back to waiting. But even those things can be done in total languages via co-induction, so exactly why do we want to make our analysis/verification work more difficult by using a non-total language for things like Ethereum?

The real answer is probably that total languages are obscure and the Ethereum inventors didn't know about them so they chose a simple and ordinary stack machine.

But those total systems are, of course, subsets of Ethereum, which means that if you write your program in an obviously finite way, you can use the same inductive proofs you would use for a total language.

Turing completeness makes it hard to prove properties automatically about arbitrary programs, but you can still prove properties about specific programs.

I'm pretty sure that MOST research on program verification has been done in the context of Turing complete systems, from the work of Floyd and Hoare, to the symbolic execution of Deutsch and King, to temporal logic, TLA+, etc.

> The real answer is probably that total languages are obscure and the Ethereum inventors didn't know about them so they chose a simple and ordinary stack machine.

I'm not an expert on Ethereum, but even if they did pick a total language, how would you deal with bounding the CPU cost of complex contracts? Even if you could formally verify a loop would eventually terminate, wouldn't long running loops or those with expensive computations have bad impacts on the network? Their "gas" system is their way of dealing with that and perhaps you would still need something similar even with a total language.

I can't think of program verification research where both termination and CPU cost is verified. I can think of some papers that deal with identifying Big Oh growth rates though.

Either way, smart contracts sound like one of the top tier areas where you want strong static typing that has a route to be formally verified.

The gas limit is one reason I think it's weird that people insist on calling the EVM "Turing complete", since one of the most prominent features of the system is that every program is guaranteed to terminate in a finite and low number of steps (via the gas mechanism). Turing complete programs are supposed to be problematic because of the halting problem, but in the EVM, the halting problem is trivial: every program halts, period.

> The gas limit is one reason I think it's weird that people insist on calling the EVM "Turing complete", since one of the most prominent features of the system is that every program is guaranteed to terminate in a finite and low number of steps (via the gas mechanism). Turing complete programs are supposed to be problematic because of the halting problem, but in the EVM, the halting problem is trivial: every program halts, period.

Exactly, knowing that the contract code will eventually halt is nice to know but knowing that it will halt after a reasonable CPU cost seems much more important in this case (which is really interesting).

From what I've seen from example contracts, it doesn't seem like the chance of infinite loops is that high. Personally, I find that in mainstream languages, if you accidentally write an infinite loop you find out very quickly on the first few runs and code that could be hiding an infinite loop stands out. The vast majority of loops just iterate from the start of a collection to the end.

The contract coders I work with try as much as possible to avoid loops altogether, because even if they're correct, they'll still have a linear cost, and that's usually not what you want. Almost all contract operations should be O(1). Sometimes we've made fairly large system design changes to avoid a loop in a function.

Interesting. So what's your view about the most practical language for writing contracts in then?

For what I've read, having the sender setting gas limits seems really awkward especially when the limit is exceeded. Are there practical alternatives? Even with O(1) you'd need to limit the computation time.

I don't have a fully formed view yet, but I think Solidity is a pretty good prototyping language, disregarding all marketing hype that it's an "easy" language. While developing, you'd also be working on a specification of exactly how the contract shall behahve, and trying very hard to simplify ruthlessly.

The Parity multisig contract is very complex and I wouldn't and didn't trust any funds with it. I hope that the newly deployed fixed multisigs are bug-free but how would you know?

Right now I'm working on tools for static analysis of bytecode and using such tools to verify the correctness of contracts written by hand in assembly, which I think makes a great deal of sense for the simple contracts that we need as utilities (multisigs, tokens, etc).

> The Parity multisig contract is very complex and I wouldn't and didn't trust any funds with it. I hope that the newly deployed fixed multisigs are bug-free but how would you know?

Yeah...any ideas why they didn't go with a language that had an easier route for formal verification? It seems like an ideal application and the contract specifications seem like they would be fairly straightforward to prove (compared to what you'd see in most journal papers for instance). I'm guessing the designers just weren't aware of theorem provers but I'm puzzled why they didn't go with a language with strong static typing where private access and immutability are the defaults plus avoiding anything to do with the mechanism they have for picking default handling functions when a message isn't understood. Great experiment to watch though!

I'm not sure static typing is tied to formal verification. In fact if you think about it most proofs are basically typeless I a lot of cases.

Dependent or even refinement type systems are where a great deal of research into proof carrying code is done (for refinement types, since systems are restricted to decidability, the proofs are automatic but more limited).

What proof systems are you thinking about? Strong static types seem the most natural way to introduce formal verification into mainstream programming to me.

(Not the parent here.) ACL2 is a prominent example of a proof assistant without a strong static type system; its object language is a pure subset of Common Lisp. The lack of static types is one of the reasons I find proving in ACL2 to be painful, but others have done amazing stuff with it.

Well general mathmatecial proofs or TLA+... or would it be better to define "integer" as a strong type which I'm willing to concede.

I don't feel there's much difference between e.g. the Coq way where types are used to bake specifications + proofs into the program and the Isabelle way where you write a program with less complex types and prove properties about the program after the fact.

General mathematical proofs? If you mean paper proofs they wouldn't be considered formal as they don't go down to the axiom level.

I guess that makes sense to count axioms as strongly typed.

Type checking can be represented as abstract interpretation. It is the mostly widely used kind of formal verification that exists.

Corecursion and codata are cool, and I would trust Solidity vastly more if it were a "total" functional language with no mutable state and aggressive type checking. Or if it were something more like https://www.idris-lang.org/ , where I had abundant tools to rigorously prove that nobody could steal my money.

Basically, if I'm going to spend even 5 minutes playing with smart contracts, I want to feel like the language designers were incredibly paranoid and aware of just how good modern languages can be at provability and security.

If you're competent with proofs in Idris, you can write your EVM programs as an Idris DSL.

But, I mean, there's no proof that the Idris compiler does what it's supposed to do, so you'd still have a huge trusted base.

> If you're competent with proofs in Idris, you can write your EVM programs as an Idris DSL.

Yeah, all my formal proof experience is with Coq, which is just a bit too idiosyncratic and difficult for this sort of thing. But I seem to remember that—especially if you're willing to certify specific results, and not necessarily the program in general—you can make your trusted computing base very small indeed.

I mean, if the CompCert C compiler can be as thoroughly verified as it is (http://compcert.inria.fr/compcert-C.html), there's no reason why it shouldn't be possible to verify smart contracts.

Some pointers you might appreciate:

Jack Petterson and Robert Edström did a master's thesis about retargeting the Idris compiler to emit EVM code, with a custom effect type to express smart contract effects. They ended up modestly skeptical of functional programming as a paradigm for EVM, instead looking toward process calculi. https://publications.lib.chalmers.se/records/fulltext/234939...

Yoichi Hirai's summary of his research into Ethereum formal verification as a full-time formal methods researcher at the Foundation: https://github.com/pirapira/ethereum-formal-verification-ove...

See especially his formalization of the EVM as Hoare triples in Lem, which is usable from Isabelle: https://github.com/pirapira/eth-isabelle -- very cool stuff, although I have to say that the ostensible complexity and difficulty of his proof verifying an utterly simple wallet contract makes me a bit skeptical of this approach to smart contract correctness: https://github.com/pirapira/eth-isabelle/blob/master/example...

> I mean, if the CompCert C compiler can be as thoroughly verified as it is (http://compcert.inria.fr/compcert-C.html), there's no reason why it shouldn't be possible to verify smart contracts.

Hmm, so from the smart contract examples I've seen, I would have thought writing them in something like Coq would be quite feasible. The code examples I've seen tend to only have simple loops if any, basic conditions and the code is short (e.g. compared to something like web development or mobile apps). Writing anything inside a theorem prover is very challenging though but it seems a compelling application.

If you were implementing a smart contract in something like Coq, I'd be interested to read about what kind of specifications you would typically want to verify. I guess properties like "the owner of this wallet cannot be changed" and "the owner of this wallet can only accept money but not give it away" would be good ones.

Etherium should have launched with a language that wasn't a high-school-extra-cirricular-level in terms of construction and consideration.

Solidity doesn't have a problem with formal verification of programs. Check their bug tracker: you can't even trust the runtime to do what it claims to do. On several levels.

> It's a disaster. But it's a disaster that points the way fairly straightforwardly.

A disaster that could have been avoided if they had done a little more research on security and smart contract languages:

http://lambda-the-ultimate.org/node/5003

Solidity is still clearly focused on programming productivity instead of contract soundness. The built in dynamism is proof of this.

> Should Ethereum not have been launched until it had solid methods for auditing and proving? Maybe, but that's not how the world works, typically. Worse is better and all that.

As a platform for experimentation that's fine. As a platform for doing real things with meaningful amounts of money, it's madness.

Madness indeed. For better or for worse, silly experiments in this industry often turn out to win. According to the "Worse is Better" theory, that's partly because they ship much faster than the projects that want to get everything right, and they're also easier for most people to understand. You could put a team of Ph.D's on inventing a really amazing smart contract formalism based on higher-order zygomorphic type theory, but if only five people in the universe understood it, we wouldn't be talking about it.

This would be compelling were it to contain accurate information. However, likening the parity incident to a "hack of ethereum" is like saying the USD is flawed because wells fargo was broken into. The same thing is true for the DAO, although it is indeed more complex in that the _resolution_ of it was handled by Ethereum proper. I think that was questionable.

Literally no one within Ethereum calls it an experiment. You have to cherry-pick from population and then ascribe it to the whole for this to be even sensical.

Essentially every technology we can think of can be rooted back to the 90s, or really any period we want to look at since that is how knowledge works. If you've got a particular, say it...rather than just this poor, lazy attempt at a sort of character assassination by employee (fairly inaccurate) appeal to oldness.

It is thoroughly _without merit_ to suggest that the analogous components of ETH and BTC have BTC being more secure. In fact, the opposite is true by any reasonable measure. Further, there are indeed things that Ethereum tries to do that add complexity, but if they come with value we shouldn't then find ourselves saying things like you do that amount to a sort of "my abacus is more secure than quickbooks online" - different purposes, solving different problems and creating different sorts of value. Even beyond that BTC holds all records for security events and $ cost of them, coin-loss amounts of of them, and so on.

> the takeover-the-world echo-chambers of ethereum

You toss out this pejorative description, and then in the next paragraph:

> When talking about engineering on such a critical subject, people should be way more responsible.

This is absurd. How could it ever become critical without a lot of research and development first?

I've been holding a handful of Ethereum since there was a decent dip in the price. I haven't spent much time on it and I have no good leads for program ideas yet, but if the code is buggy and I get hacked and lose my investment, that's fine. A smart contract is a project, and it could fail like any other.

Don't put your retirement savings in a smart contract right now unless you're OK with losing it all. Maybe in the future Ethereum will move beyond this phase, and maybe not. All the drama is ridiculous, everyone needs to chill out.

>"I've been holding a handful of Ethereum since there was a decent dip in the price. I haven't spent much time on it and I have no good leads for program ideas yet, but if the code is buggy and I get hacked and lose my investment, that's fine. A smart contract is a project, and it could fail like any other. Don't put your retirement savings in a smart contract right now unless you're OK with losing it all. Maybe in the future Ethereum will move beyond this phase, and maybe not. All the drama is ridiculous, everyone needs to chill out."

This is the exact spiel we're all sick of hearing.

Why are you sick of hearing it? Why are you even in this thread? If ethereum is so dumb, why do you care so much?

because you're shilling for a pyramid scheme , and it's not even a secure pyramid scheme. the software its's built on is shit, from top to bottom.

The people writing programs on it are writing bad programs.. but even if they write them well the environment has vulnerability built into it .

>Why are you even in this thread?

Why are you here? it's one of the top posts on this site today.

Which part do you have a problem with?

>I've been holding a handful of Ethereum since there was a decent dip in the price.

You opened by explain how you clearly have an interest in this, you got in, and since you are saying you bought during a "decent dip" that means you only got in recently.

The rest of your post would be shilling only that you disclosed your interest.

> The rest of your post would be shilling only that you disclosed your interest.

So I would be shilling in a hypothetical scenario, and that's the problem?

OK, whatever. Have a nice day.

That's the problem yes, you bought into a pyramid scheme and you need others to buy in if you want to get out with more money.

The other sad thing is that Solidity, the language of Etherium, is a trainwreck. It has tons of bugs, properties that maximize the memory cost of the program, and until ~6 days ago had crazy double init bugs in constructors using "this".

Looking at Solidity's release log, the last update was 18 days ago. It fixed some minor bugs from the previous release three days prior, and none of the bugfixes mentioned in the previous release seem to fit your description. Do you have a link?

https://github.com/ethereum/solidity/releases

A look at the recent commits would suggest they are correct: https://github.com/ethereum/solidity/commit/e506129aee5745e2...

That's just an added warning, not a bug fix.

Indeed, I mistook the added warning and ticket close for the real fix.

I'm sorry, 18 days, not ~6. I said 1/3rd the real duration. Since Solidity has only been around about 800 days, 12 days is a non-trivial error.

Still: my complaint that the language is poorly architected and dubiously implemented and tested stands.

I still don't see a bugfix that matches your complaint. The warning is about the compiler behaving as designed; it's for programmers who are probably using that behavior incorrectly.

Solidity definitely has design warts; possibly Viper will end up the leading language, once it's production-ready.

Worth mentioning that there is at least one other language being built on top of the EVM:

https://github.com/pirapira/bamboo

This one takes a strict state machine approach, and aims to solve some of the tricky reentry and state tracking problems of Solidity.

"but the takeover-the-world echo-chambers of ethereum that don't focus at all on the real tech behind it and ignore everything negative is pretty disappointing" i dont think this is a good representation of the ethereum community, most people on r/ethereum for example are quiet self conscious about the security issues. that is at least my impression from reading the threads there.

"90s cypherpunks that pioneered this ideas had considered Turing complete design and discarded it for cryptographic state-machines that allow for formal verification" - are you referring to Bitcoin?

Or some other ideas that aren't currently implemented?

When it comes to contracts I think a more interesting idea is a limited formal expression of them and thus automatic production and evaluation/translation/summaries (would require a formal spec for each domain with very limited options), not a Turing complete expression of them which as you say leaves too many holes. Also tying all of this to a currency and payments makes zero sense and just expands the attack surface massively. Just fixing contract law with automated checks of contracts would be a huge opportunity/challenge.

> Ethereum software has security hole, gets hacked

The exploits so far were NOT security holes in ethereum, they were poorly written smart contracts by third parties.....

That's pretty like early days of web development when people write SQL-injection vulnerable code on daily-basis