The introduction of smart contracts surely was one of the greatest milestones in the history of the blockchain. But just like any innovation, smart contracts aren’t free of flaws and security issues.
Developers want to be sure that the contracts they write do exactly what they’re meant to do and that their code contains no hidden errors and vulnerabilities. And this is exactly what two networks, Zilliqa and Cardano, are offering. They plan to guarantee smart contract security within their protocols.
In this article, we talk about smart contract security in Cardano and Zilliqa and test both networks by trying to exploit a reentrancy vulnerability within their contracts.
Before we start investigating key features of Cardano and Zilliqa, let’s look closer at the nature of smart contracts and how you can ensure their security. A smart contract is a self-executing contract in which the terms of the agreement are written directly into the lines of its code.
Smart contracts are supposed to securely and impartially transfer funds between two or more parties, without requiring mutual trust between them. This means that a smart contract has to be completely secure with no loopholes or vulnerabilities hidden in its code.
Currently, there are several blockchain protocols that support smart contracts, Ethereum being the most popular. However, the Ethereum platform is far from being fully secure. Some of its past vulnerabilities have led to millions of tokens being stolen or lost. In 2016, the network even had to perform a hard fork to revert damage.
There are many things that can compromise a smart contract: programming mistakes, protocol bugs, compiler errors, and various attacks on the network. And the best way to solve this problem is to create a blockchain protocol that implements fully secure smart contracts. This requires creating a system that does exactly what the programmer intends, with no room for introducing any vulnerabilities or unexpected events.
In this article, we focus on two blockchain networks that are planning to create such systems and thereby guarantee a high level of smart contract security when using their protocols: Zilliqa and Cardano. Both of these networks have recently released their testnets and are currently on their way to becoming the next big smart contract platforms.
Note that we’re not trying to compare Zilliqa vs Cardano security but rather to see whether formal verification can help developers improve the security of smart contracts in general. So let’s look closer at what each of these blockchain platforms has to offer.
Cardano is a rather new blockchain platform built on the ADA cryptocurrency. The platform was launched in September 2017. One of the main differentiators of the Cardano project is the research-driven approach they implement at the development stage and the scientific philosophy of the project. The platform was even named after one of the greatest Renaissance mathematicians, Gerolamo Cardano.
Cardano has a lot of scientific papers describing the platform’s components and protocols. The project has an interesting approach to addressing scalability and governance issues, a description of which can be found on their website along with academic research. But in terms of smart contracts, the most important part of Cardano security is the Cardano Computation Layer (CCL).
CCL is Cardano’s smart contract platform, which consists of two layers:
- A formally specified virtual machine
- Formally specified languages
The combination of these two layers allows formally specified smart contracts to be easily verified against the virtual machine. To make these formal specifications possible, Cardano uses the K framework.
Let’s take a closer look at the process of verifying a contract on the Cardano network.
In Cardano, smart contracts are written in Haskell. The process of verifying a contract on this platform is a bit more complex than on other blockchain networks. Normally, it would take only three steps to create and run a smart contract (see Figure 1).
The code of a smart contract is compiled into bytecode (virtual machine instructions), which is later executed within the network.
However, a smart contract created in this way would be unverified, as there’s no way to be sure that the final bytecode does exactly what the developer wants it to do. This is a pressing challenge with Ethereum and its language, Solidity. In order to verify a smart contract, Ethereum developers have to rely on imperfect static or dynamic analysis tools like Manticore or Mythril.
Formal verification is used to prove that a contract behaves the way it’s supposed to behave. Any accidental (or intentional) vulnerabilities that may be introduced at the development stage would be discovered during verification. So the term formally verified contract basically means that a contract is free from any exploits and does exactly what the developer wants it to do.
In order to formally verify a smart contract, we need to add a couple of additional steps to the previous scheme (see Figure 2).
To create a formally verified smart contract, you need to provide formal specifications for both the contract and its execution environment. Then, a verification tool can take the compiled bytecode and check if it runs exactly the way it’s described in the specification of the contract when implemented on the specified virtual machine. In the case of Cardano, the verification tool is already included in the K framework.
All these additional steps are necessary to ensure that a smart contract doesn’t contain any errors.
Apart from performing full formal verification, the K framework allows you to detect some edge cases, such as potential reentrancy exploits in unverified contracts. This way, even contracts that haven’t been verified are in less danger of unknown vulnerabilities and code errors.
Now let’s move to the virtual machine implementations used by Cardano.
Currently, Cardano has two virtual machine implementations on two separate test networks: KEVM and IELE.
KEVM is the Ethereum virtual machine (EVM) that was specified by the K framework. It was mainly created to study the formal verification capabilities of the K framework and to make it easier for developers to switch from Ethereum to Cardano.
The framework generates both the compiler and the runtime from the language description. This way, Ethereum smart contracts written in Solidity can be verified and executed on the Cardano blockchain. Such verification allows for detecting all major vulnerabilities such as reentrancy, integer overflows, and unchecked function calls.
However, the main focus of the Cardano developers’ research is on the IELE virtual machine. Basically, IELE is an intermediate language for translating smart contracts written in higher-level languages into executable instructions. This virtual machine is also described in terms of the K framework and was designed to ease the process of building formal verification tools.
Unlike EVM, IELE is a register-based virtual machine. It has an unbounded number of registers and supports unbounded integers. This makes it even easier to verify smart contracts since you don’t have to worry about integer overflows or stack bounds. Also, similar to Ethereum, IELE uses gas to limit resource use and prevent DoS attacks.
In the next section, we talk about the second blockchain network that promises to guarantee smart contract security within its protocol – Zilliqa.
Just like Cardano, Zilliqa is a young project and was launched in June 2017. The platform uses the concept of sharding to solve the problem of blockchain scalability and also has its own language, Scilla. Let’s look closer at what Zilliqa can offer on smart contract security.
In contrast to the languages used by Cardano and Ethereum, Zilliqa’s smart contract language, Scilla, is not Turing complete. Turing completeness refers to whether a programming language can be used to implement any algorithm and simulate any Turing machine. A non-Turing complete programming language has a limited subset of functions.
The most common example of a Turing incomplete machine is a calculator. An ordinary calculator is able to perform the majority of basic calculations such as arithmetic calculations or simple algebraic tasks. However, an ordinary calculator can’t solve equations or plot graphs.
In terms of smart contracts, a non-Turing complete language does two things:
- On the one hand, it limits the freedom of a smart contract developer.
- On the other hand, it makes smart contracts easy to verify.
When a contract is supposed to handle large amounts of currency, this is surely an acceptable tradeoff. In the case of Scilla, being non-Turing complete allows the language to be fully formally verified by mathematical proofs.
Scilla is an intermediate language, just like Cardano’s IELE. However, you can write smart contracts directly in Scilla.
Scilla was designed to ensure the separation between:
- Computation and communication – Every computation (such as a balance change or function value) is handled separately as an atomic transaction, without the involvement of any third parties. If such involvement is required, the transaction ends and appropriate messages are sent and received.
- Effectful and pure computations – Any computation happening within a transition has to terminate and have a predictable effect on the state of the contract and the execution. This is achieved by creating a distinction between pure computations (plain calculations with primitive types) and impure or effectful computations (which read/write data to/from the database).
- Invocation and continuation – Every invocation of an external function has to be absolutely last in a transaction. This helps avoid multiple common pitfalls like uncontrolled reentrancy, but this also limits the expressiveness of the language. To regain some of the language’s expressive power, Scilla supports continuations, which are a form of callback. The caller provides a function that a callee will invoke instead of returning control to the caller.
The process of formal verification of smart contracts in Zilliqa is pretty similar to the process in Cardano. However, in the case with Zilliqa, the security of smart contracts is much easier to achieve thanks to a stricter development environment. As a result, even unverified contracts are considerably safer and contain fewer vulnerabilities and errors if they’re written in Scilla.
Now it’s time to explore the process of testing smart contracts on both platforms.
In order to test both platforms, we can try to recreate one of the most famous smart contract vulnerabilities – the reentrancy vulnerability. This vulnerability is infamous for having brought down many large smart contracts. In fact, the DAO hack that led to the split of Ethereum was caused by a reentrancy vulnerability. So this is a good test case for basic smart contract exploit prevention. If such a vulnerability can be exploited, the platform doesn’t really offer any additional security apart from the ease of formal contract verification.
Let’s start our tests with Cardano. This platform will be easier to check because it supports smart contracts written in Solidity. To run the test, we can simply take a vulnerable contract from Ethereum and attempt to publish and exploit it on Cardano.
Here’s what our sample vulnerable contract looks like:
In this example, the vulnerability comes from being able to unexpectedly call back into the withdraw function from a different contract while the withdraw function is being executed (basically, re-entering the function and executing it for a second time).
And here’s what the contract that exploits the reentrancy vulnerability looks like:
The script from the file does four things:
- Sets up web3 to use the Cardano testnet
- Generates an account (a private key) and requests some tokens from the faucet to fund the test
- Compiles smart contracts and sends them to the blockchain
- Executes the transactions that are required to reproduce the exploit
This experiment showed an interesting feature of the Cardano network: it didn’t accept any transaction that could lead to reentrancy. However, we can modify the target contract to prevent reentrancy:
In this case, the network accepts transactions successfully and the contract functions normally. So apparently potential reentrancy doesn’t work on KEVM. However, another common issue in Ethereum smart contracts, integer overflow, can be easily reproduced on this virtual machine. So without formal verification, contracts are still vulnerable to overflows.
As for Zilliqa, we can start by creating a testnet wallet and signing up to receive some tokens. Then we can test a sample smart contract using the online Scilla compiler. However, none of the vulnerabilities we tested in the previous section can be implemented in Scilla.
Reentrancy is impossible by design. All invocations and messages have to be at the end of the function and no calls can return to the sender. Furthermore, the virtual machine throws an error and reverts the transaction if an overflow is detected.
Zilliqa seems to have much better exploit prevention mechanisms in general thanks to its stricter execution environment. So even unverified contracts are considerably safer if they’re written in Scilla.
Note that we didn’t test any verified contracts. Only intended exploits that were described in the formal specification of the contract can possibly pass the formal verification process. But it would be strange and suspicious if certain vulnerabilities were added into a contract by design. So formally verified smart contracts shouldn't be introducing any dangerous vulnerabilities.
The next generation of blockchain networks will certainly bring a lot of exciting changes. Cardano and Zilliqa are two blockchain platforms united in their goal of improving the safety of smart contracts and making them less vulnerable to different code errors and exploits. To accomplish this and make sure that smart contracts behave just the way they’re supposed to, both platforms use formal verification.
The process of formally verifying smart contracts is an interesting topic by itself and may come up in our future posts.
Are you working on a blockchain-based solution? At Apriorit, we have a team of passionate professionals and true blockchain experts who can assist you in solving tasks of any difficulty. Get in touch with us by filling out the form below and we’ll get back to you shortly.