Formal Methods and Verification of Blockchain Consensus and Smart Contracts

PhD Thesis and Conferences

• Stefano Lande - Formal Methods for Secure Bitcoin Smart Contracts - Universita degli Studi di Cagliari
• Workshop on Formal Methods for Blockchains
  • 2020 - Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol
  • 2019

Organisations

• SECBIT Labs
  • Token Libraries with Proofs
  • Formal Verification for Decentralized Exchange
  • Security Audit for the First zkRollup DEX Protocol

Bibliometric Analysis and Literature Survey

Click Here to view.

Model Formalisms, Specification and Verification

Model Formalisms

Contract-Level Models - (High-level or Abstract-level)

• Process Algebra
  • λ-Calculus
  • Communicating Sequential Processes (CSP) variant of 𝜋-calculus
  • 𝜌-calculus
• State-Transition
  • Behavior-Interaction Priority (BIP)
    • FSolidM
  • PetriNets
    • TINA: A tool for the analysis and verification of timed Petri Nets.
    • GreatSPN: A tool for the analysis and verification of Stochastic Petri Nets.
    • UPPAAL: A tool for modeling, simulation, and verification of real-time systems.
  • Business Process Model and Notation
    • Caterpillar
    • Lorikeet
• Set-Based Methods
  • Event-B
  • TLA+

Program-Level Models - (Source code or compiled bytecode-level)

• AST-Level
• Control Flow Graph
  • Ethainter
  • Securify
  • Vandal
  • Oyente
  • Mythril
  • Manticore
  • Annotary
  • SmartScopy
• Program Logic

Specification Logic

• Temporal Logic
  • Linear Temporal Logic
  • Computation Tree Logic
• Dynamic Logic
• Deontic and Defeasible Logics
• Defeasible logic
• Hoare-Style Properties
• Program Path-Level Patterns

Verification Technique and Tools

Model Checking	Theorem Proving	Program Verification	Symbolic & Concolic Execution	Runtime Verification & Testing
NuSMV, nuXmv SPIN CPN BIP-SMC PRISM UPPAAL MCK Maude FDR Ambient Calculus LDLf	Coq Isabelle/HOL Agda	Datalog & Soufflé Boogie Verifier & Corral LLVM & SMACK SeaHorn F* KeY Why3 K framework Custom static analyses	Oyente Maian Mythril teEther Manticore Securify SmartCheck	ContractLarva EVM* ReGuard SODA Solythesis ECFChecker

Languages

Bitcoin	Ethereum	Hyperledger	Cardano	Solana	Libra/Calibra	Tezos	RChain	Aeternity	Stratis	Aergo
BitML	Solidity Vyper Yul FE Bamboo	Go Obsidian	Marlowe Plutus	Rust C	Move	Michelson	Rholang	Sophia	C#	Lua SCL

Formal Verified Blockchain Ecosystem

• KEVEM - K Semantics of the Ethereum Virtual Machine

Amrita Blockchain and Distributed - Vulnerability Tracker (ABCD - VT)

Click Here to view.

References

• Research Publications and Thesis
• Smart Contracts Weakness Classification Registry (SWC)
• Smart Contracts Testcases for Solidity