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