MultiversX (formerly Elrond) gets new secure dev tooling and a formal semantics
MultiversX 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 MultiversX (formerly Elrond).
Runtime Verification has long been impressed by MultiversX’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 MultiversX on the development of world class tooling that will enable developers to write secure code to power applications, products, and services for the MultiversX 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 MultiversX 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 MultiversX 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 MultiversX 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 MultiversX. 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 MultiversX
MultiversX 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, MultiversX 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, MultiversX 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.
