Interactive theorem prover for FV of smart contracts
#formal_verification
eth-isabelle
Semantic in Lem, translated to Isabelle
Partially supporting Coq Article
paper Defining the Ethereum Virtual Machine for Interactive Theorem Provers, slide
Seed is still working on this GitHub Repo
Mario Alvarez (@Consensys) developing Elle, verified compiler with eth-isabelle
GitHub Repo Master thesis Paper
separation algebra
based on the work from this paper Verification of programs in virtual memory using separation logic by Rafal Kolanski
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL (2018)
Sidney Amani (NSW, Australia) et. al.
CPP18
EVM semantic in F*
TU Wien
paper: A Semantic Framework for the Security Analysis of Ethereum smart contracts (2018)
GitHub Repo
small step semantics of the EVM
Based on Oyente's EtherLite
adding contract calls and call creation
This includes an abstract security definition of smart contracts in section 4.
I think this forms a basis for properties you want to verify and then, additionally, you have functional requirements that are specific to your protocol.
discuss the semantics of CALL and CREATE in section 3.4.
Solidity to F*, F* to EVM bytecode
Formal Verification of Smart Contracts: Short Paper (2016 Nov) by Microsoft Research & Harvard Univ.
Translate Solidity to F*, decompile EVM bytecode to F*
Formal verification with F*'s type system
A subset of Solidity, removing loops, etc.
Why3 for Solidity
a post Formal Verification for Solidity Contracts by Chiris, 2015
Why3, a tool for program verification
Write a spec with the DSL called WhyML
verofy with automated solver like Z3 or interactive prover like Coq
Coq
Formal Process Virtual Machine for Smart Contracts Verification
Hoare logic in Coq
ConCert: A Smart Contract Certification Framework in Coq
Smart Contract Interactions in Coq
SECBIT
website, GitHub Repo
DSL in Coq whose syntax is similar to Solidity
Lolisa & GERM Framework
University of Electronic Science and Technology of China
GERM framwork based on Coq
Lolisa
A subset of Solidity + strong type system
Formal syntax & semantic
Based on GERM Framework
Papers
Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language (2018)
A general formal memory framework in Coq for verifying the properties of programs based on higher-order logic theorem proving with increased automation, consistency, and reusability
A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts
Zheng Yanga, Hang Leia, Weizhong Qiana
Hoare logics for EVM
Hoare Logics for Ethereum Virtual Machine by Yoichi Hirai
A variant of Hoare Logic for EVM
code: ADD
lemma add_triple :
"triple {}
(*precond*) (⟨ h ≤ 1023 ∧ g ≥ Gverylow ⟩ **
stack_height (h + 2) **
stack (h + 1) v ** (* ONE NUMBER *)
stack h w ** (* ANOTHER NUMBER *)
program_counter k **
gas_pred g **
continuing
)
(* code *) {(k, Arith ADD)}
(*postcond*)(stack_height (h + 1) **
stack h (v + w) ** (* SUM *)
program_counter (k + 1) **
gas_pred (g - Gverylow) **
continuing
)"
Detecting Reentrancy
Online Detection of Eectively Callback Free Objects with Applications to Smart Contracts by Universitat Tel-Aviv・VMWare
Introduce a concept of "Effective Callback Free"
Compared to Oyente
Implementing contracts in Idris
Safer smart contracts through type-driven development (2016)
Idris (pure functional language, dependent types)
Translated to EVM bytecode but it's not efficient
Scilla
Smart contract language for Zilliqa
formal verification with Coq
Michelson & Liquidity
Tezos
Michelson
Low leverl pure functional language
Semantic in Coq (WIP?) GitHub
Liquidity
Compiled to Michelson
OCaml
GitHub Repo
Author: OCamlPro
Tezos foundation is not supporting it
Ref
Tezos幻想を解く