English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

This paper reports on the development of a formal symbolic process virtualmachine (FSPVM) denoted as FSPVM-E for verifying the reliability and securityof Ethereum-based services at the source code level of smart contracts, and aCoq proof assistant is employed for both programming the system and for provingits correctness. The current version of FSPVM-E adopts execution-verificationisomorphism, which is an application extension of Curry-Howard isomorphism, asits fundamental theoretical framework to combine symbolic execution andhigher-order logic theorem proving. The four primary components of FSPVM-Einclude a general, extensible, and reusable formal memory framework, anextensible and universal formal intermediate programming language denoted asLolisa, which is a large subset of the Solidity programming language usinggeneralized algebraic datatypes, the corresponding formally verifiedinterpreter of Lolisa, denoted as FEther, and assistant tools and libraries.The self-correctness of all components is certified in Coq. Currently, FSPVM-Esupports the ERC20 token standard, and can automatically and symbolicallyexecute Ethereum-based smart contracts, scan their standard vulnerabilities,and verify their reliability and security properties with Hoare-style logic inCoq. To the best of authors' knowledge, the present work represents the firsthybrid formal verification system implemented in Coq for Ethereum smartcontracts that is applied at the Solidity source code level.

A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts