Fu Song

Smart contracts facilitate and enforce agreements between untrusted parties without trusted intermediaries, but vulnerabilities within contracts can cause severe damage once exploited. Various analysis techniques have been proposed for vulnerability detection, but they are typically limited to specific vulnerability types. While recent frameworks employ aggregation to broaden detection capacity, they often accumulate false positives due to loose integration that fails to resolve underlying conflicts. Meanwhile, the semantic reasoning capacity of large language models (LLMs) has shown promise in detecting vulnerabilities, despite inherent reasoning bottlenecks and hallucinations. Recognizing these challenges, in this work, we propose a novel neuro-symbolic approach, named Ensemble LLM-Assisted Static Analysis (ELSA). ELSA comprises two key modules, namely, LLM-assisted static analysis and analyzer ensemble (the ensemble of multiple LLM-assisted static analyzers), each incorporating two distinct strategies. The LLM-assisted static analysis augments individual analysis techniques with constraint-guided neural semantic reasoning, while the analyzer ensemble resolves conflicting outputs to distill a robust consensus. We evaluate ELSA on a comprehensive benchmark, including three open-source datasets and additional self-constructed Zero-Knowledge Proof-based smart contracts whose complexity poses unique challenges to static analysis. Experimental results demonstrate that our approach achieves an overall improvement of at least 17% over baselines and advanced mainstream approaches, effectively bridging semantic gaps and synergizing the complementary advantages of different analyzers. Furthermore, an ablation study and fine-grained analysis are conducted to investigate the key factors contributing to overall performance gains.

Smart contracts have achieved significant success, however, their security remains a long-standing challenge. The immutability and transparency of smart contracts require establishing a strong mechanism to prevent private leakage and trusted data tampering. Apart from traditional logic and code-level vulnerabilities arising from insufficient control over contract variables and function parameters, smart contracts may store private-dependent information in blockchain records, which is a critical type of vulnerability, but often overlooked in existing security analysis. In this paper, we present an automated approach for synthesizing security policies, named SmartIFSyn, to eliminate information flow vulnerabilities in smart contracts. We formalize the semantics of Solidity, the most widely used smart contract language, and analyze information flow security of Solidity smart contracts from two perspectives: local-variable security and global-interaction security. We present a type system to guide the elimination of local-variable vulnerabilities by inferring a policy and resort to constraint solving to synthesize a desired policy in case that the type system fails. The policy ensures both local-variable and global-interaction security while it is maximally aligned with user preference. Furthermore, the policy can be subsequently converted into enforceable specifications. We implement our approach in a tool and evaluate it on 17,160 real-world Ethereum smart contracts. The experimental results demonstrate the efficacy of our approach, e.g., detected 243 vulnerabilities in 223 real-world Ethereum smart contracts.

Dynamic languages like Python are highly valued for the flexibility they offer, primarily due to their dynamic typing system. However, this flexibility often comes at a cost: type-related errors typically manifest only at runtime, which can result in elusive bugs. This scenario highlights the urgent need for effective automatic type inference strategies. Recently, there has been significant progress in the development of deep learning-based methods targeting the issues. Despite their potential, these methods face considerable limitations in the context of rare types (predominantly user-defined types in Python), which are often underrepresented in training datasets. To tackle the inherent unpredictability of dynamic characteristics in Python, we present an innovative framework named RunTyper. RunTyper uniquely integrates dynamic analysis with a sophisticated framework that combines dynamic instrumentation and static rules. This hybrid approach is utilized to validate and refine predictions made by deep neural networks. When compared with Type4Py, a deep learning-based type inference tool, the experiment results indicate that RunTyper achieves a significantly higher accuracy rate of 53.7%, whereas Type4Py attains only 41.9%. Additionally, a series of experiments demonstrate that RunTyper significantly enhances performance in user-defined types. When compared to HiTyper, which similarly seeks to refine deep type inference but is limited to static rules, RunTyper exhibits a notable improvement, increasing accuracy from 17.0% to 22.9%, an enhancement rate of 35%. Moreover, the experiments indicate that RunTyper improves the accuracy of GPT-4 in processing user-defined types by a remarkable 17%. These findings emphasize RunTyper’s proficiency in refining and enhancing the results produced by deep prediction models as well as its ability to accurately infer rare types that are traditionally difficult to predict.

Solving constraints involving inductive (aka recursive) definitions is challenging. State-of-the-art SMT/CHC solvers and first-order logic provers provide only limited support for solving such constraints, especially when they involve, e.g., abstract data types. In this work, we leverage structured prompts to elicit Large Language Models (LLMs) to generate auxiliary lemmas that are necessary for reasoning about these inductive definitions. We further propose a neuro-symbolic approach, which synergistically integrates LLMs with constraint solvers: the LLM iteratively generates conjectures, while the solver checks their validity and usefulness for proving the goal. We evaluate our approach on a diverse benchmark suite comprising constraints originating from algebraic data types and recurrence relations. The experimental results show that our approach can improve the state-of-the-art SMT and CHC solvers, solving considerably more (around 25%) proof tasks involving inductive definitions, demonstrating its efficacy.

Formal verification provides critical security assurances for neural networks, yet its practical application suffers from the long verification time. This work introduces a novel method for training verification-friendly neural networks, which are robust, easy to verify, and relatively accurate. Our method integrates neuron behavior consistency into the training process, making neuron activation states remain consistent across different inputs within a local neighborhood. This reduces the number of unstable neurons and tightens the bounds of neurons thereby enhancing the network's verifiability. We evaluated our method using the MNIST, Fashion-MNIST, and CIFAR-10 datasets with various network architectures. The experimental results demonstrate that networks trained using our method are verification-friendly across different radii and architectures, whereas other tools fail to maintain verifiability as the radius increases. Additionally, we show that our method can be combined with existing approaches to further improve the verifiability of networks.

In the rapidly evolving landscape of neural network security, the resilience of neural networks against bit-flip attacks (i.e., an attacker maliciously flips an extremely small amount of bits within its parameter storage memory system to induce harmful behavior), has emerged as a relevant area of research. Existing studies suggest that quantization may serve as a viable defense against such attacks. Recognizing the documented susceptibility of real-valued neural networks to such attacks and the comparative robustness of quantized neural networks (QNNs), in this work, we introduce BFAVerifier, the first verification framework designed to formally verify the absence of bit-flip attacks against QNNs or to identify all vulnerable parameters in a sound and rigorous manner. BFAVerifier comprises two integral components: an abstraction-based method and an MILP-based method. Specifically, we first conduct a reachability analysis with respect to symbolic parameters that represent the potential bit-flip attacks, based on a novel abstract domain with a sound guarantee. If the reachability analysis fails to prove the resilience of such attacks, then we encode this verification problem into an equivalent MILP problem which can be solved by off-the-shelf solvers. Therefore, BFAVerifier is sound, complete, and reasonably efficient. We conduct extensive experiments, which demonstrate its effectiveness and efficiency across various activation functions, quantization bit-widths, and adversary capabilities.

Currently, large pre-trained language models are widely applied in neural code completion systems. Though large code models significantly outperform their smaller counterparts, around 70% of displayed code completions from Github Copilot are not accepted by developers. Being reviewed but not accepted, their help to developer productivity is considerably limited and may conversely aggravate the workload of developers, as the code completions are automatically and actively generated in state-of-the-art code completion systems as developers type out once the service is enabled. Even worse, considering the high cost of the large code models, it is a huge waste of computing resources and energy, which severely goes against the sustainable development principle of AI technologies. However, such waste has never been realized, not to mention effectively addressed, in the research community for neural code completion. Hence, preventing such unhelpful code completions from happening in a cost-friendly way is of urgent need. To fill this significant gap, we first investigate the prompts of unhelpful code completions, called “low-return prompts.” We empirically identify four observable patterns in low-return prompts, each lacking necessary information, making it difficult to address through enhancements to the model’s accuracy alone. This demonstrates the feasibility of identifying such low-return prompts based on the prompts themselves. Motivated by this finding, we propose an early-rejection mechanism to turn down low-return prompts by foretelling the code completion qualities. The prompts that are estimated to receive unhelpful code completions will not be sent to the model. Furthermore, we investigated five types of estimators to demonstrate the feasibility of the mechanism. The experimental results show that the estimator can reject 20% of code completion requests with a 97.4% precision. To the best of our knowledge, it is the first systemic approach to address the problem of unhelpful code completions and this work also sheds light on an important research direction of large code models.