What languages I’ll keep a close look at next year (2018)
If “crypto” stands for cryptography… then, is my auto-correct right to call “cryptocurrencies” just “currencies”?
C ryptocurrencies and blockchain made a lot of noise this year, good and bad. Smart contracts are finding new use cases (e.g. CryptoKitties), and some existing use case like multi-sig wallets (e.g. Parity) have been challenged due to their high complexity which introduced, like any piece of complex software, security vulnerabilities.
I’ll be covering some smart-contract languages that got my attention, and why I’m gonna keep a close look at them next year. No doubt I forgot several languages, the list is nonexhaustive and I’m looking forward your comments on Twitter.
This year, Ethereum and its Virtual Machine (EVM) popularized the concept of smart contracts but also highlighted its potential risks. It is now common to hear criticism on EVM or its smart contract language, Solidity, for their complexity due to the several types of security vulnerability issues discovered this year in production deployed smart contracts.
Back in February 2017, when I started working on Porosity, my decompiler and smart contract auditing tool for Ethereum smart-contracts, very few people (among those Martin H. Swende, OYENTE’s team) looked at the potential risks of embedding smart contract software, written in a non formally verifiable language, on an immutable blockchain.
Over the past few months, both Chainand Blockstreammade an interesting announcement for smart-contract developments ecosystem.
This month, Chain announceda Bitcoin Script extension of their smart contract language, Ivy, called to provide Bitcoin Script developers a high-level language to develop smart-contracts. Ivy already supported their Chain Protocol’s Virtual Machine. This extension makes sense since even their internal documentation qualifies their instruction set as an extension of Bitcoin Script instruction sets, it’s a smart move as it will probably also attract more developers to Chain Core next year.
The CVM has some overlaps and similarities with Bitcoin Script, but adds instructions to support additional functionality, including loops, state transitions (through transaction introspection), and program evaluation.
Russel O’ Connor from Blockstream released his whitepaper for Simplicity, a native Merklized Abstract Syntax Trees (MASTs) programming language. Thanks to Dan Robinson from Chain, his recent blogpost is an excellent introduction to it, while announcing a potential extension of Ivy for Simplicity.
Simplicity is designed to be small and efficient and is non-Turing-complete on purpose — mainly to stay away from potential security issues that have been hitting Ethereum smart-contracts until now. This design makes the language itself formally verifiable and even had been praised by functional programming language scientist Philip Wadler himself.
Simplicity is a typed, combinator-based, functional language without loops and recursion, designed to be used for crypto-currencies and blockchain applications. It aims to improve upon existing crypto-currency languages, such as Bitcoin Script and Ethereum’s EVM, while avoiding some of the problems they face. Simplicity comes with formal denotational semantics defined in Coq, a popular, general purpose software proof assistant. Simplicity also includes operational semantics that are defined with an abstract machine that we call the Bit Machine. The Bit Machine is used as a tool for measuring the computational space and time resources needed to evaluate Simplicity programs. Owing to its Turing incompleteness, Simplicity is amenable to static analysis that can be used to derive upper bounds on the computational resources needed, prior to execution. While Turing incomplete, Simplicity can express any finitary function, which we believe is enough to build useful “smart contracts” for blockchain applications.
Several Ethereum smart-contracts have been described as “overcomplicated” as we saw in the Parity issues, and we know with traditional software that large code base applications result in a larger attack surface and a higher rate of potential security vulnerabilities. Designing a simpler language is a better long-term plan way to introduce developers to adopt best practices rather than expecting them to make no mistakes.
Although, the introduction of Web Assembly by eWASM, as an alternative to the EVM, on the Ethereum roadmap has been on my watch list for a while and I know several security researchers are highly expecting its release to hunt for more security bugs. WebAssembly is natively supported by JavaScript engines (Chakra, Spidermonkey, V8) but is extremely complicated and is a potential goldmine for attackers looking for vulnerabilities.
Following its Elevence’s acquisition, Digital Asset Holding announced its financial service (FS) industry focus smart contract language: Digital Asset Modeling Language (DAML) — and its intent to open source it last year. I haven’t been able to find the link, so they are still part of a long list of languages I’m looking forward hearing more about — but given their FS industry focus it makes them very attractive from a security point of view.
Michelsonfor Tezos is another smart contract language designed to “facilitate formal verification”, the Tezos team explains in a blogpost the main benefits of Michelson as the following:
With Michelson you can more easily check over and verify properties of the program that is actually executed. Using a higher-level bytecode also simplifies the process of proving properties about the compiled output. Programs written in Michelson can be reasonably analyzed by SMT solvers and formalized in Coq without the need for more complicated techniques like separation logic. Similarly, the restrictions imposed by the forced indentation and capitalization ensure that the source cannot be obfuscated with indentation and alignment tricks.
Although initially criticized to be hard to read, a higher level and fully typed functional language that compiles to Michelson, is now available: Liquidity. Michelson/Liquidity are designed with strict security requirements too. I’m sure we will hear more about them too next year.
Oh! I almost forgot, between Corda R3, Microsoft Coco Framework, MobileCoin& Tesseract there is an increasing number of projects marrying the Distributed Ledger Technology (DLT) world to Intel SGX. I’m curious to see if we will see new types of attacksagainst SGX next year.
EDIT (31 Dec, 2017): Cardano
As I mentioned above I was sure I would forget some, or even not be aware of all of them as this space is moving a lot. IOHK’s Cardano seems to be very promising too, mainly because of their recent partnership with the Runtime Verification team which is adding some very significant milestones to their 2018 roadmap.
Runtime Verification team was initially behind a project called KEVM, the formal semantics of Ethereum VM they built using the K framework (whitepaper).
Apparently, their research on EVM & K framework got the attention of IOHK since a few months later in October, the Runtime Verification (cool name btw) team __ announced __ that they have been awarded a research contract from IOHK to focus on a next-generation VM (IELE) and a universal language framework (K framework).
They released two months later the first version of IELE, their Register-Based Virtual Machine, on Dec 15, 2017.
This VM is the results of research Runtime Verification made on the EVM while working on KEVM, their semantics of EVM in K. As I mentioned EVM limitations have been highlighted numerous times, the emergence of new architectures for Blockchain Virtual Machines was only a matter of time and we will for sure see a lot of work in that area.
“IELE is a variant of LLVM specialized to execute smart contracts on the blockchain. Unlike the EVM, which is a stack-based machine, IELE is a register-based machine, like LLVM.”
Along IELE, their research on K framework aims at providing smart-contract languages K semantics including IELE itself, Plutus (a strictly typed pure functional language for Cardano’s smart-contracts) and even Solidity (which is currently used to develop smart-contracts on Ethereum).
The Runtime Verification roadmap mentions very interesting milestones:
- Deploy IELE on the Cardano blockchain.
- Compilers/Translators from Solidity and Plutus to IELE.
I’m looking forward following RV team & IOHK team progress. IOHK’s team is pretty interesting too they also recruited Dr. Philip Wadler himself, I’d expect that to positively influence the development of K framework. Back in October, Charles Hoskinson also explained their roadmap in a very good video.
Thanks to @arjyparjy & Gregg Dourgarian for pointing out IELE to me!