Sunday March 07, 2021
Bitcoin (BTC) $50,018.00   Ether (ETH) $1,654.10
  • Events
  • News
    • Blockchain Technology
    • Capital Raising
    • Crypto Exchanges
    • Crypto Payments
    • Gaming & Betting
    • Networks & Protocols
    • Security
    • Vendor Technology
    • Wallets
NEWSLETTER SIGNUP
EXCHANGE 300+ COINS
CryptoNinjas
  • Crypto & Blockchain Links
  • Real-Time Market Data
  • Bitcoin ATM Map
  • Token Offerings/Listings
No Result
View All Result
CryptoNinjas
No Result
View All Result
Home Ethereum

Research project produces first complete formal semantics of Ethereum Virtual Machine

Published by CryptoNinjas.net
08/02/2017

IOHK, leading blockchain research, and development company, has announced that its research project with the University of Illinois at Urbana-Champaign (UIUC) has modeled the world’s first complete fully-executable formal semantics of the Ethereum Virtual Machine (EVM). The research produced an innovative framework, called KEVM, for formal execution, analysis, and verification of EVM smart contracts.

The Ethereum Foundation and IC3, an initiative of faculty members at Cornell University, Cornell Tech, UC Berkeley, the University of Illinois at Urbana-Champaign, and the Technion, selected KEVM as the winner of its immersive, week-long blockchain development event called the “IC3-Ethereum Crypto Boot Camp.” Led by Professor Grigore Rosu and his Ph.D. student Everett Hildenbrandt, the IOHK-funded KEVM research project competed against nine other world-leading teams to emerge the winner.

Prof. Grigore Rosu of the UIUC’s Siebel Center for Computer Science and CEO of Runtime Verification said:

“The pressing need to address repeated security vulnerabilities and high-profile failures in Ethereum smart contracts hasn’t been adequately addressed by existing formal verification and program analysis tools. No fully-formal, rigorous, comprehensive, and executable semantics of EVM existed until now, leaving a lack of rigor on which to base such tools.”

“I am delighted to announce KEVM, the first complete and fully executable formal semantics of the Ethereum Virtual Machine. KEVM, which allows us to formally verify properties of EVM-based smart contracts in a correct-by-construction and cost-effective manner, is significant because Ethereum users need the guarantees of formal verification to safeguard against financial losses due to software bugs. This work serves as a foundation for the development of new smart contract analysis tools; more importantly, it gives us invaluable insight on how to design better programming languages for smart contracts.”

KEVM not only passes the official 40,683-test stress test suite for EVM implementations but also reveals ambiguities and potential sources of error in the existing on-paper formalization of EVM semantics.

Prof. Rosu continued:

“KEVM has demonstrated that our unique approach based on K formal executable semantics is feasible and not computationally restrictive. We hope our work serves as a strong basis for the development of a wide range of useful, formally-derived tools for Ethereum, like model checkers, certified compilers, and program equivalence checkers.”

Formal verification is an integral aspect of IOHK’s approach to developing cryptocurrencies, as the company recognizes that only mathematical proofs can guarantee correctness.

IOHK selected to invest in the research and development of a formal semantics of the EVM based on the K framework due to K’s language-independent nature, wide potential application, and its success in academia, where K has been used to formalize several real-world languages, like JavaScript, Java, C, Python, and PHP. Furthermore, several language-independent analysis tools already exist for K. Notably, the K framework supplies a semantic debugger, symbolic execution engine, and verification infrastructure for each developed language. Beyond academia, this work has been successfully commercialized at Runtime Verification, Inc. where tools like RV-Match, an automatic C analyzer which includes checks for undefined behavior, are developed as applications of the K semantics of C.

Development of KEVM continues to be open-source, in line with IOHK’s mission to improve and mature the blockchain industry as a whole. IOHK recognizes the importance of open development to the security of the Ethereum community at large and is committed to ensuring this work is available to everyone for use and audit.

IOHK CEO Charles Hoskinson said:

“This research has given us a great degree of insight into what one should do to redesign the EVM to make it more secure, faster, and more efficient. It will now be easier to build tooling for the EVM, such as verified compilers. This white paper is the result of our first wave of research into this area. Based on this research, IOHK will begin building prototypes and our hope is to have an EVM 2.0 ready next year, as part of Cardano, a product we are currently building.”

Notable attendees of the IC3-Ethereum Crypto Boot Camp where the KEVM research was awarded first prize include Ethereum Co-Founder and Chief Scientist Vitalik Buterin, Ethereum Foundation Executive Director Ming Chan, and IC3 Executive Director Jim Ballingall.

10
SHARES
FacebookTwitterLinkedinRedditE-MailTelegram

Related News

Glow programming language brings smart contract simplicity to Cardano
Networks & Protocols

Glow programming language brings smart contract simplicity to Cardano

02/26/2021
IOHK to start roll-out of Cardano blockchain Shelley-era functionality
Networks & Protocols

IOHK expands Cardano development fund with launch of new $500K round

01/08/2021
IOHK integrates Cardano with Wolfram Alpha, in preparation for smart contract roll-out
Networks & Protocols

IOHK integrates Cardano with Wolfram Alpha, in preparation for smart contract roll-out

12/17/2020
Public chains Cardano and Nervos to improve on Bitcoin’s UTXO model
Networks & Protocols

Public chains Cardano and Nervos to improve on Bitcoin’s UTXO model

12/15/2020
IOHK launches unique ‘smart-contract-free’ solution for tokens on Cardano
Networks & Protocols

IOHK launches unique ‘smart-contract-free’ solution for tokens on Cardano

12/14/2020
Load More
Leave Comment

Where to Exchange

Bit2MeLeading Spanish Bitcoin ExchangeVisit
BL3P
European Bitcoin ExchangeVisit
ChangellyExchange & Buy 150+ CryptocurrenciesVisit
itBitAmerica's First Regulated Bitcoin ExchangeVisit
  • Trending
  • Latest
Enjin launching two scaling solutions to remove gas and support NFTs from any blockchain

Enjin launching two scaling solutions to remove gas and support NFTs from any blockchain

03/04/2021
Creators of crypto wallet Exodus files with SEC to allow purchase of its stock with bitcoin

Creators of crypto wallet Exodus file with SEC for $75M public offering

03/03/2021
SIMBA Chain expands to Avalanche blockchain enabling low-code smart contract deployment

SIMBA Chain expands to Avalanche blockchain enabling low-code smart contract deployment

03/02/2021
Canadian bitcoin exchange CoinSmart raises $3.5M to expand into Europe

Canadian bitcoin exchange CoinSmart raises $3.5M to expand into Europe

03/01/2021
DeFi yield optimization protocol ETHA Lend closes $1.6M funding round

DeFi yield optimization protocol ETHA Lend closes $1.6M funding round

03/04/2021
Bitcoin DeFi platform Sovryn reveals $1.25M bug bounty; raises $10M in token presale

Bitcoin DeFi platform Sovryn reveals $1.25M bug bounty; raises $10M in token presale

03/05/2021
P2P crypto escrow platform Escaroo adds staking function from Moonstake

P2P crypto escrow platform Escaroo adds staking function from Moonstake

03/05/2021
SecondState launches Ethereum compatible ParaTime on the Oasis blockchain

SecondState launches Ethereum compatible ParaTime on the Oasis blockchain

03/05/2021
NFT platform Curio closes seed funding of $1.2M to fuel expansion

NFT platform Curio closes seed funding of $1.2M to fuel expansion

03/05/2021
IOTA token added as collateral asset on Bitfinex Borrow

IOTA token added as collateral asset on Bitfinex Borrow

03/05/2021
  • Home
  • Directory
  • Data
  • About
  • Contact
SUBSCRIBE

© 2016 - 2021 CryptoNinjas Disclosures | Privacy Policy

  • Home
  • Crypto Links
  • Market Data
  • Blockchain Tech
  • Exchanges
  • Capital Raising
  • Vendor Technology
  • Token Offerings/Listings
  • Payments
  • Wallets
  • Bitcoin ATM Map
  • Conferences & Events
  • About
  • Contact

© 2016 - 2021 CryptoNinjas Disclosures | Privacy Policy


Go to mobile version