Andrei Arusoaie

Stefan-Claudiu Susan, Andrei Arusoaie, Dorel Lucanu

The irreversible nature of blockchain transactions makes the identification of smart contract vulnerabilities an essential requirement for secure system development. While Large Language Models (LLMs) are increasingly integrated into developer workflows, their reliability as autonomous security auditors remains unproven. We assess whether current generative models are a viable replacement for, or only a complement to, traditional static-analysis tools. Our findings indicate that LLM efficacy is undermined by both inherent lexical bias and a lack of rigorous validation of external data inputs. This reliance on non-semantic heuristics, such as identifier naming, leads to a high frequency of false positives. Furthermore, prompting techniques reveal a trade-off between precision and recall. These results were derived using our custom automated framework, which achieves 92% accuracy in classifying model outputs.

Ştefan-Claudiu Susan, Andrei Arusoaie, Dorel Lucanu

The high rate of false alarms from static analysis tools and Large Language Models (LLMs) complicates vulnerability detection in Solidity Smart Contracts, demanding methods that can formally or empirically prove the presence of defects. This paper introduces a novel detection pipeline that integrates custom Slither-based detectors, LLMs, Kontrol, and Forge. Our approach is designed to reliably detect defects and generate proofs. We currently perform experiments with promising results for seven types of critical defects. We demonstrate the pipeline's efficacy by presenting our findings for three vulnerabilities -- Reentrancy, Complex Fallback, and Faulty Access Control Policies -- that are challenging for current verification solutions, which often generate false alarms or fail to detect them entirely. We highlight the potential of either symbolic or concrete execution in correctly classifying such code faults. By chaining these instruments, our method effectively validates true positives, significantly reducing the manual verification burden. Although we identify potential limitations, such as the inconsistency and the cost of LLMs, our findings establish a robust framework for combining heuristic analysis with formal verification to achieve more reliable and automated smart contract auditing.

Andreea Buterchi, Andrei Arusoaie

Lots of existing web applications include a component for rating internet resources (e.g., social media platforms include mechanisms for rating videos or posts). Based on the obtained rating, the most popular internet resources can generate large amounts of money from advertising. One issue here is that the existing rating systems resources are entirely controlled by a single entity (e.g., social media platforms). In this paper we present a blockchain-based decentralized application for rating internet resources. The proposed solution provides a transparent rating mechanism, since no central authority is involved and the rating operations are handled by a specialised smart contract. We provide an implementation of our idea, where we combine existing authentication methods with blockchain specific features so that anonymity is preserved. We show that this approach is better than existing rating components present in various web applications.

Andrei Arusoaie, Ionut Pistol

Artificial Intelligence problems, ranging form planning/scheduling up to game control, include an essential crucial step: describing a model which accurately defines the problem's required data, requirements, allowed transitions and established goals. The ways in which a model can fail are numerous and often lead to a failure of search strategies to provide a quick, optimal, or even any solution. This paper proposes using SMT (Satisfiability Modulo Theories) solvers, such as Z3, to check the validity of a model. We propose two tests: checking whether a final(goal) state exists in the model's described problem space and checking whether the transitions described can provide a path from the identified initial states to any the goal states (meaning a solution has been found). The advantage of using an SMT solver for AI model checking is that they substitute actual search strategies and they work over an abstract representation of the model, that is, a set of logical formulas. Reasoning at an abstract level is not as expensive as exploring the entire solution space. SMT solvers use efficient decision procedures which provide proofs for the logical formulas corresponding to the AI model. A recent addition to Z3 allowed us to describe sequences of transitions as a recursive function, thus we can check if a solution can be found in the defined model.