-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
41 lines (41 loc) · 20.4 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
<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 style="background-repeat: no-repeat; background-size: 15%; background-origin: padding-box; background-position: bottom 1% right 1%; background-image: url('resources/pic/alacris_small_logo.png'); "><div class="reveal"><div class="slides"><section><table><tr><td width="15%"></td><td width="33%"><img src="resources/pic/alacris_logo.png" style="border: 0; vertical-align: top; background-color: transparent" /></td><td width="15%"></td><td><div fgcolor="#ff0000"><b> 𝕃 anguage <br />
𝔸 bstraction for <br />
⟦𝕍⟧ erifiable <br />
𝔹 lockchain <br />
𝔻 ecentralized <br />
𝔸 pplications</b></div></td></tr></table> <div align="left"><small> </small></div><div align="center" style="font-size: 1.2em; font-weight: bold;">Why Writing Blockchain Applications is Hard, and <br />
How Functional Programming Can Help</div> <div align="center">François-René Rideau, <em>Alacris</em> <br />
<code class="email">fare@alacris.io</code></div> <!--Alacris Tech Talk 2019-04-11--><!--IOHK Summit, 2019-04-18--><div align="center">LambdaConf 2019 Unconference, 2019-06-07</div><a href="https://alacrisio.github.io/lavbda/"><tt>https://alacrisio.github.io/lavbda/</tt></a></section><section><section><h1>Introduction: Challenges for Secure DApps</h1></section><section><p align="right" valign="top"><font size="4"><b>Introduction: Challenges for Secure DApps</b></font></p><h1>Why No DApps? a Vicious Circle</h1> <table class="noborder" id="noborder"><tr><td style="text-align: center; border: none;"></td><td style="text-align: center; border: none;">No apps</td><td style="text-align: center; border: none;"></td></tr><tr><td style="text-align: right; border: none;">⬈</td><td style="text-align: center; border: none;"></td><td style="text-align: left; border: none;">⬊</td></tr><tr><td style="text-align: center; border: none;">No tech</td><td style="text-align: center; border: none;"></td><td style="text-align: center; border: none;">No users</td></tr><tr><td style="text-align: right; border: none;">⬉</td><td style="text-align: center; border: none;"></td><td style="text-align: left; border: none;">⬋</td></tr><tr><td style="text-align: center; border: none;"></td><td style="text-align: center; border: none;">No money</td><td style="text-align: center; border: none;"></td></tr></table> <span class="fragment" data-fragment-index="1"> <br /> <br /> Typical bootstrapping issue!</span></section><section><p align="right" valign="top"><font size="4"><b>Introduction: Challenges for Secure DApps</b></font></p><h1>What Missing Tech?</h1> <p>Scalability</p><p>Interoperability</p><p>Portability</p><p>Usability</p><span class="fragment" data-fragment-index="1"><h6>Security</h6></span><!----></section><section><p align="right" valign="top"><font size="4"><b>Introduction: Challenges for Secure DApps</b></font></p><h1>Why is Blockchain Security so Hard?</h1><div align="left">1. Transactions: high-stake, irreversible.</div><span class="fragment" data-fragment-index="1"><div align="left"> The "bug budget" is <em>zero</em>.</div></span><!--Aerospace or biomedical industries--> <div align="left">2. Code is fragile.</div><span class="fragment" data-fragment-index="2"><div align="left"> Usual languages, tools & methodologies <em>don't even try</em>.</div></span><!--Parity Wallet: 400 lines, one bug, 280 M$ disappeared!--> <div align="left">3. The Internet is hostile.</div><span class="fragment" data-fragment-index="3"><div align="left"> Each dollar controlled by a DApp is <em>a bounty to the bad guys</em>.</div></span></section><section><p align="right" valign="top"><font size="4"><b>Introduction: Challenges for Secure DApps</b></font></p><h1>The Solution: Logic</h1><div align="left"><em>You</em> may eschew math automation—the bad guys won't.</div><span class="fragment" data-fragment-index="1"><div align="left"> Dijkstra's approach: <em>prove all code correct</em> with math.</div></span> <div align="left">You can't retrofit math in existing code.</div><span class="fragment" data-fragment-index="2"><div align="left"> You must build around <em>math from the start</em>.</div></span> <div align="left">Complexity quickly makes math intractable.</div><span class="fragment" data-fragment-index="3"><div align="left"> Adopt <em>Radical Simplicity</em>—in math terms.</div></span></section><section><p align="right" valign="top"><font size="4"><b>Introduction: Challenges for Secure DApps</b></font></p><h1>Alacris: Our Take Home Points</h1> <div align="left">1. Building secure DApps is extremely hard,</div><div align="left"> a Domain Specific Language (DSL) makes it tractable.</div> <div align="left">2. Automatic Cascading Verification of correctness,</div><div align="left"> from DSL down to bit-bashing, composing full abstractions.</div> <div align="left">3. Blockchain-Agnostic Model: Consensus as Court</div><div align="left"> Scal-, Interoper-, Port-, Us- ability—through <em>Logic</em>.</div></section></section><section><section><h1>A Domain Specific Language (DSL) for DApps</h1></section><section><p align="right" valign="top"><font size="4"><b>A Domain Specific Language (DSL) for DApps</b></font></p><h1>Why not just a Library?</h1><div align="left">A Library: can <em>do</em> everything, but not <em>prevent</em> much.</div><span class="fragment" data-fragment-index="1"><div align="left"> Manually respect its unenforced global invariants… or else.</div>
<div align="left"> Leaks complexity, makes verification harder.</div></span> <div align="left">A DSL: can express both positive and negative.</div><span class="fragment" data-fragment-index="2"><div align="left"> Global invariants automatically enforced.</div>
<div align="left"> Seals complexity, makes verification easier.</div></span></section><section><p align="right" valign="top"><font size="4"><b>A Domain Specific Language (DSL) for DApps</b></font></p><h1>Why not just a new General Purpose Language?</h1><div align="left">General Purpose Language: Library-generator.</div><span class="fragment" data-fragment-index="1"><div align="left"> Leaks complexity exponentially until untractable.</div>
<div align="left"> Mushes all abstraction levels into one.</div></span> <div align="left">Proper DSLs: keep small problem spaces.</div><span class="fragment" data-fragment-index="2"><div align="left"> Seal complexity at each level of abstraction.</div>
<div align="left"> General-Purpose Logic Meta-Language: factor in multiple layers.</div></span></section><section><p align="right" valign="top"><font size="4"><b>A Domain Specific Language (DSL) for DApps</b></font></p><h1>Why not just a Contract Language?</h1><div align="left">A DApp is much more than a smart contract:</div><span class="fragment" data-fragment-index="1"><div align="left"> Also code running on clients, servers, etc.</div>
<div align="left"> Any bug and poof money gone. Any discrepancy is a bug.</div></span> <div align="left">DSL: a single spec for the entire DApp.</div><span class="fragment" data-fragment-index="2"><div align="left"> End-Point Projection: extract code for all components.</div>
<div align="left"> Do it correctly—consistently across components.</div></span></section><section><p align="right" valign="top"><font size="4"><b>A Domain Specific Language (DSL) for DApps</b></font></p><h1>Why not a least share VM with Contracts?</h1><div align="left">Contract VM is for deterministic consensual computations.</div><span class="fragment" data-fragment-index="1"><div align="left"> Computations cost > 10⁶ more than on cloud.</div> <!--over a million times-->
<div align="left"> Optimize programs for cost.</div></span> <div align="left">DApp VM is for asynchronous multiparty computations.</div><span class="fragment" data-fragment-index="2"><div align="left"> Most computations on private cloud.</div>
<div align="left"> Optimize programs for auditability.</div></span><!--XXXX Cut...
Consensus: everything computed is public
All: Keys are private information
Poker: hands are private information--></section><section><p align="right" valign="top"><font size="4"><b>A Domain Specific Language (DSL) for DApps</b></font></p><h1>What features in the DApp DSL then?</h1><div align="left">Functional Programming.</div><div align="left">Asynchronous and Synchronous Communication.</div><div align="left">Cryptographic Primitives.</div><div align="left">Modal Logic: Epistemic + Temporal.</div><div align="left">Linear Logic: Resource Management.</div><div align="left">Game Theory: Economic Equilibrium.</div><div align="left">Refinement Logic: Work at many abstraction levels.</div><div align="left">Finitary Logic: zk-proofs (optional).</div> <span class="fragment" data-fragment-index="2"><div align="center">An extensible framework!</div></span></section></section><section><section><h1>Automatic Cascading Verification</h1></section><section><p align="right" valign="top"><font size="4"><b>Automatic Cascading Verification</b></font></p><h1>Semantic Tower</h1><div align="left">Verify entire semantic tower, from user spec to bit bashing.</div><span class="fragment" data-fragment-index="1"><div align="left"> Full Abstraction: no semantic leak.</div></span> <div align="left">Address each issue at proper level of abstraction.</div><span class="fragment" data-fragment-index="2"><div align="left"> Zoom in and out—at compile-time <em>and</em> runtime.</div></span> <span class="fragment" data-fragment-index="3"><div align="left">Regular developers <em>automatically</em> get proofs with Z3.</div>
<div align="left">System extenders <em>manually</em> prove correctness with Coq.</div></span></section><section><p align="right" valign="top"><font size="4"><b>Automatic Cascading Verification</b></font></p><h1>Correctness Properties to Automatically Verify</h1><span class="fragment" data-fragment-index="1"><div align="left">User-defined protocol invariants.</div></span> <span class="fragment" data-fragment-index="2"><div align="left">Linear Resources, Access Control, Time Bounds.</div></span> <span class="fragment" data-fragment-index="3"><div align="left">Game-Theoretic Liveness: progress if all actors honest.</div>
<div align="left">Game-Theoretic Safety: no loss to bad actors.</div></span></section><section><p align="right" valign="top"><font size="4"><b>Automatic Cascading Verification</b></font></p><h1>Verification techniques</h1><div align="left"><em>Type Theory</em>: grow system with Coq.</div><div align="left"><em>Theorem Proving</em>: user automation with Z3.</div><div align="left"><em>Model Checking</em>: domain-specific models.</div><div align="left"><em>Strand Spaces</em>: model attacker capabilities.</div><div align="left"><em>Dynamical System Simulation</em>: test attack scenarios.</div><div align="left"><em>Composable Implementation Layers</em>: keep complexity in check.</div></section><section><p align="right" valign="top"><font size="4"><b>Automatic Cascading Verification</b></font></p><h1>Composable implementation layers</h1><div align="left">Category Theory: Computations as categories.</div><div align="left"> States as nodes ("objects"), transitions as arrows ("morphisms").</div> <div align="left">Implementations as partial functors (profunctors).</div><div align="left"> Game-Theoretic Safety & Liveness as composable properties.</div><div align="left"> Code Instrumentations as natural transformations.</div> <span class="fragment" data-fragment-index="1"><div align="left">Good sign: functoriality implies full abstraction!</div></span></section><section><p align="right" valign="top"><font size="4"><b>Automatic Cascading Verification</b></font></p><h1>Less Formal Methods</h1><div align="left">Lightweight Formal methods: Quickly check simple properties.</div><span class="fragment" data-fragment-index="1"><div align="left"> Starve attackers of low-hanging fruits.</div></span> <div align="left">Can't do without axioms. Can make them explicit, audit them.</div><span class="fragment" data-fragment-index="2"><div align="left"> Automatically track axioms from every abstraction level.</div></span> <div align="left">Human Processes matter.</div><span class="fragment" data-fragment-index="3"><div align="left"> Design. Review. Discipline. Check lists. Red team.</div></span></section></section><section><section><h1>Blockchain-Agnostic Model: Consensus as Court</h1></section><section><p align="right" valign="top"><font size="4"><b>Blockchain-Agnostic Model: Consensus as Court</b></font></p><h1>Consensus as Court</h1><div align="left">Analogy: common abstraction, different parameters.</div><div align="left"> Conflict avoidance & resolution. Machines <em>vs</em> humans.</div> <div align="left">Avoidance: Good guy pays, all the time. Reliably Slow.</div><div align="left">Resolution: Bad guy pays, in unhappy case only. Faster/Slower.</div> <div align="left">Machines: verification games with logic—fast cheap rigid.</div><div align="left">Humans: legal arguments with rhetoric—slow expensive flexible.</div></section><section><p align="right" valign="top"><font size="4"><b>Blockchain-Agnostic Model: Consensus as Court</b></font></p><h1>Logic for Smart Contracts</h1><div align="left">Smart contract clause is <em>arbitrary logical formula</em>.</div><div align="left"> NB: Requires logic model of the blockchain or side-chain.</div> <div align="left"><em>Game Semantics</em>: translate formulas to verification games.</div><div align="left"><em>Fundamental Theorem</em>: Good guy has winning strategy.</div> <div align="left">Bad guy loses, then pays damages and court fees...</div><div align="left"> out of <em>bond</em>—with any claim, deposit collateral.</div></section><section><p align="right" valign="top"><font size="4"><b>Blockchain-Agnostic Model: Consensus as Court</b></font></p><h1>Mutual Knowledge</h1><div align="left">Winning Strategy: "there exists" not enough—"I know" needed.</div><div align="left"> All evidence must be <em>Mutual Knowledge</em> (MK).</div> <div align="left">Consensus (<em>Common Knowledge</em>, CK). State channels. Plasma.</div><div align="left"> Side-chains? Need a data availability engine, a.k.a. MKB.</div> <div align="left">Scale with general purpose MK validator network.</div><div align="left"> MK easier to achieve <em>and shard</em> than consensus.</div></section><section><p align="right" valign="top"><font size="4"><b>Blockchain-Agnostic Model: Consensus as Court</b></font></p><h1>Extension: Zero-Knowledge Proofs</h1><div align="left"><em>Private</em> interactive validation.</div><div align="left"> Anyone can see who's right, no one knows about what.</div> <div align="left"><em>Non-interactive</em> a priori validation.</div><div align="left"> Trade-off: good guy pays all the time, a lot.</div> <div align="left"><em>Interoperability</em>: commitment with different hash functions.</div> <div align="left"><em>Gambling</em>: Homomorphic encryption of card game hands.</div></section><section><p align="right" valign="top"><font size="4"><b>Blockchain-Agnostic Model: Consensus as Court</b></font></p><h1>One DApp Many Backends</h1><table class="noborder" id="noborder"><tr><td style="text-align: right; border: none;">This blockchain</td><td style="text-align: center; border: none;"><em>vs</em></td><td style="text-align: left; border: none;">That blockchain</td></tr><tr><td style="text-align: right; border: none;">Interactive verification</td><td style="text-align: center; border: none;"><em>vs</em></td><td style="text-align: left; border: none;">Non-interactive enforcement</td></tr><tr><td style="text-align: right; border: none;">Public computation</td><td style="text-align: center; border: none;"><em>vs</em></td><td style="text-align: left; border: none;">Private computation</td></tr><tr><td style="text-align: right; border: none;">Slow and trustless</td><td style="text-align: center; border: none;"><em>vs</em></td><td style="text-align: left; border: none;">Fast semi-trusted middleman</td></tr></table> <div align="left"> Different sets of users have different needs from backends.</div><div align="left"> Different blockchains offer different capabilities to backends.</div></section><section><p align="right" valign="top"><font size="4"><b>Blockchain-Agnostic Model: Consensus as Court</b></font></p><h1>Blockchain-Agnostic Model</h1><p>Scalability</p><p>Interoperability</p><p>Portability</p><p>Usability</p><h6>Security</h6> <span class="fragment" data-fragment-index="1"><div align="left">Mathematical essence of the Blockchain:</div>
<b>Common Knowledge about Monotonic Verifiable Data Structures</b></span></section></section><section><section><h1>Conclusion</h1></section><section><p align="right" valign="top"><font size="4"><b>Conclusion</b></font></p><h1>Alacris: Our Take Home Points (redux)</h1> <div align="left">1. Building secure DApps is extremely hard,</div><div align="left"> a Domain Specific Language (DSL) makes it tractable.</div> <div align="left">2. Automatic Cascading Verification of correctness,</div><div align="left"> from DSL down to bit-bashing, composing full abstractions.</div> <div align="left">3. Blockchain-Agnostic Model: Consensus as Court</div><div align="left"> Scal-, Interoper-, Port-, Us- ability—through <em>Logic</em>.</div></section><section><p align="right" valign="top"><font size="4"><b>Conclusion</b></font></p><h1>The Meta-Story</h1><div align="left">Go to the mathematical essence of things.</div><div align="left"> Itself the essence of category theory.</div> <div align="left">Strip all incidental complexity.</div><div align="left"> Identify what the domain is and isn't.</div> <div align="left">Embrace multiple levels of abstraction.</div><div align="left"> Reconcile Semantics and Reflection.</div><!--In the words of Dick Gabriel:
The programming language paradigm vs the systems paradigm.--></section><section><p align="right" valign="top"><font size="4"><b>Conclusion</b></font></p><h1>Contact</h1> <div align="left">I NEED MORE INFO! Our website <a href="https://alacris.io/"><tt>https://alacris.io/</tt></a></div> <div align="left">I WANT TO FOLLOW ALONG! Medium <a href="https://medium.com/alacris"><tt>https://medium.com/alacris</tt></a></div> <div align="left">I WANT TO HELP! Telegram <a href="https://t.me/alacrisio"><tt>https://t.me/alacrisio</tt></a></div> <div align="left">SHOW ME THE CODE! <a href="https://github.com/AlacrisIO"><tt>https://github.com/AlacrisIO</tt></a></div></section></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>