-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathvdacoab.html
18 lines (18 loc) · 5.42 KB
/
vdacoab.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link rel="stylesheet" href="resources/my.css" />
<link rel="stylesheet" href="resources/reveal/css/reveal.css" />
<link rel="stylesheet" href="resources/reveal/css/theme/black.css" />
<link rel="stylesheet" href="resources/reveal/lib/css/zenburn.css" />
<link rel="stylesheet" href="resources/my.css" /></head>
<body><div class="reveal"><div class="slides"><section><h1>Verifying dApp Computations on a Blockchain</h1><p> </p><p> </p><p>François-René Rideau, <em>Legicash</em></p><div align="center">fare@legi.cash</div><p> </p><p> </p><p>Deepspec Summer School 2018, July 19th 2018</p><a href="http://bbt.legi.cash/vdacoab.html"><tt>http://bbt.legi.cash/vdacoab.html</tt></a></section><section><h1>dApps I'd like to see</h1><p> </p><div align="left">Non-custodial Exchange: real-time match traders for atomic swaps</div><p> </p><div align="left">Cross Payment: I pay the Bitcoin I have, you get the ZCash you want</div><p> </p><div align="left">Supply Chain: log shipments and deliveries, automatic settlement</div><p> </p><div align="left">CryptoScalies: toys that can interact, not just be traded</div></section><section><h1>Issues with Cryptocurrency dApps</h1><p> </p><div align="left">Scale: from 10 tps to 10000 and beyond, latency 60 min to 6 s</div><p> </p><div align="left">Interoperate: contracts that bind across multiple blockchains</div><p> </p><div align="left">Be safe: don't lose USD 3e7 to one bug in 400 lines of code</div><p> </p><div align="left">Have a paradigm: not just random code and silly games</div></section><section><h1>Consensus as Judicial System</h1><p> </p><div align="left">An analogy is one abstraction, instantiated twice</div><p> </p><div align="left">Common Abstraction: dispute prevention and resolution system</div><p> </p><div align="left">Distinct Parameters: humans & rhetoric vs computers & logic</div><p> </p><div align="left">Common Observation: go to court to buy a house, not a drink</div></section><section><h1>What are <q>Smart Lawsuits</q>? Interactive Proofs!</h1><p> </p><div align="left">Game Semantics: Transform formula into verification game</div><p> </p><div align="left">Exhibit witness for my ∃. My ∀ is your ∃, so I challenge you.</div><p> </p><div align="left">One step per (dependent) product/sum alternation.</div><p> </p><div align="left">Skolemization: <tt>∀x:X ∃y:Y P(x,y)</tt> <em>becomes</em> <tt>∃f:X→Y ∀x:X P(x,f(x))</tt></div></section><section><h1>What Logic?</h1><div align="left">Game Theory: align participants' interests</div><div align="left">Game Semantics: validate past events</div><div align="left">Epistemic Logic: you are what you know</div><div align="left">Temporal Logic: multiple possible futures, timeouts</div><div align="left">Computability Logic: (game) Semantics first, syntax second</div><div align="left">... it already has Classical, Intuitionistic, Linear fragments</div><p> </p><div align="left">Coq: internal models, reflection and extraction</div><div align="left">Layers: verify the past, make the present, reason about future</div></section><section><h1>A Higher-Level Paradigm</h1><div align="left">Invariants for all future dApp evaluations (Coq)</div><div align="left">Regular behavior for each participant (OCaml)</div><div align="left">Referee to resolve disputes about past behavior (EVM)</div><div align="left">Strategies to argue the verification game in court (TBD)</div><div align="left">Vigilantism to watch the network and stop the bad guys (TBD)</div><div align="left">Counsel to explain consequences of (in)action (Expert System)</div><div align="left">Showcase for robustness vs attack scenarios (Integration Tests)</div><p> </p><div align="left">Low-level detail: semantics of individual contract invocation</div></section><section><h1>Shared Knowledge: the Court Registry</h1><p> </p><div align="left">Winning Strategy for good guys <em>iff</em> predicate decidable</div><p> </p><div align="left">BUT to find it, must only quantify over <em>Shared Knowledge</em></div><p> </p><div align="left">Shared Knowledge, precursor to Common Knowledge</div><p> </p><div align="left">Court Registry: Oracle for public data availability</div></section><section><h1>The Take Home Points</h1><p> </p><div align="left">Solve Scalability, Interoperability, Safety issues for dApps</div><p> </p><div align="left">Consensus as Court, Lawsuit as Interactive Proof</div><p> </p><div align="left">Game Theory, Game Semantics, Temporal Logic, Epistemic Logic</div><p> </p><div align="left">Higher-Level: dApp invariants, not contract virtual machines</div></section><section><h1>Thanks</h1><p> </p><div align="left">Our startup: <em>Legicash</em> <a href="https://legi.cash/"><tt>https://legi.cash/</tt></a></div><p> </p><div align="left">WE ARE HIRING! Coq clubbers wanted</div><p> </p><div align="left">WE ARE SEEKING COLLABORATORS! Research grant proposals</div><p> </p><div align="left">SHOW ME THE CODE! <a href="https://j.mp/LegicashCodeReleasePreview"><tt>https://j.mp/LegicashCodeReleasePreview</tt></a></div></section></div></div>
<script src="resources/reveal/lib/js/head.min.js"></script>
<script src="resources/reveal/js/reveal.min.js"></script>
<script>
//<![CDATA[
Reveal.initialize({
dependencies: [
{src: "resources/reveal/plugin/highlight/highlight.js",
async: true, callback: () => hljs.initHighlightingOnLoad()}],
controls: false})
//]]>
</script></body></html>