Simple Verified DApps
not just Smart Contracts
Why DApps are the very hardest programs to write
&
How our DApp language can help

François-René Rideau, CEO,  Mutual Knowledge Systems
EthCC[3] 2020-03-03 video: https://youtu.be/VJ8CzqLGsu8
Slides: https://mukn.io/ethcc2020/
PgDn: nextPgUp: previous↑ ↓ ← → ESC ⏎ Touchscreen: swipe down until you must swipe right

Introduction: The Hardest Programs To Write

Introduction: The Hardest Programs To Write

Decentralized Applications

The DApp market: billions of dollars
Transitioning to trillions?
Instead, it's slumping

Introduction: The Hardest Programs To Write

Vicious Cycle

No apps
No techNo users
No money


Introduction: The Hardest Programs To Write

Virtuous Cycle

Mo' apps
Mo' techMo' users
Mo' money


Typical bootstrapping issue!

Introduction: The Hardest Programs To Write

What Missing Tech?

Scalability

Portability

Interoperability

Usability

Flawless Security

Introduction: The Hardest Programs To Write

Issues

Costs: from $80k to write and audit, to millions
Risks: audit is still not enough, even for small DApps
Volatility: each DApp tied to a single blockchain
But what if we could solve these issues?

Introduction: The Hardest Programs To Write

Why is Blockchain Security so Hard?

1. Zero tolerance to bug
2. All code is fragile
3. Active Adversaries
4. All code is public
5. Usual reasoning techniques are lacking
DApps are the Very Hardest Programs to Write!

Introduction: The Hardest Programs To Write

The Solution: Logic

Dijkstra's approach: prove all code correct with formal logic.
DApps require Domain-Specific Logic
Logic can't be retrofitted into a DApp
Complexity makes logic intractable
You may eschew logic automation—bad guys won't.

Introduction: The Hardest Programs To Write

MuKn: MUtual KNowledge

Solving the hardest problem: making DApps safe to write
A Domain-Specific Language (DSL) for DApps
With builtin Domain-Specific Logic for DApps
Not just smart contracts, also matching client/server code
MuKn.io — looking for early customers, investors

Glow: MuKn's DApp Language

Glow: MuKn's DApp Language

What's a DApp?

An interaction, between
Multiple untrusting parties, exchanging
Assets on public ledgers, subject to
algorithmically verifiable rules

Glow: MuKn's DApp Language

Example: Rock, Paper, Scissors

Total 22 loc
data Hand = | Rock | Paper | Scissors;
data Outcome = | B_Wins | Draw | A_Wins;
let winner = (handA : Hand, handB : Hand) : Outcome => {
    NatToOutcome((HandToNat(handA) + 4 - HandToNat(handB)) % 3) }
@interaction([A, B])
let rockPaperScissors = (wagerAmt) => {
    @A assert! canReach(end, end.outcome == A_Wins);
    @A let handA = inputHand("First player, pick your hand");
    @A let salt = randomUInt256();
    @A @verifiably let commitment = digest(salt, handA);
    @A publish! commitment; @A deposit! wagerAmt; };
    @B assert! canReach(end, end.outcome == B_Wins);
    @B let handB = inputHand("Second player, pick your hand");
    @B publish! handB; @B deposit! wagerAmt; };
    @A publish! salt, handA;
    verify! commitment;
    let outcome = winner(handA, handB);
  end: switch(outcome) {
      | A_Wins => withdraw! A, 2*wagerAmt
      | B_Wins => withdraw! B, 2*wagerAmt
      | Draw => withdraw! A, wagerAmt; withdraw! B, wagerAmt }}

Glow: MuKn's DApp Language

Zooming on the Setup

data Hand = | Rock | Paper | Scissors;                        
data Outcome = | B_Wins | Draw | A_Wins;                      
let winner = (handA : Hand, handB : Hand) : Outcome => {      
 NatToOutcome((HandToNat(handA) + 4 - HandToNat(handB)) % 3) }
@interaction([A, B])                                          
let rockPaperScissors = (wagerAmt) => {                       

Glow: MuKn's DApp Language

Zooming on the Interaction

@A assert! canReach(end, end.outcome == A_Wins);              
@A let handA = inputHand("First player, pick your hand");     
@A let salt = randomUInt256();                                
@A @verifiably let commitment = digest(salt, handA);          
@A publish! commitment; @A deposit! wagerAmt;                 
@B assert! canReach(end, end.outcome == B_Wins);              
@B let handB = inputHand("Second player, pick your hand");    
@B publish! handB; @B deposit! wagerAmt;                      
@A publish! salt, handA;                                      
verify! commitment;                                           
let outcome = winner(handA, handB);                           
end: switch(outcome) {                                        
| A_Wins => withdraw! A, 2*wagerAmt                           
| B_Wins => withdraw! B, 2*wagerAmt                           
| Draw => withdraw! A, wagerAmt; withdraw! B, wagerAmt}}      

Glow: MuKn's DApp Language

Generated smart contract

About 60 loc. Excerpt for third transaction:
event e2(uint256 salt, uint256 handA);
function m2(address payable pA, address payable pB, uint256 wagerAmt,
            uint256 escrowAmt, uint256 commitment, uint256 handB,
            uint256 salt, uint256 handA) external payable {
  require(current_state == uint256(keccak256(abi.encodePacked(
    uint256(2), pA, pB, wagerAmt, escrowAmt, commitment, handB))));
  require(msg.sender == pA);
  require(msg.value == uint256(0));
  require(commitment == uint256(keccak256(abi.encodePacked(salt, handA))));
  require(handA < 3);
  uint256 outcome = handA + (4 - handB) % 3;
  bool a_wins = outcome == 2;
  bool b_wins = outcome == 0;
  pA.transfer(escrowAmt + a_wins ? 2*wagerAmt : b_wins ? 0 : wagerAmt);
  pB.transfer(a_wins ? 0 : b_wins ? 2*wagerAmt : 0);
  emit e2(salt, handA);
  current_state = 0x0;
  selfdestruct(residualRecipient);}

Glow: MuKn's DApp Language

Generated client code for player A

21 loc
export async function A(stdlib, ctc, input, wagerAmt, escrowAmt) {
  const {assert, eq, lt, add, sub, mod, keccak256, uint256_to_bytes, bytes_cat}
        = stdlib;
  const hash = (x, y) => keccak256(bytes_cat(uint256_to_bytes(x), uint256_to_bytes(y)));
  const isHand = (x) => lt(x, 3);
  const handA = await input("First player, pick your hand");
  assert(isHand(handA));
  const salt = random_uint256();
  const commitment = hash(salt, handA);
  const state0 = {_state:0, wagerAmt, escrowAmt, salt, handA, commitment};
  await ctc.send("A", "m0", state0, add(wagerAmt, escrowAmt),
                 [wagerAmt, escrowAmt, commitment]);
  const [handB, txn1] = await ctc.recv("A", "e1", state0);
  assert(eq(txn1.value, wagerAmt));
  assert(isHand(handB));
  const outcome = mod(add(handA, sub(4, handB)), 3);
  const state2 = {...state0, _state: 2, handB, outcome};
  await ctc.send("A", "m2", state2, 0,
                 [wagerAmt, escrowAmt, commitment, handB, salt, handA]);
  return state2;
}

Glow: MuKn's DApp Language

Generated client code for player B

22 loc
export async function B(stdlib, ctc, input, wagerAmt, escrowAmt) {
  const {assert, eq, lt, add, sub, mod, keccak256, uint256_to_bytes, bytes_cat}
        = stdlib;
  const hash = (x, y) => keccak256(bytes_cat(uint256_to_bytes(x), uint256_to_bytes(y)));
  const isHand = (x) => lt(x, 3);
  const state = {wagerAmt, escrowAmt};
  await [wagerAmt0, escrowAmt0, commitment, txn0] = ctc.recv("B", "e0", state);
  assert(wagerAmt0 == wagerAmt);
  assert(escrowAmt0 == escrowAmt);
  const handB = await input("Second player, pick your hand");
  assert(isHand(handB));
  const state1 = {...state, _state:1, salt, handA, commitment, handB};
  await ctc.send("B", "m1", state1, wagerAmt,
                 [handB]);
  const [salt, handA, txn2] = await ctc.recv("B", "e2", state1);
  assert(eq(txn2.value, 0));
  assert(isHand(handA));
  assert(eq(commitment, hash(salt, handA)));
  const outcome = mod(add(handA, sub(4, handB)), 3);
  const state2 = {...state1, _state: 2, salt, handA, outcome};
  return state2;
}

Glow: MuKn's DApp Language

Generated interface declarations

export const ABI = [
  {"type":"constructor","inputs":[{"name":"pA","type":"address"},{"name":"pB","type":"address"}],"payable":true,"stateMutability":"payable"},
  {"name":"timeout","type":"function","outputs":[],"inputs":[],"constant":false,"payable":true,"stateMutability":"payable",},
  {"name":"etimeout","type":"event","inputs":[{"indexed":false,"name":"m","type":"address"}],"anonymous":false},
  {"name":"m0","type":"function","outputs":[],"inputs":[{"name":"pA","type":"address"},{"name":"pB","type":"address"},{"name":"wagerAmt","type":"uint256"},{"name":"escrowAmt","type":"uint256"},{"name":"commitment","type":"uint256"}],"constant":false,"payable":true,"stateMutability":"payable"},
  {"name":"e0","type":"event","inputs":[{"indexed":false,"name":"wagerAmt","type":"uint256"},{"indexed":false,"name":"escrowAmt","type":"uint256"},{"indexed":false,"name":"commitment","type":"uint256"}],"anonymous":false},
  {"name":"m1","type":"function","outputs":[],"inputs":[{"name":"pA","type":"address"},{"name":"pB","type":"address"},{"name":"wagerAmt","type":"uint256"},{"name":"escrowAmt","type":"uint256"},{"name":"commitment","type":"uint256"},{"name":"handB","type":"uint256"}],"constant":false,"payable":true,"stateMutability":"payable"},
  {"name":"e1","type":"event","inputs":[{"indexed":false,"name":"handB","type":"uint256"}],"anonymous":false},
  {"name":"m2","type":"function","outputs":[],"inputs":[{"name":"pA","type":"address"},{"name":"pB","type":"address"},{"name":"wagerAmt","type":"uint256"},{"name":"escrowAmt","type":"uint256"},{"name":"commitment","type":"uint256"},{"name":"handB","type":"uint256"},{"name":"salt","type":"uint256"},{"name":"handA","type":"uint256"}],"constant":false,"payable":true,"stateMutability":"payable"},
  {"name":"e2","type":"event","inputs":[{"indexed":false,"name":"salt","type":"uint256"},{"indexed":false,"name":"handA","type":"uint256"}],"anonymous":false}];

Glow: MuKn's DApp Language

Generated logic spec

2 kloc of z3 interaction. TODO: make it readable
Ledger always balanced, never negative, zero when done
Liveness: OK when everyone cooperates
Safety: OK when some participants don't
User-specified: know your DApp

Glow: MuKn's DApp Language

What else can we automate?

Escrow to incentivize continued cooperation
Merkleization of contract state
Generalized State Channels vs Direct Style
privacy via MAST, zkSNARKs
Generation for other blockchains

Glow: MuKn's DApp Language

Why does it matter?

A fraction of the effort
Code stays in synch as spec evolves
Safer thanks to formal methods
Optimizations you wouldn't afford by hand
Portable to any blockchain

Glow: MuKn's DApp Language

Why is MuKn the right company?

Intersection of Blockchain, Economics, Computing, Logic, Design
Passion of all my career
Left research for industry to build usable systems
My partner: litigator also excited by adversarial environments

Attack Model

Attack Model

Abstraction Failures

DAO hack ($60M): reentrancy issue
Parity Wallet hack 1 (30M$): bad access delegation
Parity Wallet hack 2 (280M$): library destruction
Many other M$ hacks : bad or missing permission checks
Solution: better programming model, well-implemented once

Attack Model

Misplaced Trust

Exchange hacks: mistrusted centralized custody (>$1G)
DeFi hacks: mistrusted centralized oracle (>$25M)
Make trust assumptions explicit
Killer DApps: non-custodial DEX, decentralized oracles

Attack Model

Lower-level Attacks

Stolen Keys: attack on IT, on crypto
Network DoS: attack on network infrastructure
Economic DoS: block-buying à la FOMO3D
Systems Programming Bug: data loss, security vulnerability
Distributed Systems Bug: data loss, stuck systems, bad config…
A lot of specialized engineering required

Attack Model

Expertise Need with or without Glow

Business Logic!
Distributed Systems, Systems Programming
Economic Modelling, Economic Mechanism Design
Cryptography, Information Security
Programming Language use, PL implementation
... Management
Sharing costs and expertise

Conclusion

Conclusion

MuKn: MUtual KNowledge (bis)

Solving the hardest problem: making DApps safe to write
A Domain-Specific Language (DSL) for DApps
With builtin Domain-Specific Logic for DApps
Not just smart contracts, also matching client/server code
MuKn.io — looking for early customers, investors

Conclusion

MuKn: Business Plan

1. Open-Source language, so much better everyone uses it
2. Build Killer DApps to demonstrate value
3. Sell support services
4. Sell custom and proprietary extensions
5. Fees from subscriptions, saved gas, referrals
6. All-blockchains service marketplace
Commoditize blockchains

Conclusion

The Meta-Story

The importance of Simplicity
Intersection of Blockchain, Economics, Computing, Logic, Design
Give back our users control on their digital sovereignty
Internet 3.0

Conclusion

For More Information

Our Website & Whitepaper   https://mukn.io
Our News Feed   https://twitter.com/MutualKnowledge
Our Code:   https://gitlab.com/mukn
Join Us!   contact@mukn.io
Questions?