Circom is a popular programming language for writing arithmetic circuits that can be used to generate zero-knowledge proofs (ZKPs) like zk-SNARKS. ZKPs have received tremendous attention in protocols like zkRollups. The Circom circuits are compiled to Rank-1 Constraint Systems (R1CS) circuits, based on which zk-SNARK proofs are generated. However, one major challenge associated with R1CS circuits is the problem of under-constrained circuits, which are susceptible to allowing incorrect computations to pass verification due to insufficient constraints, potentially leading to security vulnerabilities. In this paper, we propose a novel framework CONSCS to automatically verify Circom circuits. Our contributions are threefold: 1) we propose novel circuit inference rules to help reduce the size of circuits and to extract more comprehensive information than existing works; 2) we introduce the novel Binary Property Graph (BPG) as a highly efficient reasoning engine, outperforming all existing tools in effectiveness and efficiency; 3) we leverage fine-grained domain-specific information to guide the SMT solving to address non-linear constraints, increasing the success rate of SMT queries of existing works from 2.68% to 48.84%. We conduct experiments to show that CONSCS enhances the solved rate of existing works from around 50-60% to above 80%.

Zero-knowledge proof (ZKP) circuits implemented in programming languages like Circom are fundamental to blockchain and privacy-preserving applications. These code often suffer from constraint-related issues where constraints fail to accurately specify intended computations. While existing analysis tools have been proposed, they struggle with large-scale circuits containing complex template embeddings. We present ScaleCirc, a novel framework that addresses such limitations through: 1) systematic management of analysis redundancy via circuit deduplication strategies; 2) constrainedness propagation methods leveraging source code semantic information; and 3) a generalizable framework for different circuit analysis tasks. Evaluation on 691 real-world circuits shows ScaleCirc demonstrates higher efficiency, and successfully analyzes many Circom programs that existing works failed on.

Smart contracts are automated programs stored on a blockchain, featuring unique attributes such as permissionlessness, trustlessness, immutability, and transparency. These properties underpin an array of unprecedented decentralized services. Compiled into bytecodes, Ethereum smart contracts are executed within the Ethereum Virtual Machine (EVM). Ethereum's distinct gas mechanism assigns a price to each bytecode execution, incentivizing resource-efficient computing. However, a disconnect exists between conventional coding practices and the less intuitive gas consumption computation mechanism, resulting in inadvertent gas wastage. Gas-wasting code smells at the source code level have been studied in various related works; however, the task of manually identifying such code smells by reading through codes and reasoning about them is both time-consuming and economically inefficient. In this work, we propose to leverage Large Language Models (LLMs), which have seen a surge in popularity recently, to facilitate undertaking the labor-intensive part of the code-smell-finding pipeline. In particular, we focus on Solidity, the predominant programming language for Ethereum smart contracts. Overall, we identified 26 gas-wasting code smells, out of which 13 were not presented in previous papers. On average, applying these code smells led to a reduction of approximately 10.534% in deployment costs and 21.528% in message call costs across our test codes. We further make a report on each of the identified code smells with associated example contracts sourced from either previous literature or recently deployed contracts.

The Decentralized Autonomous Organization (DAO) has emerged as a popular governance solution for decentralized applications (dApps), enabling them to manage their members across the world. This structure ensures that no single entity can arbitrarily control the dApp without approval from the majority of members. However, despite its advantages, DAOs face several challenges within their governance processes that can compromise their integrity and potentially lead to the loss of dApp assets. In this paper, we first provided an overview of the DAO governance process within the blockchain. Next, we identified issues within 3 key components of the governance process: the Governance Contract, Documentation, and Proposal. Regarding the Governance Contract, malicious developers could embed backdoors or malicious code to manipulate the governance process. In terms of Documentation, inadequate or unclear documentation from developers may prevent members from effectively participating, increasing the risk of undetected governance attacks or enabling a small group of members to dominate the process. Lastly, with Proposals, members could submit malicious proposals with embedded malicious code in an attempt to gain control of the DAO. To address these issues, we developed automated methods to detect such vulnerabilities. To investigate the prevalence of these issues within the current DAO ecosystem, we constructed a state-of-the-art dataset that includes 3,348 DAOs, 144 documentation, and 65,436 proposals across 9 different blockchains. Our analysis reveals that many DAO developers and members have not given sufficient attention to these issues. For the Governance Contract, 176 DAOs allow external entities to control their governance contracts, while one DAO permits developers to arbitrarily change the contract's logic. In terms of Documentation, only 71 DAOs provide adequate guidance for their members on governance processes. As for Proposals, over 90% of the examined proposals (32,500) fail to provide consistent descriptions and code for their members, highlighting a significant gap in transparency within the DAO governance process. For a better DAO governance ecosystem, DAO developers and members can utilize the methods to identify and address issues within the governance process.

The Linux kernel is popular and well-maintained. Over the past decade, around 860 thousand commits were merged with hundreds of vulnerabilities (i.e., 223 on average) disclosed every year, taking the total lines of code to 35.1 million in 2022. Many algorithms have been proposed to detect the vulnerabilities, but few studied how they were induced. To fill this gap, we conduct the first empirical study on the Kernel Vulnerability Inducing Commits (KVIC), the commits that induced vulnerabilities in the Linux kernel. We utilized six different methods on identifying the Kernel Vulnerability Fixing Commits (KVFCs), the commits that fix vulnerabilities in the Linux kernel, and proposed the other four different methods for identifying KVICs by using the identified KVFCs as a bridge. In total, we constructed the first dataset of KVICs with 1,240 KVICs for 1,335 CVEs. We conducted a thorough analysis on the characteristics, purposes, and involved human factors of the KVICs and obtained many interesting findings and insights. For example, KVICs usually have limited reviewers and can still be induced by experienced authors or maintainers. Based on these insights, we proposed several suggestions to the Linux community to help mitigate the induction of KVICs.