Haseeb-Qureshi

Formally Verifying Dapps from the Ground up

Martin Lundfall, MKR

K Framework

• Allows you to define a programming language by specifying a:
  • Syntax
    • via BNF notation
  • Configuration
    • state according to your VM, things like stack, memory, storage, etc.

• Rewrite rules

Haseeb-Qureshi

// From: https://github.com/bitcoin/bitcoin/blob/master/src/chainparams.cpp

        vSeeds.emplace_back("seed.bitcoin.sipa.be"); // Pieter Wuille, only supports x1, x5, x9, and xd
        vSeeds.emplace_back("dnsseed.bluematt.me"); // Matt Corallo, only supports x9
        vSeeds.emplace_back("dnsseed.bitcoin.dashjr.org"); // Luke Dashjr
        vSeeds.emplace_back("seed.bitcoinstats.com"); // Christian Decker, supports x1 - xf
        vSeeds.emplace_back("seed.bitcoin.jonasschnelli.ch"); // Jonas Schnelli, only supports x1, x5, x9, and xd
        vSeeds.emplace_back("seed.btc.petertodd.org"); // Peter Todd, only supports x1, x5, x9, and xd
        vSeeds.emplace_back("seed.bitcoin.sprovoost.nl"); // Sjors Provoost
        vSeeds.emplace_back("dnsseed.emzy.de"); // Stephan Oeste

Haseeb-Qureshi

# JSON Resume

[JSON Resume] is an easy way to produce an adaptible and professional-looking resume. We recommend that you use it. It'll save you a lot of headaches about formatting, file types, and the like. Plus, it'll make you look like you know how to Internet.

This is what the underlying format looks like:
```
{
  "basics": {
    "name": "John Doe",
    "label": "Programmer",

Haseeb-Qureshi

Zexe: Enabling Decentralized Private Computation

Speaker: Pratyush Mishra

• How can we do computing on distributed ledgers?
  • Many existing systems for smart contract execution
    • Ethereum, Tezos, EOS, etc.
  • They all work through re-computation—every party redundantly performs the computations to agree on state
  • This comes with scalability tradeoffs
    • Recomputing all of these programs is costly

• Weakest computers (e.g. cell phones) can't keep up recomputing all transactions

Haseeb-Qureshi

Formal verification: the road to complete security of smart contracts

Martin Lundfall (MakerDao)

• What is formal verification?
  • Process of specifying and verifying the behavior of programs
  • Specification: mathematical description of intended program behavior
  • Verification: operational semantics of a language -> spec -> proof
  • There are 4 different "flavors" of assurances that formal verification can provide
    • 1. Smart contract bytecode verification - "Full description of EVM behavior"

• What can happen over the course of one transaction?

Haseeb-Qureshi

Privacy-preserving Multi-hop Locks for Blockchain Scalability and Interoperability

Speaker: Pedro Monero-Sanchez

• Payment channels are a widely pursued layer 2 scaling solution
  • But they only solve for bidirectional payments (between the two parties who open the channel)
• What if we build a payment channel network?
  • Naive solution—every pair of parties (N^2) opens a channel with each other
    • But then we need to lock up an exorbitant amount of capital in all these channels
  • Instead, let's open a few channels for each party

• And rely on other intermediary channels to reach the intended receiver

Haseeb-Qureshi

New and Simple Consensus Algorithms for ThunderCore’s MainNet

Speaker: Elaine Shi

• Synchronous, with a change of partition tolerance
• State machine replication (e.g., blockchain consensus)
  • Requires safety (nothing bad ever happens), and liveness (eventually something good happens)
• Thunderella
  • If you don't know Thunderella, go look it up (check out the BPASE '18 talk)
• Wait, there's a flaw in Thunderella?!

• A confirmed transaction can be undone, even in a somewhat benign setting

Haseeb-Qureshi

Building Mimblewimble/Grin, an implementation for privacy and scalability

Speaker: Quentin Le Sceller

• MimbleWimble
  • Proposed anonymously in IRC by Tom Elvis Jedusor
  • Private by default
  • Massively prunable
  • Relies solely on elliptic curve cryptography
  • No scripting
• MW transactions consist of:

Haseeb-Qureshi

The Case for Application-Specific Blockchains

Loi Luu, Kyber Network

Why Loi Luu is a badass

• Designed Elastico, first peer-reviewed sharding protocol for public blockchain
  • Inspired Zilliqa
• Created Oyente, first open-source smart contract verifier
  • Used by Melonport, Quantstamp, Augur
• Co-founder at Kyber Network

• On-chain liquidity protocol for token swaps

Haseeb-Qureshi

The Gap Game

Itay Tsabary, Technion

Headline result: miners in PoW are incentivized to shut off their hardware occasionally.

Proof of Work

• Find a value for which a protocol-defined condition holds
  • In Bitcoin, hash(block) < K
• Memory-less process
• PoW is very expensive