Focus on Bitcoin and some other platforms.
Contents
A ledger of transactions
Replication among a dynamic set of nodes.
Decentralization
Smart Contracts
Programs or protocols that run on blockchains.
Possible to custom decentralized functionalities.
Platforms like Ethereum natively support smart contracts, but Bitcoin doesn't.
Why Formal Methods for Blockchain and Smart Contracts?
Errors cause huge economical losses.
Many platforms don't allow to modify contracts after deployment.
Formal verification of contracts prior of deployment is desirable.
Consensus
Consensus algorithm:
- Classical consensus
- Nakamoto consensus
- ...
Cryptographic Hash Functions
\(h:\{0,1\}^*\to\{0,1\}^n\) such that
- given \(h(x)\), finding \(x\) is computationally hard. (pre-image resistance)
- finding \(x\neq y\) s.t. \(h(x)=h(y)\) is computationally hard (collision resistance)
- given \(x\), finding \(y\) s.t. \(h(x)=h(y)\) is computationally hard (second pre-image resistance)
- \(h\) can be computed efficiently
On Collisions
\(\{0,1\}^*\) is bigger than \(\{0,1\}^n\), therefore collisions must exist.
How to find collisions: By brute force: try \(2^n+1\) distinct inputs. Finding such is computationally hard. If inputs are uniformly at random, \(2^{n/2}\) attempts lead to a collision with \(1/2\) probability. (Still exponential)
Realistic Hash Functions
Complex combination of simple operations
SHA256 (Bitcoin)
KECCAC256 (Ethereum), precursor of SHA3
Applications
Message digests, digital signatures...
In blockchain:
- Proof of work
- To link the previous block
- To link a block header to the list of transactions of the block.
Digital Signatures
Formally, a digital signature consists of 3 probabilistic polynomial algorithms (gen, sign, vrfy)
- gen returns a pair of keys (pk, sk), resp called public key and private key.
- sign takes in input a message \(m\) and a private key sk and returns a signature \(\sigma\)
- vrfy is deterministic, it takes in input a public key pk, a message \(m\) and a signature \(\sigma\), and check if the signature is equal to the value of message \(m\) crypted on pk.
A digital signature is used as follows
- A participant S runs gen and gets key pair.
- public key is broadcasted to the network, while sk is kept secret
Security of Signatures
The probability of successful attack (run in polynomial time) is low
Or to find a collision takes exponential time.
Desidarable Properties
Authentication: Receiver can verify sender's identity
Integrity: Modifying a signed message invalidates its signature
Non-repudiation: If an entity signs a message, she can't deny having signed it.
ECDSA
Elliptic Curve Digital Signature Algorithm
Both Bitcion and Ethereum use it for signing transactions.
Cryptocurrencies and Blockchians
A Naive Cryptocurrency
Each unit of currency is associated with a bit string (coin ID)
Currency is created by a special participant \(T\), which signs the newly generated coin \(<ID,SIGN_T(ID)>\), owned by \(T\).
The owner \(A\) of a coin \(c\) can spend it by generating \(<c,B,SIGN_A(c,B)>\) where \(B\) is the payee. After this transaction, \(B\) is the owner of the coin \(<c,B,SIGN_A(c,B)>\).
Problem: Double spending attack
Ruling out: Introducing a Trusted Authority (TA)
But TA can be problematic:
- It might become unreliable
Ruling out TA
Use p2p network of nodes
In order to avoid double spending, we need to record all payments
Transactions
Bitcoin transactions: units of currency can be split and multiple transactions can be spent at once
Ethereum has an account based model of transactions.
Transaction is in the block proves there is no double spending
Blockchains and Decentralization
How are new transactions added, and who adds them?
How do we ensure that all nodes have the same copy of the blockchain?
- Users broadcast their transactions to the network
- Nodes collect new transactions
- A randomly selected node groups the received transaction inside a block, appends it to the local copy of the blockchain and broadcasts the new block to the networks. If the block is valid the other nodes will append it to their local copies of the blockchain.
- The probability of being selected is not uniform: by computing power? on amount of currency owns?
- The selected node usually gets rewarded by some cryptocurrency.
Smart Contracts
Blockchians beyond Cryptocurrency
Blockchains were introduced in 2008 for implementing the Bitcoin cryptocurrency.
However, transactions doesn't need to be mere payments
In 2015, Ethereum blockchain was launched: it allows users to create custom programs (smart contracts) that run on the blockchain
On Smart Contracts
Proposed in 1994 by Nick Szabo.
A smart contract is a computerized transaction protocol that executes the terms of a contract.
Blockchains allow implementing smart contracts in a relative simple manner
Smart contracts exploit the following properties of programming languages
- unambiguous semantics
- executable
Implications of Contracts as Code
Contract clauses cannot be modified after stipulation
Code should be non-updatable
Problematic in case of buggy software
Decentralized Applications
dApps
Exchanges
DeFi (Decentralized Finance)
Market places
Gambling
Games