The last few weeks in the world of smart contracts have been definitely interesting. From spectacular proposals for SVM integrations to the Vyper exploitation crippling Curve and almost annihilating our DeFi ecosystem, the narrative is pretty clear for what the next wave of smart contract needs are: a natively secure and high-throughput virtual machine powered by a cutting-edge programming language. For years, reentrancy has been the most notable attack vector in crypto, especially for the large DeFi hacks.

The Curve Attack:

Looking recently at the Curve attack, the fallback function allowed multiple reentrant AddLiquidity() and RemoveLiquidity() functions, enabling the attackers to exit the pools with excess assets relative to their initial deposit while the pool retained the pre-deposit balance and the LP token mint and burn records showing pretty accurate values. Liquidity in affected pools was drained as the attackers repeated this sequence.

In this case, the fallback function recalls the fund’s withdrawal function in an attempt to exploit target pools. The fallback function is executed in a loop as the attacker’s resources are retained in the execution sequence after the initial transaction is executed.

The DAO Attack:

The infamous DAO attack was also an industry-devastating event that crippled Ethereum’s ecosystem.

The DAO's splitDAO function, meant for token holders who wanted to leave the DAO and create their own 'child DAO', had a flaw in the sequence of its operations. This flaw made it susceptible to a reentrancy attack.

1. Initial Setup: The attacker first became a participant in The DAO by purchasing DAO tokens. This meant they had some ether inside The DAO represented by the tokens they held.

2. Malicious Contract Creation: The attacker didn't initiate the attack directly from a regular Ethereum address. Instead, they crafted a malicious contract. This contract had a specially designed fallback function that would be invoked when the contract received ether.

3. Triggering the splitDAO: From their malicious contract, the attacker then called the splitDAO function to create a 'child DAO'. When it came time for The DAO to return the Ether representing the attacker's DAO tokens (using the msg.sender.call.value(balance)()), the Ether was sent to the attacker's malicious contract, triggering its fallback function.

4. Reentrancy Through Fallback: The malicious fallback function, upon receiving this Ether, immediately called splitDAO again, requesting another withdrawal.

5. State Not Yet Updated: Because the state of the original contract (setting shares[msg.sender] = 0) only happened after the Ether was sent, and since the malicious contract initiated a new splitDAO call before that state change, from The DAO's perspective, the attacker still had their full balance. This allowed the attacker to "withdraw" the same amount again.

6. Recursive Drainage: This recursive call to splitDAO from the malicious fallback function happened multiple times, essentially allowing the attacker to drain Ether continuously until their original balance was many times withdrawn.

The flaw in The DAO's contract was the order of operations:

1. Sending Ether to an external address.

2. Then updating the internal state.

This order allowed the external address, especially if it was a contract with a specific function (like the malicious fallback in this case), to take advantage of the not-yet-updated state.

If The DAO's contract had first updated the internal state and then sent the Ether, the attack would not have been possible. This is because when the malicious fallback function made its reentrant call, the balance for the attacker would have already been set to zero.

For the nerds, here’s a simplified version of the crisis code:

function splitDAO(...) { 

var balance = shares[msg.sender]; // Get the balance of the sender        shares[msg.sender] = 0; // Set the sender's shares to 0    msg.sender.call.value(balance)(); // Send the Ether back to the sender ...

}

What now?

Many developers in the industry have acknowledged the flaws of Solidity and have turned to Rust-based languages. Within these developer groups, two main virtual machines have risen: the SVM and the MoveVM. While I personally am an ardent supporter of both and see use cases for both, it is evident that from a technical point-of-view the Move language takes the cake in terms of performance. Derived from the Rust language and designed by the Diem project from Facebook, Move was designed to be the blockchain-focused version of Rust (think Move is to Rust as React is to Javascript).

Move Safety Mechanisms

1. Use Case & Design Philosophy:

   • Rust: Designed as a general-purpose language with a focus on "safe concurrency" and "zero-cost abstractions". Was designed for multiple sectors and has rapidly grown in adoption across AI, blockchain, web development, etc

   • Move: Designed for blockchains specifically the Diem (previously known as Libra) ecosystem. With an unique set of requirements, blockchains have their own traits: immutability, consensus mechanisms, and especially the high-cost of errors (as seen with The DAO incident).

2. Safety Mechanism Deep Dive:

   Despite the revolutionary Anchor framework, the task of managing assets securely often falls on the shoulders of the developer: creating room for reentrancy and other major bugs.To combat this, Move was designed with these core principles:

   1. Resource Types: A central feature of Move is its "resource types". Resources are used to represent digital assets. They can't be copied or discarded, only moved between storage locations. This guarantees assets can't be unintentionally duplicated or lost.

   2. Module System: Move uses a module system where each module defines the resource types and procedures, creating a clear namespace and encapsulation. This allows for strong invariants about behavior and data integrity. It also allows for an intuitive development experience for newer/intermediate developers where they are able to

   3. Linear Type System: Similar to Rust's ownership system, Move's linear type system ensures that there is always a single "owner" for a resource. This is vital for representing digital assets, where double-spending is a concern. It embraces a linear execution and utility system that shuts out an attempt at a reentrance attack. The transaction signer or the private key holder is the principal entity in Move contracts with every function being modularized. This design means that every transaction is handled as a ‘one off’ request and leaves zero space for a successful repeat. For example, calling a fallback() function could eventually go through the RPC but get blocked at execution. In this case, linear execution ‘clears the rack’ once a transaction signed by the private key holder is successfully executed.

   4. Bytecode Verification: Furthermore, Move adds an extra layer of security to its smart contract execution through a bytecode verifier that guarantees type and memory safety. The bytecode verifier uses a borrowing-checking scheme which allows for only one mutable reference to a value at any given time. To simplify the recognition of the effects of write operations, the bytecode verifier ensures that the global storage is tree-based (like the Merkle root) and not graph-based. Graph-based storage systems are unstable and complicated due to a lack of direct structure. The Move verifier is always rigid and delivers this role even in the presence of untrusted code. It prevents hackers from making multiple manipulations that can crash multiple nodes and control entire account balances commonly known as the re-entrancy attack.

   5. Formal Verification: Move aims to integrate formal verification directly into its development process. Formal verification uses mathematical methods to prove the correctness of code, ensuring that smart contracts behave as intended. It does so through a few radical improvements

      1. Prover Tool: The “Move Prover” was designed specifically for performing formal verification on Move code. This tool translates Move bytecode into logical specifications, which are then checked by a backend solver to ensure that the code adheres to its specifications, ensuring that developers can understand who is accessing a smart contract, when they are accessing, and why they are accessing.

      2. Behavior Specifications: Move allows developers to write formal specifications directly in the Move code, alongside the implementation. These specifications are expressed in a high-level, declarative manner, allowing developers to define expected behaviors, invariants, postconditions, and preconditions. Essentially, devs can say who specify who has access to a module, when they have access, and why they have access.

      3. Rich Standard Library: The Move standard library, which provides core functionalities like handling of the MOVE token (shhhh teaser), is extensively specified and formally verified to ensure correctness.

      4. Modular Verification: The Move Prover performs modular verification. This means that it verifies each function and procedure independently of its callers. It helps in reducing the complexity of the verification process and ensures that each part of the code is correct.

      5. Boogie Intermediate Language: The Move Prover translates Move bytecode into an intermediate representation using the Boogie language. Boogie is an intermediate verification language that serves as an abstraction layer between high-level languages and theorem solvers. This translation facilitates the interaction with backend solvers like Z3 to prove the correctness of the code.

      6. Backend Solvers: After translating to Boogie, the Move Prover uses powerful theorem solvers like Z3 to check the correctness of the specifications against the translated code. If the solver finds a discrepancy between the specification and the code’s behavior, it indicates a potential error in the code.

      7. Invariant Maintenance: One key aspect of formal verification in Move is maintaining invariants, especially for the resource types. Invariants are conditions that remain true throughout the code execution. By specifying and checking these invariants, Move ensures that resources like tokens are handled safely and correctly.

The Future

With the rise of cutting-edge frameworks like Move, the question revolves around adoption. How can we bring Move to EVM-traditional communities where it can be adopted seamlessly (and even abstracted away)? Imagine a world where Curve could launch on a SDK and have built-in provers and linear logic that safeguards against reentrancy bugs. Or a world where any existing Solidity game facing throughput bottlenecks can seamlessly leverage parallel execution to tap into 160k+ TPS at will. It’s an honor to be working with a wicked team at Movement Labs to make this reality and make the MoveVM the standard for smart contract deployment.

Twitter: @rushimanche

TG: @rushiman