In which we're talking about what it feels like to write code for ethereum contacts…
I didn't know much about the topic, some of the main takeaways for me:
1. Smart contact is like a microservice: a stateful program with a public API
2. Unlike a microservice, the code, the state and all the calls to it are publicly available & are immutable (b/c blockchain)…
1. Smart contact is like a microservice: a stateful program with a public API
2. Unlike a microservice, the code, the state and all the calls to it are publicly available & are immutable (b/c blockchain)…
3. Unlike a microservice, you don't need a server to run the code, it's run by the ethereum network in a P2P fashion
4. The native language of Ethereum is assembly-like set of opcodes
5. Executing a transaction (a call to an API) costs money, priced per opcode…
4. The native language of Ethereum is assembly-like set of opcodes
5. Executing a transaction (a call to an API) costs money, priced per opcode…
6. There's a bunch of languages, that compile to EVM assembly. Solidity is the default one, a C-like lang w/inheritance & many other means to shoot yourself in the foot
7. 2 bugs in Parity multisig wallet show how easy it is to get it wrong: $300M in $eth stolen or frozen…
7. 2 bugs in Parity multisig wallet show how easy it is to get it wrong: $300M in $eth stolen or frozen…
8. "Code was not audited" is one reason people voiced. Another one: dev tools & practices are immature, seems more fitting to me.
9. It's easy to: deploy a new contract, find & exploit bugs. It's very hard to: fix & redeploy a contract, fix results of an exploit…
9. It's easy to: deploy a new contract, find & exploit bugs. It's very hard to: fix & redeploy a contract, fix results of an exploit…
10. So what kind of infra can help prevent these kind of bugs? Let's break down the problem:
10.1. We need to know what contacts should and shouldn't do (good specs)
10.2. We need to know that the actual code matches the spec (good implementation)
10.1. We need to know what contacts should and shouldn't do (good specs)
10.2. We need to know that the actual code matches the spec (good implementation)
11. For better specs there's not much in terms of tools. There's thehydra.io They run several implementations of the same contract simultaneously. If someone figures out a series of calls that lead to different results in different implementations, they found a bug…
…the bug could be in one of the implementations, but also could be in the spec (e.g. unspecified behavior)
12. For finding bugs in an implementation of a contract we can use classic methods e.g. unit & integration tests (good to catch regressions) or we can use formal methods, like symbolic execution and deductive verification (good uncover unknown bugs)…
…btw something we didn't go into in the podcast, we can also use property-based testing (á la quickcheck) to uncover bugs as well
13. "Formal" verification means looking at the form (aka analysing the code itself)
14. For example, using symbolic execution or abstract interpretation we can construct a tree of possible execution paths. If one of those leads to a "selfdestruct" call, there could be a bug
14. For example, using symbolic execution or abstract interpretation we can construct a tree of possible execution paths. If one of those leads to a "selfdestruct" call, there could be a bug
15. Deductive verification means using maths (logic) to prove statements (theorems) about the code. Even with a proof assistant the process is very manual and effortful.
16. Having an advanced type system (e.g. dependent types) is a good balance between expressivity and ease of use. It's like doing deductive verification in the code with the help of a compiler
