Summary

In a recent presentation at Breakpoint 2023, a speaker from Sertora discussed the challenges of smart contract security, particularly within the realm of decentralized finance (DeFi) on the Solana blockchain. The increasing scale of crypto hacks and thefts emphasizes the need for reliable security solutions. Sertora's response to these challenges is formal verification, a systematic process that mathematically proves the correctness of smart contracts or highlights potential security breaches. Through this approach, the company aims to revolutionize the way Solana smart contracts are verified, ensuring higher safety standards in the crypto space.

Key Points:

The Challenges of Smart Contract Security

The rise of DeFi and blockchain technology has revolutionized financial transactions but has also introduced new security challenges. The speaker highlighted the alarming increase in crypto theft and the scale of hacks, making it imperative to seek out effective solutions for securing smart contracts. These solutions need to be robust and capable of adapting to the complexity and evolving nature of smart contracts.

The Role of Formal Verification

Formal verification stands as a beacon of hope in securing smart contracts. The technique involves constructing mathematical proofs to confirm that a program adheres to its specifications. In cases where specifications are not met, formal verification can identify the underlying issue. Sertora specializes in developing advanced formal verification tools that ease the process for developers and enhance the security of smart contracts on the blockchain. This method addresses the core needs of the blockchain sector by proving contract safety or identifying and rectifying vulnerabilities before deployment.

Sertora's Verification Approach

Sertora has been a prominent player in the formal verification domain since its establishment in 2018. Their verification tools have been successfully utilized in the Ethereum Virtual Machine (EVM) environment, analyzing millions of lines of code. In 2022, they turned their focus to the Solana ecosystem. The Sertora Prover, a proprietary tool, automatically scrutinizes Solana bytecode files (SBF) at various abstraction levels, ensuring that virtual machine details are considered during verification and even permitting code analysis without the source code or reliance on the compiler.

Case Study: Formal Verification of Squads' Multi-Sig Wallet

Sertora showcased its expertise through a case study involving the formal verification of a multi-signature wallet called "Squads." This sophisticated wallet, having undergone multiple manual audits and holding over 600 million dollars in assets, presented an ideal scenario to demonstrate the power of Sertora's tools in a complex DeFi application. The verification process targeted key components like the multi-sig mechanism and new features like time locks, proving essential safety properties and enhancing trust in the system.

Facts + Figures

• Security breaches in the crypto space have been on the rise over the last six to seven years.
• Sertora was founded in 2018, it's a globally operating company with expertise in verification and DeFi.
• Over two million lines of code in solidity and viper have been verified by Sertora within the EVM ecosystem.
• In 2022, Sertora began focusing on the verification of Solana smart contracts.
• The Solana ecosystem offers different levels of abstraction for verification, including rust IR, LLVM bytecode, and SBF.
• Formal verification at the SBF level entails challenges due to the loss of information during the compilation process.
• Sertora provides a tool, Sertora Prover, to formally verify SBF code, analyzing it mathematically for correctness against specifications.

Top quotes

• "The trend [of crypto hacks and theft] is actually at a scale, right? So it's increasing and the amount is getting bigger and bigger."
• "To write a specification is hard and it's time-consuming."
• "You need to decide which level of abstraction you want to do verification."
• "We don't trust anyone."
• "We are able to find... to build the proof that the code is safe."
• "A Squat is a very sophisticated multi-sig wallet, has already more than 600 million in asset secure."
• "You should be approved only if you reach the threshold."
• "We actually verify the SBF code."
• "You cover all the possible permissions that the member may have or any other informational value."

Questions Answered

What is the purpose of formal verification in smart contracts?

Formal verification serves to mathematically prove that a smart contract adheres to its predefined specifications, ensuring its correct operation and security. By either confirming safety or identifying violations, developers can employ this process to debug and refine smart contract code before deployment.

Why is formal verification important for the future of DeFi and blockchain technology?

As the amount of funds and sensitive transactions managed by smart contracts grows, the need for robust security measures becomes critical. Formal verification provides stronger security guarantees, ensuring that smart contracts operate as intended and helping to prevent costly hacks and thefts in the DeFi sector.

How does Sertora's formal verification tool work?

Sertora's tool, the Sertora Prover, inputs Solana bytecode files and applies a rigorous process of decompilation to reconstruct information lost during compilation. It then creates a mathematical formula representing the program's semantics and uses SMT solvers to determine the safety of the contract relative to its specifications.

What are the challenges in performing formal verification at the SBF level?

Verification at the Solana binary format (SBF) level includes all details of the Solana virtual machine, which is beneficial for thoroughness. However, a significant challenge arises due to the loss of information like types and pointer details during compilation, making verification a more complex task.

How did Sertora's formal verification approach aid Squads' multi-sig wallet?

Sertora rigorously examined several core parts of the Squads multi-sig wallet protocol through formal verification. By mathematically proving its safety properties, they increased confidence in the protocol's robustness against potential hacks or logical errors, enhancing the overall security of the wallet's stored assets.