Academic research: Findings from our smart contract security research

Veridise
Veridise
Published in
6 min readAug 28, 2024

At Veridise, we combine cutting-edge academic research with the latest industry experience.

Along with our extensive experience auditing key blockchain infrastructure protocols, smart contracts, and zero-knowledge implementations, many of our team members have academic research backgrounds.

In this blog post, we’d like to feature the academic research on smart contract security conducted by our team members and how it relates to the work we do at Veridise. We’ve also conducted extensive zero-knowledge security research, which we will feature in the next (Part II) blog post.

We’ve picked five papers and cover the following:

Below, we’ve summarized each paper, along with their authors from the current Veridise team — click on each name to learn more about our team members!

Veridise’s academic research series:
📚 Part I: Findings from our smart contract security research
📚 Part II: Finding from our zero-knowledge security research (to-be-published)

SmartPulse: Automated Checking of Temporal Properties in Smart Contracts

Veridise Authors: Jon Stephens, Kostas Ferles, Benjamin Mariano, Işil Dillig.

The SmartPulse paper can be seen as the foundational work that kickstarted Veridise. Its novel methods for checking the liveness properties of smart contracts generated significant interest among blockchain security experts, prompting the early team to establish Veridise.

The paper addresses the challenge of verifying liveness properties in smart contracts. Checking liveness properties means ensuring that “something good” will eventually happen (e.g., “I will eventually receive my refund”), rather than just verifying safety properties (”X will never happen”). To tackle this, the authors introduce SmartPulse, a tool that can automatically verify both safety and liveness properties in smart contracts.

SmartPulse introduces a new specification language, SmartLTL, tailored for expressing temporal properties specific to smart contracts over blockchain states. It also allows for customizable attack models, enabling comprehensive testing under various threat scenarios. The tool is fully automated and can generate concrete attack scenarios for vulnerable contracts. SmartPulse was evaluated on a total of 1947 smart contracts, showing that liveness checking can be done at scale and produce counter-example that correspond to realistic attacks.

Interestingly, the SmartLTL specification language was an inspiration for the [V] specification language that we currently use in our in-house tools such as OrCa.

Synthesis-Powered Optimization of Smart Contracts via Data Type Refactoring

Veridise Author: Işil Dillig

This paper tackles the problem of optimizing gas usage in Ethereum smart contracts by automatically refactoring data layouts. This is important because executing smart contracts on Ethereum costs gas, which is tied to real-world currency. Reducing gas usage makes contracts more cost-efficient.

While there has been prior work on reducing gas usage, they focus on low-level optimizations. This is the first paper to reduce gas usage by changing the data representation, and the results show significant savings.

The solution proposed in this work introduces a domain-specific language (DSL) for specifying type-level transformations and uses program synthesis to automatically generate a functionally equivalent contract with an optimized data layout. The approach leverages a novel synthesis technique that finds the most gas-efficient code under given transformations. The tool, Solidare, significantly reduces gas consumption in real-world contracts.

SolType: Refinement Types for Arithmetic Overflow in Solidity

Veridise Authors: Bryan Tan, Benjamin Mariano, Işil Dillig

This paper aims to prevent arithmetic overflow and underflow in Solidity smart contracts. The paper introduces SolType, a refinement type system that allows developers to annotate contracts to prove the safety of arithmetic operations.

The system can express complex relationships between integer values and aggregate properties of data structures. Implemented in a prototype called Solid, SolType includes a type inference engine to automatically infer useful type annotations and contract invariants.

Evaluations on 120 smart contracts show that Solid can automatically eliminate 86.3% of redundant SafeMath calls, outperforming the state-of-the-art Solidity verifier Verismart in both accuracy and efficiency.

Demystifying Loops in Smart Contracts

Authors: Benjamin Mariano, Isil Dillig

The paper addresses the challenge of analyzing loops in Solidity smart contracts, which are more common than previously thought, occurring in about one in five contracts. The authors study over 20,000 Solidity contracts deployed on the Ethereum blockchain.

Traditional analysis tools often overlook the complexity of these loops, leading to potential security and functionality issues. To tackle this, the authors introduce a domain-specific language (DSL) called Consul, designed to summarize common looping patterns in Solidity. They also develop a program synthesis toolchain named Solis, which can automatically generate loop summaries using Consul.

The evaluation shows that Solis can summarize 56% of analyzed loops, with 81% of these summaries being exactly equivalent to the original loops. The study identifies key semantic patterns in Solidity loops, emphasizing the need for tailored analysis tools in smart contract verification.

At Veridise, we have used the lessons from the Solis evaluation to inform the development of our various tailored analysis tools for Solidity smart contract verification and bug-finding.

Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain

Veridise Authors: Isil Dillig, Kostas Ferles

This paper was one of the first papers to introduce fully automated formal verification for smart contracts, aiming to ensure the correctness of smart contracts within Microsoft’s Azure Blockchain Workbench.

Given a smart contract and a property defined as a finite state machine, the proposed technique can automatically determine whether the smart contract satisfies or violates the property.

The proposed approach was implemented in a tool called VeriSol and applied to all application contracts in the Azure Blockchain Workbench and uncovered previously unknown bugs. After these bugs were fixed, VeriSol successfully performed full verification of all the contracts.

The paper has been instrumental in shaping our in-house vulnerability detection tools, emphasizing the critical role of defining key protocol properties and verifying (either manually or automatically) that the protocol conforms to the property — both of which are vital for conducting thorough, high-quality security audits.

Conclusion

In summary, these five research papers on smart contract security led to the following tools, findings and contributed to the development of our in-house vulnerability detection software, such as:

  • SmartPulse, for checking the liveness properties of smart contracts. SmartPulse verified 1947 smart contracts and discovered several vulnerabilities. Afterwards, the work served as inspiration for the [V] specification language that we currently use in our in-house tools such as OrCa.
  • Solidare, which optimized real-world contracts and reduced gas usage effectively.
  • SolType, which eliminated 86.3% of redundant SafeMath calls in 120 contracts.
  • Solis, which studied loops in over 20000 Solidity smart contracts and was able to summarize 56% of them using the authors’ newly introduced DSL, with 81% of these summaries being exactly equivalent to the original loops.
  • VeriSol, which uncovered and fixed bugs in Azure Blockchain Workbench contracts, and later shaped our in-house vulnerability detection tools by emphasizing the critical role of defining and verifying key protocol properties.

We are committed to combining academic research with industry practice to enhance smart contract security and zero-knowledge security. More research is in the works, and we look forward to sharing it with you soon.

In our next blog post, we’ll feature our academic research on zero-knowledge security.

Veridise’s academic research series:
📚 Part I: Findings from our smart contract security research
📚 Part II: Finding from our zero-knowledge security research (to-be-published)

Author:
Mikko Ikola, Head of Marketing at Veridise

Thank you Isil Dillig, Bryan Tan, Jon Stephens for reviewing the blog post.

Want to learn more about Veridise?

Twitter | Lens | LinkedIn | Github | Request Audit

--

--

Veridise
Veridise

Hardening blockchain security with formal methods. We write about blockchain & zero-knowledge proof security. Contact us for industry-leading security audits.