13 ms·
How We Proved the Eth2 Deposit Contract Is Free of Runtime Errors
- unixhero 5y agoThis is what certik tries to solve. I just don't understand why smart contracts need certik to be verified.
- lima 5y ago> I just don't understand why smart contracts need certik to be verified. How would CertiK sell their token otherwise? :p
- 19h 5y agoHow does one prove the correctness of the correctness proofs?
- jkhdigital 5y agoGotta formally verify the source code of the proof checker… then the entire bootstrapped tool chain that was needed to compile it. No big deal
- junon 5y agoGenerally using a language like OCaml, which is the language of choice for most large formal proofing projects.
- AmericanChopper 5y agoYou can’t. The headline is missing a piece of context in that the proved it was free of runtime errors… according to a specification they chose to evaluate it against. What if their specification contained an error? You could verify that specification against another specification, you could even do that formally if you want to. Eventually you have to confront Gödel’s incompleteness theorem, and accept that such a level of proof is not possible. Formal verification btw is just a formalised methodology for evaluating something against a specification. It doesn’t prove that errors don’t exist, or that the verifier hasn’t managed to independently make their own error. It’s just a rigorous PR.
- pharmakom 5y agoThe idea is that we have more confidence in the model and model checker than the actual code. At the very least, this is a form of double entry.
- k__ 5y agoWeren't there some efforts in a new, safer language for the EVM? I think, Vyper or something. What happened?
- casi18 5y agoVyper has safe math built in, so you wont get accidental over/underflows. but Solidity also has that now in the newer versions. so its really a preference if you prefer the python-like text. Fe is also being developed, looks like it has been planned out a bit more than vyper. But more likely we will see developments of security and proofs in languages like cairo, to be used on zkrollups, where we will also see alternative VMs to the EVM. So there will be lots of options with different tradeoffs between composability/security/efficiency/redundancy.
- mypastself 5y agoI think Solidity won out due to to the ease of developer adoption (unlike Vyper, it is object-oriented). ETH2’s EVM replacement, EWASM, will use WebAssembly, so developers should be able to use saner programming languages than Solidity.
- jkhdigital 5y agoCall me old fashioned, but I’m of the opinion that every “smart contract” should come with a machine-checkable proof of correctness.
- casi18 5y agoI think we will see more work like this, and tools developed to help. but really it comes down to tradeoffs of speed and security, what cant be insured, and the impact of bugs. you might have an uninsured contract with multiple audits and proofs of correctness, vs an insured contract with one quick review. which one would you put money into?
- nicoburns 5y agoNeither? I'd much rather use a traditional contract that can fallback on the legal system if need be.
- bbarnett 5y agoA handshake can be a binding contract. Words spoken can bind you. Thus, eth contracts can be enforced by civil courts too, if there is some chicanery going on...
- dsr_ 5y ago...as long as all the participants are traceable entities with known legal jurisdictions.
- jacquesm 5y agoYes, but that would invalidate a very large chunk of the possible usecases for eth contracts. After all, if you end up needing the courts anyway you might as well use a normal contract, and the whole advantage of eth contracts - to me at least - appears to be the feature that the eth contract is the entirety of the arrangement. So it can be used between two parties in entirely different jurisdictions without that creating an imbalance.
- Taikonerd 5y agoYou know, I'm not really into cryptocurrency, but it does seem like it's contributing to a resurgence of interest in formal methods. So - thank you, cryptocurrency community!
- galangalalgol 5y agoI've worked on safety critical software, but we did not use formal methods. Lots of test and checking for coverage (at asm level). Oodles of static analysis and wading through false positives. Do formal methods usually supplement those or replace some of it? Can provers or formal methodologies scale to safety critical codebases of 100s of ksloc? Whether such codebases should exist, or be better partitioned is a separate issue.
- notimrelakatos 5y agoFormal methods seems to be perfect for verifying protocols, specially finding design flaws, here an example of an ongoing effort to verify TLS https://www.mitls.org/ https://www.mitls.org/ https://github.com/project-everest/mitls-fstar https://github.com/project-everest/mitls-fstar
- someguyorother 5y agoThe current crowning achievement of formal methods is, as I understand it, seL4. It is a formally proven microkernel of about 8500 LOC. There's still a while to go until they can scale to 100kLOCs, unfortunately.
- nextaccountic 5y agoCompCert is also very impressive. It's not, however, free software / open source (the source is available though) https://www.absint.com/compcert/structure.htm https://www.absint.com/compcert/structure.htm A problem with both seL4 and CompCert is that the code written to express the proofs is huge, much larger than code that actually does stuff. This puts a ceiling on the size of the projects we can verify. F* is a language that tries to address that, by finding proofs with z3, a smt prover; z3 can't prove everything on its own but it cuts down proof code by orders of magnitude. They have written a verified cryptography stack and TLS stack, and want to write a whole verified http stack. https://www.fstar-lang.org/ https://www.fstar-lang.org/ https://github.com/project-everest/hacl-star https://github.com/project-everest/hacl-star https://www.mitls.org/ https://www.mitls.org/ https://project-everest.github.io/ https://project-everest.github.io/ F* (through Low, a verified low-level subset of F) can extract verified code to C, which is kind of the inverse than the seL4 proof: seL4 begins with C code and enriches it with proofs of correctness; hacl* (a verified crypto F* lib) begins with a proven correct F* code and extracts C code (I gather the actual crypto primitives is compiled directly to asm code because C has some problems with constant time stuff). This enables hacl* to make bindings to other languages that can just call C code, like this Rust binding https://github.com/franziskuskiefer/evercrypt-rust https://github.com/franziskuskiefer/evercrypt-rust Also this F* stuff is all free software / open source, so it might become a very prevalent crypto and TLS stack
- jeffrallen 5y agoThis was is great! And also, as a long time observer of software correctness proof fails, I'm getting the old popcorn popper ready for the first instance where there's a bug and then we'll have explained to us that, well actually, the prover wasn't covering that case...
- nlitened 5y agoNo biggie, they will just make a new fork of modified ETH blockchain where this error is fixed, and all the users will follow.
- 0des 5y agoA lot of folks might think this is you pushawing on ETH because you invested differently, but this is quite literally the established track record. For the uninitiated, this is how we got Ethereum and Ethereum Classic. I'd be interested in some of the downvoters making a sound rebuttal rather than graying you into obsolescence but it's 2021. The filter bubble expands thusly.
- whoknowswhat11 5y agoEXACTLY this. It'll be like - oh we proved it using X, but wrote code using Y and ooops, there is some difference so this doesn't count as a break in the proof. If that's the case, you have not in fact proved the contract, you've proved a different contract or code base.
- throwaway98797 5y agoIt’s all good until it isn’t.
- klik99 5y agoThe formal proof stuff is very cool, but I'm getting some unsinkable titanic vibes from how they present this.
- mabbo 5y agoAdmittedly I'm being a bit trollish as I say this, but do you get the same feeling from proofs that Pythagorean Theorem is correct? Proving things correct is much harder than finding counter-examples that they aren't correct. But the methods do work. Their based on sound formal logic. Proofs can have mistakes, certainly, but it's a darn strong signal that their system is correct.
- tikhonj 5y agoThe problem with proving things about software is less in the proof itself and more in the connection between the proof and the real world. If somebody told me that they had a financial system whose security was based on applying the Pythagorean Theorem to physical triangles, it would raise exactly the same red flags—the theorem itself isn't a question, but it doesn't even try to capture how physical materials might be imperfect or change over time, and those are exactly the sort of inconsistencies a motivated attacker could exploit.
- klik99 5y agoI was going to reply but exactly this - I'll add that the proof work in the article is really interesting and I love to see practical work in formal proofs happening as a result of eth in particular. However 100% proven code on eth I just don't believe is 100% trustworthy. Another way of phrasing it is that the law of leaky abstractions means that though the code itself might be 100% correct, lower levels can puncture the assumptions and make that correctness moot - IE, unsinkable titanic vibes
- deleted 5y ago[deleted]
- hibikir 5y agoFormal methods are good and all, but you can still run into trouble when you fail to account for everything. Some years ago, I had to work on a massively distributed system that scaled up or down with minimal communication between nodes, depending on the amount of work the system had. The developer of that scaling algorithm, a mathematician that gives quite a few software talks, and writes books teaching functional programming, wrote a proof for the system, guaranteeing its upper and lower bounds of performance. I was brought in because the system wasn't acting anywhere near those parameters: The worst part was that often it'd not downscale at all. The mathematician pointed at his proof, and therefore at the fact that if there was a problem, it must be a bug somewhere else. So after learning how to read his proof, executing it, and doing all the typical ops stuff to identify what the system believed was going on at any particular time, it became clear that the proof had a significant flaw: It believed that the amount of work that the system received was perfect information, with no latency. Since the real world has latency, and none of that was accounted for, the proof was guaranteeing success in a universe that is different from ours. Once I modified the model to represent the real information quality, the outcomes were pretty close to what we were seeing in reality, and equally unacceptable. So proofs are powerful, and maybe there are zero issues in the proof of this smart contract, but formal models and proofs can still fail you, they'll just fail far less often than your typical system made with unit tests and chewing gum.
- wilde 5y agoCan Etherium run contracts written in Dafny? This is cool, but it doesn’t guarantee that the Solidity matches the proof at all, does it?
- schelling42 5y agoIt is spelled Ethereum.
- vmception 5y agoEh staking Eth2 fits my risk profile and I dont care if another TheDao incident occurs resulting in loss of my Eth A state rollback would be extremely disappointing to me, even though that much Eth in the hands of one party would undermine the security of Eth2 (which is why the other state rollback occurred) This proof is impressive, but doesnt change anything for me whether it is bulletproof or not
- rfd4sgmk8u 5y agoYou are ok with losing $100k of collateral? I just don't have the fortitude to put that much on the line. I could... but I don't think it is wise. I still don't believe this migration is going to happen at all. If you look at the PoS blocks from other EVM chains, you see that reorgs happen way too often to be comfortable with $100B of assets.
- juskrey 5y agoBut not from logical, especially forward compatibility errors?
- pidge 5y agoTo clarify, they implemented the algorithm in Dafny, and then proved that version correct. They did not verify code that will actually run in production. From the paper: > Dafny is a practical option for the verification of mission-critical smart contracts, and a possible avenue for adoption could be to extend the Dafny code generator engine to support Solidity … or to automatically translate Solidity into Dafny. We are currently evaluating these options
- X6S1x6Okd1st 5y agoAdditionally it's proving a translation of the algorithm implemented in solidity. Solidity is not what is run on Ethereum, EVM bytecode is. Solidity is compiled down to EVM bytecode and that's what is run. That seems like another point where a bug could creep in. I wouldn't be surprised if there was a hard fork to save the deposit contract if there was a critical bug discovered.
- latchkey 5y agoThere will be many hard forks before the funds from the deposit contract can be retrieved.
- X6S1x6Okd1st 5y agoFair enough, non-contentious hard forks in Ethereum are usually called upgrades at this point.
- yissp 5y agoI mean if there was a critical bug in the solidity compiler itself that would put the correctness of pretty much every contract into question, right? It seems like a fork would be hard to argue against in that case.
- ilammy 5y ago“Beware of bugs in the above code; I have only proved it correct, not tried it.” — D.E.K.
- 5y ago
- agomez314 5y agoNothing motivates people to do the hard work than money!
- goolulusaurs 5y agoWithout knowing much about the topic, when I hear about code being proven to be correct it makes me think of the Curry-Howard correspondence, which states that proofs and programs are isomorphic to each other. Is this related at all? If programs and proofs are the same thing and you have a proof that a program is correct, is that like having a proof that a proof is correct? In which case it seems like you are getting into the domain of meta-logic.
- skybrian 5y agoNo, not really. Under Curry-Howard, if you have a total function that returns an integer, you’ve proven that an integer exists. But we knew that already. To prove non-trivial things, you need more sophisticated types that make interesting assertions about their values, where it’s not immediately obvious how to construct a value of that type. Special proof languages are used for this.
- fooker 5y agoIt is related, but not in the way you are imagining.
- joelbondurant 5y agoJust store your pngs in MongoDB.
- deleted 5y ago[deleted]