Detecting Bugs with Substantial Monetary Consequences by LLM and Rule-based Reasoning

Response to Reviewer 2yGP

Answers to Questions of Reviewer 2yGP

Q1. How were the rules derived?

      We are smart contract auditors with years of experience. We have studied many business models (and their variants). These rules are invariants (i.e., properties held across different business models) we manually summarized. We really appreciate the pointer to the inspiring “seven sins” paper [1]. As mentioned in the limitations of our submission (lines 613-615), our rules are not comprehensive. A large empirical study involving more domain experts would help us complete the rule set. In addition, our rules could be extended to capture smells, as according to the paper, smells are quite problematic.

Generalization to unknown bugs

      Please see C2 of the global response.

Using CodeLlama and CodeBert

      We tried CodeLlama-7B-instruct-hf and 13B-instruct-hf during rebuttal. CodeLlama-7B failed to produce formatted outputs in many cases such that our pipeline could not parse its results properly. Similar problems were observed in existing works [2,3]. 13B performs better in this matter. However, it does not seem to understand the nuances of various financial meanings even with the few-shot examples. As such, it produced much worse annotation results than our default setting (41.9% vs 75.6%). This indicates the level of intelligence of the underlying LLM is quite important. Please also see C1 in the global response, in which GPT4 has better performance than our default setting (using GPT3.5), namely, 86.6% annotation accuracy (versus 75.6%), fewer FPs, and a much smaller number of iterations before termination (2 vs 12), indicating that it has much fewer hallucinations. However, it also comes with a much higher cost.

      CodeBert generates embeddings for both code and natural languages and does not operate like an LLM that can answer our questions. As such, it cannot be used in our pipeline. Exploring integration of code-language models and LLMs is part of our future work.

Reducing FPs

      Thanks for your pointer to the ASE’22 paper [4]. Although our tool does not produce that many FPs, reducing them is always highly desirable. We will open-source the tool upon publication and plan to solicit feedback from the community through a large-scale study like the one in the paper. The authors have strong connections with both the blockchain industry and the auditing community. These connections will be instrumental for the study.

How to scale our approach

      Thank you for the pointer to the “Gang of Eight” paper [5]. The scale of the study in the paper and the impact are exemplary. We aim to achieve similar ramifications. Our work mainly followed the taxonomy proposed in [6], which studied 500 or so critical/exploitable real-world smart contract bugs in 2021-2022. We can clearly see the benefits of having a larger study than and a more thorough taxonomy than [6]. From our experience, accounting bugs continue to be a very important bug category, causing substantial monetary loss, and the current tool support is still insufficient. Moreover, we observe that recent smart contracts have increasingly complex business models which demand a more fine-grained study. We plan to conduct a larger scale study focusing on accounting bugs in the past five years and hopefully come up with a fine-grained taxonomy and a comprehensive set of invariants (similar to the rules in our submission). Similar to [1,4,5], we will leverage efforts/feedback from the community.

      We will cite [1,4,5] and include the above discussion in the paper.

References

[1] Rahman, A., et al. “The seven sins: Security smells in infrastructure as code scripts.” ICSE’19.

[2] Beurer-Kellner, Luca, et al. "Prompt Sketching for Large Language Models." ICML’24.

[3] Beurer-Kellner, Luca, et al. "Prompting is programming: A query language for large language models.", PLDI’23.

[4] Reis, S., et al. “Leveraging practitioners’ feedback to improve a security linter.”, ASE’22

[5] Rahman, A., et al. “Gang of eight: A defect taxonomy for infrastructure as code scripts.” ICSE’2064).

[6] Zhang, Zhuo, et al. "Demystifying exploitable bugs in smart contracts." ICSE’23.

Thank you for reviewing our paper. We hope that our responses have addressed your concerns. If there are any remaining issues or questions, we would greatly appreciate your feedback so we can make further improvements.

I would like to thank the authors for their time and addressing my comments. I have also read other reviewers' feedback and the authors global rebuttal and I have increased my score.

As this paper addresses an important yet underexplored real-world problem, e.g., automatically detecting accounting bugs, I will be happy to see this paper accepted.

I would request the authors to incorporate all reviewers' feedback in the camera-ready version if the paper is accepted.

Response to Reviewer uXwt

Answers to Questions of Reviewer F88y

Q1. False positive (FP) rate when bugs are unknown

      Please see C2 in the global response.

Q2. Code snippets included during prompting

      We prompt functions individually. We parse the output of each variable (including global variables). Our rules will propagate such information across functions (e.g., parameter passing from a caller to a callee and uses of the same global variable). In other words, we do not have to prompt a large code body (e.g., including relevant functions) because of the use of rules.

Q3. Other baselines

      Please see C1 in the global response.

Q4. Sensitivity to variable names

      We conducted an experiment in which we leveraged the Solidity compiler to rewrite variable names (to something as plain as v1, v2), without changing program semantics. We kept the function names. We then reran our pipeline with the modified code. Our results showed that the annotation accuracy degraded from 75.6% to 31.7%. The true positives (TPs) degrade from 19 to 14, and the FPs increase from 9 to 21. It is not surprising because without proper variable names, it is extremely difficult even for humans to decide the financial meaning of an operation, e.g., a simple addition. Please also see Q5 to find the explanation of why substantial annotation degradation may not yield proportional loss in TPs.

Q5. Incorrect annotation may not affect TP or FP, and What is essential for the system to detect accounting bugs effectively if the annotation is not perfect?

      For TPs, many incorrect annotations do not happen in the variables that are involved in the bugs. For FPs, the same operations (e.g., simple additions) are allowed for multiple financial types such that even though a variable is mis-annotated, the system may not flag its operation as an error. We will elaborate.

      To detect an accounting bug, the annotations for the variables involved in the business operation should be correct.

Q6. Termination of reflection

      It terminates when the LLM does not propose any new annotations for variables. Note that there are finite types of annotations and hence termination is guaranteed.

Can a model less powerful than GPT3.5 work?

      We tried CodeLlama-7B-instruct-hf and 13B-instruct-hf during rebuttal. CodeLlama-7B failed to produce formatted outputs in many cases such that our pipeline could not parse its results properly. Similar problems were observed in existing works [1,2]. 13B performs better in this matter. However, it does not seem to understand the nuances of various financial meanings even with the few-shot examples. As such, it produced much worse annotation results than our default setting (41.9% vs 75.6%). This indicates the level of intelligence of the underlying LLM is quite important. Please also see C1 in the global response, in which GPT4 has better performance than our default setting (using GPT3.5), namely, 86.6% annotation accuracy (versus 75.6%), fewer FPs, and a much smaller number of iterations before termination (2 vs 12), indicating that it has much fewer hallucinations. However, it also comes with a much higher cost.

References

[1] Beurer-Kellner, Luca, et al. "Prompt Sketching for Large Language Models." ICML’24.

[2] Beurer-Kellner, Luca, et al. "Prompting is programming: A query language for large language models.", PLDI’23.

Thank you for reviewing our paper. We hope that our responses have addressed your concerns. If there are any remaining issues or questions, we would greatly appreciate your feedback so we can make further improvements.

Response to Reviewer F88y

Answers to Questions of Reviewer F88y

Q1. How many times were the experiments run?

      Three due to the cost involved. We will clarify.

Q2. Origin of the rules

      We are smart contract auditors with years of experience. We have studied many business models (and their variants). These rules are invariants (i.e., properties held across different business models) we manually summarized. We are currently exploring using LLMs to extract a more comprehensive set of such properties. We will elaborate in the paper.

Q3. Manual evaluation process

      Three people were involved in the manual process. Two were annotating the variables independently, and the third served as a judge when inconsistencies occurred.

Comparison with [1] and [2]

      We cited [1] and the arxiv version of [2] in our submission (lines 472-474 and 454-456). [1] is an empirical study of exploitable bugs in real-world smart contracts and the effectiveness of existing tools on these bugs. It inspired us to work on accounting bugs as the authors found that such bugs are difficult, critical (as they may cause substantial financial loss), and beyond existing tools. [2] used prompt engineering (with Chain-of-Thought) to detect ten bug patterns. Most of them are not related to accounting bugs.

      Please also see C1 in the global response.

Scaling to other programming languages

      Solidity is the most popular programming language for smart contracts, and our implementation currently only supports that. The rule checker is implemented inside Slither, a Solidity analysis engine that generates intermediate representations (IR) of smart contracts and provides a rich set of APIs to manipulate the IRs. That said, it is possible to implement the rule checker at the source level (using just a parser), which would allow easy extension to other languages.

Comprehensiveness of the 119 rules

      Although these rules cover common business models, as stated in our limitations (lines 612-621), they are not comprehensive. For example, we currently do not model options in future contracts. We leave it for our future work.

References

[1] Zhang, Zhuo, et al. "Demystifying exploitable bugs in smart contracts." ICSE’23.

[2] Sun, Yuqiang, et al. "Gptscan: Detecting logic vulnerabilities in smart contracts by combining gpt with program analysis." ICSE’24.

Thank you for reviewing our paper. We hope that our responses have addressed your concerns. If there are any remaining issues or questions, we would greatly appreciate your feedback so we can make further improvements.

We are grateful for your continuous support and response, which discloses a few places that we did not sufficiently clarify.

1. Lower performance compared to [1]: [1] is an empirical study. It does not propose any technique. One of its important conclusions motivating our work is that accounting bugs are beyond existing automated tools. To confirm this, we double-check their project repo. There were only benchmark programs without any bug detection tools. Our tool is the first fully automated technique that can effectively detect accounting bugs.

2. ChatGPT-4: The reviewer may have some misunderstanding of our GPT-4 results. The reported results are acquired by replacing GPT-3 in our pipeline with GPT-4, not by directly prompting. Our technique is independent of the underlying LLMs. A more powerful LLM yielding better results is indeed a plus for our technique. Directly prompting GPT-4 (with few-shot examples) does not detect accounting bugs. In our experiment, GPT-4 was used to derive the annotations, which were further used in rule-based propagation and checking.

3. Comprehensiveness and clarity of the rules: our rules are comprehensive for common business logics. Note that since these are annotation propagation and checking rules. Problematic rules will lead to failures in type checking. The fact that our system can detect real accounting bugs and rarely has false positives (when typing thousands of functions) demonstrates the quality of our rules. That said, our rules do not model certain rare business behaviors such as options in future contracts. That is why we said our rules are not comprehensive. An analogy is that we are building some type system for Python programs. We design some rules. These rules allow typing common program behaviors, for example, those involving integers and strings. However, we lack rules to type rare behavior of complex numerical values. The rules are comprehensive and correct for typing the common behaviors, because if they were problematic, many correct Python programs (operating on integers and strings) would be flagged as having type errors, and buggy Python programs would escape the type checking. We will open-source our system and the rules upon publication.

4. Lower performance than other techniques: our tool has the state-of-the-art performance in automatically detecting accounting bugs. We have compared with recent automatic tools and tools that require intensive manual annotations. The results show that our tool substantially outperforms in terms of effectiveness and automation. We would be more than happy to empirically compare with any other tools that the reviewer may point us to before the discussion period ends.

Thank you again for your time. Please let us know if there are places that we can further clarify.

Based on the responses, the comprehensiveness and clarity of the rules being considered remain unclear. Additionally, the experiments presented in the rebuttal show that ChatGPT-4 significantly outperforms the proposed model, albeit with higher computational costs. This raises concerns about the effectiveness of your model in detecting bugs, especially given its lower performance compared to other techniques, including [1]. Thank you to the authors for their effort in the rebuttal. However, due to concerns about the rules considered and the model's performance relative to other approaches, my score remains unchanged.

Response to Reviewer zmms

Answers to Questions of Reviewer zmms

Q1. Replacing with rule-based reasoning with SMT solving and expressiveness of the reasoning technique

      It is possible to enhance our system with an SMT solver. In lines 346-348 of our submission, we mentioned that the most common reason for FPs is the lack of path feasibility reasoning. This can be addressed by using a solver. From our experience, the difficulty of handling accounting bugs may not lie in using inference rules or the much more expressive SMT solving. Instead, it lies in deriving a set of rules/invariants that generalize across a wide spectrum of business models. Complex reasoning rules often run the risk of being too specific to a subset of business models. That said, we do think more expressive reasoning methods such as Symbolic Finite Automata (SFA), which can model symbolic transitions between states could be quite useful in modeling stateful behaviors of business models. It belongs to our future work.

Q2. Baselines

      Please see C1 in the global response.

Q3. Benefits of finetuning

      Please see C1 in the global response.

Q4. Unknown bugs

      Please see C2 in the global response.

Covering more bug types

      Accounting bugs are quite different from other bugs as they are closely coupled with application specific business logics. Other bugs such as reentrancy and frontrunning have precise definitions and general oracles. To some extent, accounting bugs are analogous to the traditional functional bugs, whereas other smart contract bugs are analogous to buffer-overflow and divided-by-zero bugs. In traditional bug detection, functional bugs are a lot more difficult to deal with than others. In our work, we use type rules, which essentially denote the invariants that all business models should respect, to construct a general detector. Although there may be future designs different from ours, we believe detectors for accounting bugs would likely be different from those for other bug types. Moreover, just like functional bugs, accounting bugs are quite diverse and can be further classified to many sub-categories such as normalization errors, unit errors, interest errors, etc.

Example in Sec-2 is too simplistic

      In general, accounting bugs are much more complex than that in Sec-2. We chose it for readability. The average reasoning trace for a real bug is 20 lines, where the trace for that example is only 4 lines.

Minor changes

      Thanks for pointing them out. We will change all of them accordingly.

Thank you for reviewing our paper. We hope that our responses have addressed your concerns. If there are any remaining issues or questions, we would greatly appreciate your feedback so we can make further improvements.