Elrond gets new secure dev tooling and a formal semantics

Elrond and Runtime Verification started as friends, professional admirers of each other’s organizations. The picture attached to this post shows members of both companies together at DevCon IV in Prague, October 2018. Quickly thereafter, Grigore Rosu, Runtime Verification’s founder and CEO, agreed to become an advisor to Elrond.

Runtime Verification has long been impressed by Elrond’s dogged determination to build a world class blockchain, and their commitment to executing their strategic roadmap with minimal distraction.

A little more than two years after Prague, Runtime Verification is proud to partner with Elrond on the development of world class tooling that will enable developers to write secure code to power applications, products, and services for the Elrond ecosystem.

Building tools for developers
At Runtime Verification, we believe that all languages should have a formal semantics. For blockchain languages, that is non-negotiable. That is why we developed KEVM in 2017.

The Elrond virtual machine, called Arwen, is built on WebAssembly. WebAssembly comes with formal semantics, but every specific flavor of WebAssembly requires some extension. We already have a complete executable WebAssembly semantics in K, which we extended to implement Arwen. So now Elrond contracts can run on a fully formalized, auto-generated virtual machine. On top of that we have given the KArwen semantics support for the Arwen contract testing framework, Mandos.

A K semantic comes with many benefits. It allows formal verification to prove that your contracts do what you expect them to. But formal verification is a heavy-duty tool and rarely usable for the average smart contract developer. So we are also adding highly accessible features for you to improve your contract security. As a first, dead simple tool, we measure the code coverage of your Mandos tests.

The coverage is at the WebAssembly level, so it will include functions your compiler added. That gives you higher assurance that you are testing all code paths that are in the actual, deployed contract — the one that hackers and flash loan hawks will go after.

The coverage tool has been used internally to look at coverage of some example contracts, and will be put to more heavier use early next year. A nice benefit of the tool so far has been that it has revealed several functions that the Rust compiler inserts automatically which are not actually reachable from any of the callable contract functions. The Elrond team has been able to use this knowledge to cut down compiled contract size significantly, by around 40%, on average.

So far, we are showing coverage at the function level, and we plan to add full code-level coverage soon.

We have great plans for the new formal semantics of Elrond. We plan to push out dev tooling internally as it becomes ready, and release it to the wider community once the internal alpha is done.

The semantics are open source and available on Github.

About Elrond
Elrond is the internet-scale blockchain, designed from scratch to bring a 1000-fold cumulative improvement in throughput, execution speed and transaction cost. To achieve this, Elrond introduces two key innovations: a novel Adaptive State Sharding mechanism, and a Secure Proof of Stake (PoS) algorithm, enabling linear scalability with a fast, efficient, and secure consensus mechanism. Thus, Elrond can process upwards of 15,000 transactions per second (TPS), with 6-second latency, and negligible cost, attempting to become the backbone of a permissionless, borderless, globally accessible internet economy.

About Runtime Verification
Runtime Verification is a technology startup based in Champaign-Urbana, Illinois. The company uses runtime verification-based techniques to perform security audits on virtual machines and smart contracts on public blockchains. It is dedicated to using its dynamic software analysis approach to improve the safety, reliability, and correctness of software systems in the blockchain field.

Originally published at https://runtimeverification.com on January 5, 2021.




Runtime Verification Inc. is a technology startup providing cutting edge formal verification tools and services for aerospace, automotive, and the blockchain.

Love podcasts or audiobooks? Learn on the go with our new app.

Recommended from Medium

Run ArcGIS On MacBook



How VR Builder promotes collaboration in VR content creation

Ultra fast asynchronous counters in Postgres

Delete a VMware Virtual Machine Snapshot — Ansible module vmware_guest_snapshot

Installing Tensorflow with CUDA, cuDNN and GPU Driver support on Windows 10

Understanding Web1 and Web2 and the Web3 Business model. (Part1).

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Runtime Verification

Runtime Verification

Runtime Verification Inc. is a technology startup providing cutting edge formal verification tools and services for aerospace, automotive, and the blockchain.

More from Medium

On Harold Bloom’s The Western Canon

Origins of Quantum One part 1— How I modified the Cardano Blockchain


Taraxa: Can New Layer-Ones Challenge Solana & Avalanche?

Taraxa: Can New Layer-Ones Challenge Solana & Avalanche?

Evvy Co-Founder Laine Bruzek: We’re an ‘Answers Company’