The basics of Ethereum are described in the Gavin Wood paper. A list of keywords in Solidity are described in this file from its source, which includes “address”, “contract”, “event”, “mapping” and “wei” ( 1 Eth= 10^18 Wei). This list does not include “gas”, which is a mechanism described in Wood’s paper to combat abuse. Interestingly the paper says “The first example of utilising the proof-of-work as a strong economic signal to secure a currency was by Vishnumurthy et al [2003]”, aka the Karma paper.

The karma paper talks about solving a cryptographic puzzle as enabling one to join the network and be assigned a bank set: “the node certifies that it completed this computation by encrypting challenges provided by its bank-set nodes with its private key. Thus each node is assigned an id beyond its immediate control, and acquires a public-private key pair that can be used in later stages of the protocol without having to rely on a public-key infrastructure”. Crypto puzzles for diverse problems have been proposed before, a survey and comparison is at https://pdfs.semanticscholar.org/d8b9/a0309cef8c309541876c9c2c5ad5c16c3b7a.pdf

The DAO attack had 3 components, a hacker, a malicious contract and a vulnerable contract. The malicious contract was used to withdraw funds from the vulnerable contract so that it never got to the code to decrement its balance. Oddly enough the gas mechanism which is supposed to limit (runaway) computation did not kick in to stop this repeated remittance.

A few weeks before the DAO attack someone had pointed out to me that security of solidity was a bit of an open problem. My feeling was contracts should be layered above the value exchange mechanism, not built into it. Bitcoin based protocols with the simpler OP_RETURN semantics appeared more solid. Later around October’16 at an Ethereum meetup, Fred Ehrsam made the comment that most new projects would be using Ethereum instead of bitcoin. But Bitcoin meetups had more real-world use cases being discussed. The technical limitations exist, which are being addressed by forks such as SegWit2x this November. Today saw a number of interesting proposals with Ethereum, including Dharma, DataWallet and BloomIDs. Security would be a continuing  concern with the expanding scope of such projects.

Sequence diagram of the attack, showing a double-withdraw –

More on Ethereum –

It uses the Keccac-256 hash function.

It supports the Ethereum Virtual Machine. The EVM is formally specified in section 9 of Gavin Wood paper. Some properties –

• computation on EVM is intrinsically tied to a parameter ‘gas’ which limits the amount of computation.
• stack based machine, with max stack depth of1024
• 256-bit word size. 256-bit stack item size. 256-bit chosen to facilitate Keccak-256 hash and Elliptic Curve computations
• machine halts on various exceptions including OOG (out of gas)
• memory model is a word-addressed byte-array
• program code is store in a ‘virtual ROM’ accessed via a specialized instruction
• runs state transition function

The state transition function takes as input – state σ, remaining gas g, and a tuple I.
The execution agent must provide in the execution environment, certain information, that are contained in the tuple I:
• Ia, the address of the account which owns the code that is executing.
• Io, the sender address of the transaction that originated this execution.
• Ip, the price of gas in the transaction that originated this execution.
• Id, the byte array that is the input data to this execution; if the execution agent is a transaction,
this would be the transaction data.
• Is, the address of the account which caused the code to be executing; if the execution agent is a
transaction, this would be the transaction sender.
• Iv , the value, in Wei, passed to this account as part of the same procedure as execution; if the
execution agent is a transaction, this would be the transaction value.
• Ib, the byte array that is the machine code to be executed.
• IH , the block header of the present block.
• Ie, the depth of the present message-call or contract-creation (i.e. the number of CALLs or
CREATEs being executed at present).
The execution model defines the function Ξ, which can compute the resultant state σ′, the remaining gas g′, the suicide list s, the log series l, the refunds r and the resul- tant output, o, given these definitions:
(115) (σ′, g′, s, l, r, o) ≡ Ξ(σ, g, I)

The official code is written in Golang (~640,000 lines). A code walkthrough is at https://www.mslinn.com/blog/2018/06/13/evm-source-walkthrough.html

The table of Opcodes is at https://github.com/ethereum/go-ethereum/blob/master/core/vm/jump_table.go

But what is a formal notion of a contract (specifically on the EVM which aims to generalize contracts) ? Is it any function. Is it a function of a specific template, expecting certain inputs/outputs. Can these functions be composed ?

The notions of contracts are delved in https://nakamotoinstitute.org/formalizing-securing-relationships/

“The contractual phases of search, negotiation, commitment, performance, and adjudication constitute the realm of smart contracts.”

Example – a vending machine. The machine ‘takes in coins and dispenses change and product according to the displayed price’, it is ‘a contract with bearer: anybody with coins can participate in an exchange with the vendor’.

So one can think of a smart contract as a digital vending machine. That’s actually a useful mental model. With a digital vending machine (DVM ?), the buyer can make a choice of what product buyer wants (of possibly very many – not limited to a physical machine), and be served that product upon due payment without interaction with another person or agency.