What makes Move Safe?

On the 4th of March, Pontem hosted a panel discussion at MoveCon featuring industry leaders from MoveBit, and Aptos. The topic of the discussion was what makes Move safe?

You can listen to the full recording on Twitter or YouTube.

Meet the Speakers:

• Wolfgang Grieskamp: Lead of Move on Aptos with an impressive track record at Meta where he worked on the formal verification tool for the Move language – Move prover.

• Yi: Co-founder of Movebit, a security company focused on the Move ecosystem and building the standard for secure Move applications.

• Boris: Co-founder and CTO of Pontem Network, he is well-versed in the Move language and serves as the lead Move smart contract developer on Pontem.

What Safety Means for Smart Contract Languages: Exploring what makes Move Safe

Ensuring safety in smart contracts is of paramount importance in the blockchain industry as even a minor vulnerability can lead to catastrophic outcomes, given the enormous value of assets involved. Therefore, the choice of programming language plays a crucial role in guaranteeing the safety and dependability of smart contracts.

However, what exactly does safety imply in the context of smart contract languages?

The primary objective of safety in smart contract languages is to comprehend what is happening within the contract and prevent potential issues caused by bugs or security vulnerabilities such as  the reentrancy problem, a typical smart contract issue where the contract executes multiple calls to itself, leading to a depletion of funds.

The Move language provides developers with valuable tools such as the Move prover, which assists in ensuring the proper functionality of their contracts.

By utilizing Move, developers can specify the intended actions and rules that their contract should abide by. During the contract's execution, the Move language verifies that these rules are adhered to, resulting in fewer errors and security vulnerabilities.

The Move language is not flawless and may not have all the features required for absolute safety. However, it represents a significant step forward in smart contract language design and provides a solid foundation for developers to build safe and reliable contracts.

Move Language: Empowering Developers to Build Safe and Secure Smart Contracts

Move Language empowers developers to create secure and reliable blockchain applications, allowing them to build with confidence. The language's advanced features prevent errors and vulnerabilities, ensuring that applications function as intended. These features include:

• Linear Type System:

Move has a strong linear type system which ensures that data structures within a Move program can only be accessed and modified in certain ways. This helps prevent unexpected behavior.

• Visibility System:

Move also has a robust visibility system that allows developers to control exactly how data can be accessed, modified, and stored within a blockchain. This helps prevent unauthorized access to sensitive data or code.

• Modulation:

Move is also highly modular, which allows for the ownership of resources by modules, meaning that only the module that defines the source can modify the resources. This creates a well-protected data structure, as only authorized modules can access and modify the information within.

Move Ahead of the Curve: Embracing Move for Safe and Efficient Programming

While some experience with programming is necessary to fully understand Move's capabilities, the language's basic concepts are relatively easy to grasp. Learning the type system and abilities is a good starting point, and more advanced features can be mastered over time.

Move's safety features make it an attractive option for larger corporations and traditional tech companies. As concerns regarding data breaches and cyber attacks continue to rise, many companies are actively searching for ways to safeguard their data and minimize risk. By employing a language such as Move, developers can effectively manage sensitive transactions and data.

As Move gains traction in the industry, it may become a prevalent language for efficient system design and smart contract development. Projections suggest that the majority of the industry may employ Move for these purposes in the next five years.

Solidity Vs Move: Advantages and Limitations

While Move is designed to be more secure and scalable than Solidity, it currently lacks some of the features and capabilities that Solidity offers such as dynamic dispatch. However, experts are actively working on improving the Move language, with plans to add some form of dynamic dispatch and other features that will make migration from Solidity easier for developers.

Furthermore, lead Move developers are working on new educational materials and development tools to make it easier for developers to learn and use Move. This includes a compiler for Move to the Ethereum Virtual Machine (EVM), making it interoperable with Solidity contracts.

Additionally, the Move team is also experimenting with a dialect of Move called "async move," which aims to enable synchronous calls between different virtual machines. This could allow for even greater interoperability between different blockchain ecosystems, potentially solving one of the biggest challenges facing the blockchain industry.

The Origins of Move: A Look at the Inspiration and Development of Move

Wolfgang shares an insider's perspective on the history of Move and what drove its creation.

According to him, Move was not born out of a desire to create a new language, but rather out of a necessity to address certain limitations that existed with the options available at the time. The team at Libra explored different possibilities for programming the blockchain and concluded that using Solidity or EVM, the popular options at the time, wasn't the right fit due to safety concerns.

Instead, they looked at using bytecode assembly and executing Rust inside of it. However, certain key aspects like metering of guests and determinism of execution were still missing, which led them to explore the possibility of creating a new language altogether.

The language, which we know today as Move, was created two years after the decision was made to create it. The designers first created Move Intermediate Representation (MVIR) and the Move Virtual Machine (MVM) to define the core concepts and safety aspects of the language. For a long time, there was only MVIR. Then, the aspects of the Move Prover and all the semantics of the type checker were explored on the level of the MVM.

The Power of Formal Verification: Catching Bugs and Enhancing Security with Move

The Move language prioritizes security and includes a specialized tool called the Move prover for formal verification. Formal verification is the process of using mathematical and logical methods to prove that a program meets its specification.

Specifications can include requirements for the environment, constraints on inputs and outputs, and guarantees about the behavior of the program under different conditions.

By verifying a program's correctness, Move developers can catch errors and bugs early in the development process, before they become expensive and time-consuming to fix.

Nonetheless, formal verification is a challenging process. Writing specifications can be challenging, as it requires a deep understanding of the program's behavior and the problem domain it addresses.

Formal verification tools and techniques can also be complex and difficult to use by developers who lack specialized training and expertise in blockchain security. Thus expert advice from blockchain auditors may be required.

ABOUT PONTEM

Pontem is a product development platform that enables global financial inclusion through blockchain technology. Pontem is developing infrastructure and decentralized tools for the fastest and most scalable Layer 1 blockchain – Aptos.

The Pontem Wallet is the gateway to the Aptos ecosystem available for Chrome,  Firefox, and iOS. Pontem Wallet users can send and receive tokens, connect to decentralized applications, and explore the Aptos ecosystem.

As a result of its partnership with Aptos, Pontem has developed foundational dApps like the Move Playground IDE, Liquidswap AMM, and ByteBabel code translator.