Publications

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.

Here you can find featured publications conducted by our team members.

Publications in smart contract security

Our academic work centers on advanced vulnerability detection tools, utilizing research advancements in our tools, such as Vanguard (a static analyzer) and OrCa (an oracle-guided fuzzer).

Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain

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.

Veridise authors: Isil Dillig, Kostas Ferles

Published in: Verified Software: Theories, Tools, Experiments (VSTTE)

Read

Demystifying Loops in Smart Contracts

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.

Veridise authors: Benjamin Mariano, Isil Dillig

Published in: CAV 2024 Computer Aided Verification conference

Read

SolType: Refinement Types for Arithmetic Overflow in Solidity

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.

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

Published in: Principles of Programming Languages (POPL)

Read

Synthesis-Powered Optimization of Smart Contracts via Data Type Refactoring

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.

Veridise authors: Işil Dillig

Published in: Object-oriented Programming, Systems, Languages and Applications (OOPSLA)

Read

SmartPulse: Automated Checking of Temporal Properties in Smart Contracts

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.

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

Published in: IEEE Symposium on Security and Privacy (Oakland)

Read

Publications in zero-knowledge proof security

The advancements in our academic research on zero-knowledge security are directly integrated into our in-house ZK vulnerability detection tools: Picus and ZK Vanguard.

Split Gröbner Bases for Satisfiability Modulo Finite Fields

This research paper aims to improve the scalability of solvers used in the automated verification of cryptosystems by addressing the inefficiencies of previous solvers that build a full Gröbner basis (GB) for systems of field equations.

Authors: Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Işil Dillig

Published in: CAV 2024 Computer Aided Verification conference

Read

Practical Security Analysis of Zero-Knowledge Proof Circuits

This research paper presents a lightweight technique for detecting vulnerabilities in zero-knowledge proof circuits, focusing on those written in Circom, a popular domain-specific language (DSL). The paper introduces a static analysis framework that uses a new program abstraction called Circuit Dependence Graph (CDG) to capture key properties of the circuit.

Authors: Jon Stephens, Kostas Ferles, Shankara Pailoor, Işil Dillig

Published in: USENIX Security Conference

Read

Automated Detection of Under-constrained Circuits in Zero-Knowledge Proofs

This research paper addresses the issue of underconstrained arithmetic circuits in zero-knowledge proofs, which can lead to security vulnerabilities. These circuits, generated by domain-specific languages (DSLs) like Circom, can admit multiple witnesses for a given input, enabling malicious parties to create bogus proofs.

Authors: Shankara Pailoor, Jacob Van Gaffen, Işil Dillig

Published in: Academic Paper PLDI 2023

Read

Certifying Zero-Knowledge Circuits with Refinement Types

The paper addresses the challenge of verifying the correctness of zero-knowledge (ZK) proof systems, which are essential for secure applications like privacy-preserving apps and Layer 2 scaling solutions (ZK-Rollups).

Authors: Bryan Tan, Işıl Dillig

Published in: IEEE Security & Privacy Conference Oakland Security

Read

Key takeaways from our research publications

Not in the mood to read the full papers?
We’ve got you covered—check out the summaries in these two blog posts!

Academic research: Findings from our smart contract security research

Picture of Mikko Ikola
Mikko Ikola

Aug 28

| 6 min read

Read

Picture of Mikko Ikola
Mikko Ikola

Aug 28

| 6 min read

Read

Academic research: Findings from our zero-knowledge research

Picture of Mikko Ikola
Mikko Ikola

Sep 10

| 6 min read

Read

Picture of Mikko Ikola
Mikko Ikola

Sep 10

| 6 min read

Read

Considering an audit?
Contact us today!

Contact Us