🛡️ Dependent Types as 💪⚛️ Strong Proofs for Secure Finance 💯
Dependent types are for specifying program security in a fully general language. Let’s (re)build finance with formal methods and modern tools – much like Rust’s Fearless Concurrency with ownership types and Java’s with Dynamic Classfile with typed bytecode.
The most critical smart contracts are already verified by Runtime Verification (Ethereum staking deposit, Uniswap market making, Gnosis Safe multisig), by Adam Chlipala (process algebra, cryptography, virtual machines), by Nomos (resource-bound session types for auctions and votes), and by ConCert (proof assistant on exchanges and escrows).
Let’s make ALL correct-by-construction – more than randomized property-based testing for gas fee, integer finite domains with model checkers. The essential critical components are MetaMask Portfolio’s bridge and Coinbase Wallet’s Socket bridge.
My past work of compiler research and formal security focused on runtime types and information flows, including dependent type in lambda calculi, refinement type in compiler checks, and session type in machine verification. My favorite language of all time is Twelf! Software Foundation by Penn’s Programming Language Group and DeepSPEC. Frank Pfenning’s Computation and Deduction. UPenn professor Steve Zdancewic’s security-oriented languages.
Stanford postdoctorate, Common Prefix and Resarch DAO founder Dionysis Zindros’s analysis on our protocol and wallets, Hours of Horus: Keyless Cryptocurrency Wallets and Cassiopeia: Practical On-Chain Witness Encryption.
AI on Formal Security
Homotopy Type Theory (Univalent Foundations of Mathematics), Calculus of Constructions
Building the Mathematical Library of the Future and Proof Assistant Makes Jump to Big-League Math.
Galois on memory safety, Vitalik.
Zero Dependencies for Fearless, Composable Extensions
Dependent types
Carnegie Mellon University Carsten Schuermann’s Twelf, user guide, book Programming language theory with Twelf.
University of Pennsylvania professor Benjamin Pierce’s book series Software Foundation.
Carnegie Mellon University professor Frank Pfenning’s book Computation and Deduction.
MIT professor Adam Chlipala’s Formal Reasoning About Programs and Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant.
Formal Security: Zero libraries.
Cornell professor Andrew Myers’s Compositional Security for Reentrant Applications
Formalising Decentralised Exchanges in Coq (Uniswap V1 on Tezos)
One-Time-Password (OTP) wallets
Finance with dependent-type security
Security bugs: arithmetic erros (underflow or overflow), reentrancy, gas limit.
Ethereum Virtual Machine, EVM, Solidity, smart contract.
solc-verify: A Modular Verifier for Solidity Smart Contracts
SoK and top conference papers.
Fellow at Harvard University Library Innovation Lab and Wikipedia editor Molly White’s Web3 is Going Just Great. Immunefi’s Top 10 bugs, Consensys’ known vulnerabilities. Open Zeppelin’s Capture The Flags (CTF), Runtime Verification’s list.
Fearless Finance, like Rust’s Fearless Concurrency by Graydon Hoare.
MIT professor Adam Chlipala’s Certified Programming with Dependent Types. Field medalist Terrence Tao’s work on finite-field polynomials with Lean.
minimal syntax and. Type check, deploy, monitor.
Hacker-Proof Code Confirmed and The Deep Link Equating Math Proofs and Computer Programs
Halborn on Top 50 hacks and formal verification. Halborn conducts both manual analysis and automated testing to secure smart contract applications. This includes key features like Code Review, static & dynamic analysis, auto tool deployment, and financial testing… For Solidity, formal verification is done with the use of Satisfiability Modulo Theories (SMT) and Horn solving. Using the proof-based approach that involves writing theorems manually by a human. This method is more precise but requires the assistance of a proof assistant (such as Coq or Isabelle).
a16z. Halmos: Symbolic testing with Halmos: Leveraging existing tests for formal verification.
Cornell professor Andrew Myers’s Compositional Security for Reentrant Applications.
Microsoft Research, Celestial: A Smart Contracts Verification Framework and Formal verification of smart contracts.
Meta Research, Sui, Aptos. Fast and Reliable Formal Verification of Smart Contracts with the Move Prover.
Beihang University: A comprehensive survey on smart contract construction and execution: paradigms, tools, and systems.
One-Time-Password wallets (1Wallet), market-making swaps (Uniswap), overcollaterized lending (Compound), autonomous stablecoins (Liquity), light-client bridges (Layer Zero), and multi-signature safes (Gnosis).
In proof-assistants Coq and Lean, or model-checkers.
Other Ecosystems: Languages & Formalism
Tezos’ Michaelson and Formalising Decentralised Exchanges in Coq (Uniswap V1 on Tezos) along with… Helmholtz with refinement types.
Zillica’s Scilla (Smart Contract as Automata)
SECBIT Labs’s TokenLibs (Ethereum token contracts)
Applied Type System (ATS)
UIUC professor and Runtime Verification founder Grigore Rosu’s vision on Proof Chain and Universal Truth.
Sui’s Move. Circuits of zero-knowledge proofs.
Aarhus University professor Bas Spitters’s ConCert (A framework for smart contract verification in Coq).
Purdue University professor Xiangyu Zhang’s Demystifying Exploitable Bugs in Smart Contracts.
Certora report on Open Zeppelin token contracts.
Ethereum Foundation & Grants
Ethereum Foundation has continued to give grants to promising research work and academic labs. The following are for Academic GRants Round 2023.
Ethereum Foundation, University of California Santa Barbara, Veridise. Financial Model-Driven Attack Synthesis for DeFi: “To develop a highly effective attack synthesis framework for DeFi protocols that goes beyond the capabilities of existing tools like Foundry and Slither. The project aims to address the limitations of these tools, which struggle with complex interactions and large search spaces in non-trivial DeFi protocols. Rather than constructing the attack from scratch, the new approach will respect the high-level semantics of DeFi protocols and be guided by the financial models underpinning them.”
Ethereum Foundation and University of Madrid. FORVES 2.0: FORmally VErified EVM optimizationS – leveraging FORVES to inter-block optimizations: “To develop FORVES 2.0, a fully automated context-sensitive verification tool in Coq, designed to check the semantic equivalence of two EVM sequences under a given initial context. This project's objective is to facilitate the verification of cross-block optimizations in Ethereum's Virtual Machine.”
Ethereum Foundation and ConsenSys’s Trustworthy Smart Contracts Team, David Pearce. Real-World Demonstrations of the DafnyEVM: “To continue the development of DafnyEVM, an executable and formal EVM semantics developed by ConsenSys' Trustworthy Smart Contracts (TSC) Team, and further leverage its deductive verification capabilities for EVM bytecode. DafnyEVM provides an easily understandable representation of EVM semantics that is verified using the Dafny verifier, enabling formal verification of smart contract properties at the bytecode level. This project seeks to enhance DafnyEVM's robustness in reasoning about bytecode, as demonstrated through validation against numerous Ethereum Common Tests.”
In 2020, Anoma founder Awa Sun Yin’s Juvix on the design smart contract languages. See also: Earlier work by Ethereum Foundation and BedRock Systems research engineer Yoichi Hirai (平井洋一), Bamboo makes state transition explicit and avoids reentrance problems, and Defining the Ethereum Virtual Machine for Interactive Theorem Provers.
Zero-Knowledge Proofs & Cryptography
In blockchains, privacy and fairness are closely related to security. Harmony’s ZK DAO launched ZKU lectures and Blue Forest with UCLA professor Hakwan Lau in 2022.
0xparc is making big progress with ZK-Hunt and Autonomous Worlds Hackathon – along with others on Dark Forest, ETHdos, Autonomous Worlds Arcade, Curio Game, Moving Castles, Topology, Clockless, Zordle, WordLines, zkDocs. More coming from ZK Security David Wong on ZPrize!
Zupass, incubated at Zuzalu earlier this year, is an excellent example of this in practice. This is an application, which has already been used by hundreds of people at Zuzalu and more recently by thousands of people for ticketing at Devconnect, that allows you to hold tickets, memberships, (non-transferable) digital collectibles, and other attestations, and prove things about them all without compromising your privacy.
For example, you can prove that you are a unique registered resident of Zuzalu, or a Devconnect ticket holder, without revealing anything else about who you are. These proofs can be shown in-person, via a QR code, or digitally, to log in to applications like Zupoll, an anonymized voting system available only to Zuzalu residents.
Let’s explore more from the top research conferences, including Financial Cryptography and Data Security (FC), Stanford’s The Science of Blockchain Conference (SBC); and, those on languages and compilers including PLDI, POPL (CCP, CoqPL, Dafny), ICFP, CC, SIGPlan; finally, those on systems and security, including S&P, OSDI, USENIX.