Searcharxiv⌕ Search

arXiv subjects

Zhe Hou

Publications and source records attributed to Zhe Hou.

At least 37 records · Page 2Linked to original sources

FTSmartAudit: A Knowledge Distillation-Enhanced Framework for Automated Smart Contract Auditing Using Fine-Tuned LLMs

The rapid growth of blockchain technology has driven the widespread adoption of smart contracts. However, their inherent vulnerabilities have led to significant financial losses. Traditional auditing methods, while essential, struggle to keep pace with the increasing complexity and scale of smart contracts. Large Language Models (LLMs) offer promising capabilities for automating vulnerability detection, but their adoption is often limited by high computational costs. Although prior work has explored leveraging large models through agents or workflows, relatively little attention has been given to improving the performance of smaller, fine-tuned models--a critical factor for achieving both efficiency and data privacy. In this paper, we introduce HKT-SmartAudit, a framework for developing lightweight models optimized for smart contract auditing. It features a multi-stage knowledge distillation pipeline that integrates classical distillation, external domain knowledge, and reward-guided learning to transfer high-quality insights from large teacher models. A single-task learning strategy is employed to train compact student models that maintain high accuracy and robustness while significantly reducing computational overhead. Experimental results show that our distilled models outperform both commercial tools and larger models in detecting complex vulnerabilities and logical flaws, offering a practical, secure, and scalable solution for smart contract auditing. The source code is available at Github repository.

cs.CR↗

QAE-BAC: Achieving Quantifiable Anonymity and Efficiency in Blockchain-Based Access Control with Attribute

Blockchain-based Attribute-Based Access Control (BC-ABAC) offers a decentralized paradigm for secure data governance but faces two inherent challenges: the transparency of blockchain ledgers threatens user privacy by enabling reidentification attacks through attribute analysis, while the computational complexity of policy matching clashes with blockchain's performance constraints. Existing solutions, such as those employing Zero-Knowledge Proofs (ZKPs), often incur high overhead and lack measurable anonymity guarantees, while efficiency optimizations frequently ignore privacy implications. To address these dual challenges, this paper proposes QAEBAC (Quantifiable Anonymity and Efficiency in Blockchain-Based Access Control with Attribute). QAE-BAC introduces a formal (r, t)-anonymity model to dynamically quantify the re-identification risk of users based on their access attributes and history. Furthermore, it features an Entropy-Weighted Path Tree (EWPT) that optimizes policy structure based on realtime anonymity metrics, drastically reducing policy matching complexity. Implemented and evaluated on Hyperledger Fabric, QAE-BAC demonstrates a superior balance between privacy and performance. Experimental results show that it effectively mitigates re-identification risks and outperforms state-of-the-art baselines, achieving up to an 11x improvement in throughput and an 87% reduction in latency, proving its practicality for privacy-sensitive decentralized applications.

cs.CR↗

The fate of disorder in twisted bilayer graphene near the magic angle

In disordered lattices, itinerant electrons typically undergo Anderson localization due to random phase interference, which suppresses their motion. By contrast, in flat-band systems where electrons are intrinsically localized owing to their vanishing group velocity, the role of disorder remains elusive. Twisted bilayer graphene (TBG) at the magic angle $\sim 1.1^\circ$ provides a representative flat-band platform to investigate this problem. Here, we perform an atomistic tight-binding quantum transport calculation on the interplay between disorder and flat-bands in TBG devices. This non-phenomenological approach provides direct evidence that moderate disorder enhances conductance, whereas stronger disorder restores localization, revealing a disorder-driven delocalization-to-localization transport behavior. The underlying physical mechanism is understood by an effective inter-moir{é} tunneling strength via spectral flow analysis of a disordered TBG cylinder. Moreover, by comparing magic-angle and large-angle TBG, we demonstrate qualitatively distinct disorder responses tied to the presence of flat-bands. Our quantitative results highlight the unconventional role of disorder in flat-band moir{é} materials and offer insights into the observation of the fractional quantum anomalous Hall effect in disordered moir{é} systems.

cond-mat.mes-hall↗

PAT-Agent: Autoformalization for Model Checking

Recent advances in large language models (LLMs) offer promising potential for automating formal methods. However, applying them to formal verification remains challenging due to the complexity of specification languages, the risk of hallucinated output, and the semantic gap between natural language and formal logic. We introduce PAT-Agent, an end-to-end framework for natural language autoformalization and formal model repair that combines the generative capabilities of LLMs with the rigor of formal verification to automate the construction of verifiable formal models. In PAT-Agent, a Planning LLM first extracts key modeling elements and generates a detailed plan using semantic prompts, which then guides a Code Generation LLM to synthesize syntactically correct and semantically faithful formal models. The resulting code is verified using the Process Analysis Toolkit (PAT) model checker against user-specified properties, and when discrepancies occur, a Repair Loop is triggered to iteratively correct the model using counterexamples. To improve flexibility, we built a web-based interface that enables users, particularly non-FM-experts, to describe, customize, and verify system behaviors through user-LLM interactions. Experimental results on 40 systems show that PAT-Agent consistently outperforms baselines, achieving high verification success with superior efficiency. The ablation studies confirm the importance of both planning and repair components, and the user study demonstrates that our interface is accessible and supports effective formal modeling, even for users with limited formal methods experience.

cs.SE↗

VeriFuzzy: A Dynamic Verifiable Fuzzy Search Service for Encrypted Cloud Data

Enabling search over encrypted cloud data is essential for privacy-preserving data outsourcing. While searchable encryption has evolved to support individual requirements like fuzzy matching, dynamic updates, and result verification, designing a service that supports dynamic, verifiable fuzzy search (DVFS) over encrypted cloud data remains a fundamental challenge due to inherent conflicts between underlying technologies. Existing approaches struggle with simultaneously achieving efficiency, functionality, and security, often forcing impractical trade-offs. This paper presents \textbf{VeriFuzzy}, a novel DVFS service framework that cohesively integrates three innovations: an \textit{Enhanced Virtual Binary Tree (EVBTree)} that decouples fuzzy semantics from index logic to support $O(\log n)$ search/updates; a \textit{blockchain-reconstructed verification} mechanism that ensures result integrity with logarithmic complexity; and a \textit{dual-repository state management} scheme that achieves IND-CKA2 security by neutralizing branch leakage. Extensive evaluation on 3,500+ documents shows VeriFuzzy achieves 41\% faster search, $5\times$ more efficient verification, and constant-time index updates compared to state-of-the-art alternatives. Our code and dataset are now open source, hoping to inspire future DVFS research.

cs.CR↗

Generically Automating Separation Logic by Functors, Homomorphisms and Modules

Foundational verification considers the functional correctness of programming languages with formalized semantics and uses proof assistants (e.g., Coq, Isabelle) to certify proofs. The need for verifying complex programs compels it to involve expressive Separation Logics (SLs) that exceed the scopes of well-studied automated proof theories, e.g., symbolic heap. Consequently, automation of SL in foundational verification relies heavily on ad-hoc heuristics that lack a systematic meta-theory and face scalability issues. To mitigate the gap, we propose a theory to specify SL predicates using abstract algebras including functors, homomorphisms, and modules over rings. Based on this theory, we develop a generic SL automation algorithm to reason about any data structures that can be characterized by these algebras. In addition, we also present algorithms for automatically instantiating the algebraic models to real data structures. The instantiation reuses the algebraic models of component structures and preserves their data abstractions. Case studies on formalized imperative semantics show our algorithm can instantiate the algebraic models automatically for a variety of complex data structures. Experimental results indicate the automatically instantiated reasoners from our generic theory show similar results to the state-of-the-art systems made of specifically crafted reasoning rules. The presented theories, proofs, and the verification framework are formalized in Isabelle/HOL.

cs.PL↗

Fermi energy sensitive universal conductance fluctuations in anisotropic materials

Universal conductance fluctuations (UCF) are a hallmark of quantum interference in mesoscopic devices. According to the Altshuler-Lee-Stone theory, the amplitude of UCF remains independent of system parameters such as Fermi energy and disorder strength. However, recent experiments have demonstrated a significant variation in UCF with respect to Fermi energy in the anisotropic Dirac semimetal $\mathrm{Cd_3As_2}$, suggesting a dependence on band anisotropy. In this work, we reconcile the discrepancy between theoretical predictions and experimental observations through a detailed study of UCF versus Fermi energy using a tight-binding model with tunable anisotropy parameters. Near the band edge, the Hamiltonian is simplified to an anisotropic free electron gas model, recovering the generalized Altshuler-Lee-Stone theory. However, as the Fermi energy shifts toward the band center, where rotational symmetry breaks into $C_4$ (four-fold rotational) symmetry, the UCF amplitude deviates from the standard theory. Our findings reveal that UCF becomes increasingly sensitive to Fermi energy as the anisotropy grows stronger. Furthermore, using realistic parameters for $\mathrm{Cd_3As_2}$, our calculations demonstrate an increase in UCF away from the Dirac point, in qualitative agreement with experimental results. The enhancement of UCF occurs in two perpendicular transport directions that we have calculated, albeit with quantitative differences in magnitude, which can be tested in future experiments. Given the prevalence of anisotropic materials and technical advances in engineering anisotropy through strain or twist, our results offer a valuable reference for characterizing intrinsic electronic properties via UCF.

cond-mat.mes-hall↗

Adaptive Plan-Execute Framework for Smart Contract Security Auditing

Large Language Models (LLMs) have shown great promise in code analysis and auditing; however, they still struggle with hallucinations and limited context-aware reasoning. We introduce SmartAuditFlow, a novel Plan-Execute framework that enhances smart contract security analysis through dynamic audit planning and structured execution. Unlike conventional LLM-based auditing approaches that follow fixed workflows and predefined steps, SmartAuditFlow dynamically generates and refines audit plans based on the unique characteristics of each smart contract. It continuously adjusts its auditing strategy in response to intermediate LLM outputs and newly detected vulnerabilities, ensuring a more adaptive and precise security assessment. The framework then executes these plans step by step, applying a structured reasoning process to enhance vulnerability detection accuracy while minimizing hallucinations and false positives. To further improve audit precision, SmartAuditFlow integrates iterative prompt optimization and external knowledge sources, such as static analysis tools and Retrieval-Augmented Generation (RAG). This ensures audit decisions are contextually informed and backed by real-world security knowledge, producing comprehensive security reports. Extensive evaluations across multiple benchmarks demonstrate that SmartAuditFlow outperforms existing methods, achieving 100 percent accuracy on common and critical vulnerabilities, 41.2 percent accuracy for comprehensive coverage of known smart contract weaknesses in real-world projects, and successfully identifying all 13 tested CVEs. These results highlight SmartAuditFlow's scalability, cost-effectiveness, and superior adaptability over traditional static analysis tools and contemporary LLM-based approaches, establishing it as a robust solution for automated smart contract auditing.

cs.CR↗

Clustering and analysis of user behaviour in blockchain: A case study of Planet IX

Decentralised applications (dApps) that run on public blockchains have the benefit of trustworthiness and transparency as every activity that happens on the blockchain can be publicly traced through the transaction data. However, this introduces a potential privacy problem as this data can be tracked and analysed, which can reveal user-behaviour information. A user behaviour analysis pipeline was proposed to present how this type of information can be extracted and analysed to identify separate behavioural clusters that can describe how users behave in the game. The pipeline starts with the collection of transaction data, involving smart contracts, that is collected from a blockchain-based game called Planet IX. Both the raw transaction information and the transaction events are considered in the data collection. From this data, separate game actions can be formed and those are leveraged to present how and when the users conducted their in-game activities in the form of user flows. An extended version of these user flows also presents how the Non-Fungible Tokens (NFTs) are being leveraged in the user actions. The latter is given as input for a Graph Neural Network (GNN) model to provide graph embeddings for these flows which then can be leveraged by clustering algorithms to cluster user behaviours into separate behavioural clusters. We benchmark and compare well-known clustering algorithms as a part of the proposed method. The user behaviour clusters were analysed and visualised in a graph format. It was found that behavioural information can be extracted regarding the users that belong to these clusters. Such information can be exploited by malicious users to their advantage. To demonstrate this, a privacy threat model was also presented based on the results that correspond to multiple potentially affected areas.

cs.LG↗

F$^3$Set: Towards Analyzing Fast, Frequent, and Fine-grained Events from Videos

Analyzing Fast, Frequent, and Fine-grained (F$^3$) events presents a significant challenge in video analytics and multi-modal LLMs. Current methods struggle to identify events that satisfy all the F$^3$ criteria with high accuracy due to challenges such as motion blur and subtle visual discrepancies. To advance research in video understanding, we introduce F$^3$Set, a benchmark that consists of video datasets for precise F$^3$ event detection. Datasets in F$^3$Set are characterized by their extensive scale and comprehensive detail, usually encompassing over 1,000 event types with precise timestamps and supporting multi-level granularity. Currently, F$^3$Set contains several sports datasets, and this framework may be extended to other applications as well. We evaluated popular temporal action understanding methods on F$^3$Set, revealing substantial challenges for existing techniques. Additionally, we propose a new method, F$^3$ED, for F$^3$ event detections, achieving superior performance. The dataset, model, and benchmark code are available at https://github.com/F3Set/F3Set.

cs.CV↗

The Fusion of Large Language Models and Formal Methods for Trustworthy AI Agents: A Roadmap

Large Language Models (LLMs) have emerged as a transformative AI paradigm, profoundly influencing daily life through their exceptional language understanding and contextual generation capabilities. Despite their remarkable performance, LLMs face a critical challenge: the propensity to produce unreliable outputs due to the inherent limitations of their learning-based nature. Formal methods (FMs), on the other hand, are a well-established computation paradigm that provides mathematically rigorous techniques for modeling, specifying, and verifying the correctness of systems. FMs have been extensively applied in mission-critical software engineering, embedded systems, and cybersecurity. However, the primary challenge impeding the deployment of FMs in real-world settings lies in their steep learning curves, the absence of user-friendly interfaces, and issues with efficiency and adaptability. This position paper outlines a roadmap for advancing the next generation of trustworthy AI systems by leveraging the mutual enhancement of LLMs and FMs. First, we illustrate how FMs, including reasoning and certification techniques, can help LLMs generate more reliable and formally certified outputs. Subsequently, we highlight how the advanced learning capabilities and adaptability of LLMs can significantly enhance the usability, efficiency, and scalability of existing FM tools. Finally, we show that unifying these two computation paradigms -- integrating the flexibility and intelligence of LLMs with the rigorous reasoning abilities of FMs -- has transformative potential for the development of trustworthy AI software systems. We acknowledge that this integration has the potential to enhance both the trustworthiness and efficiency of software engineering practices while fostering the development of intelligent FM tools capable of addressing complex yet real-world challenges.

cs.AI↗

LLM-SmartAudit: Advanced Smart Contract Vulnerability Detection

The immutable nature of blockchain technology, while revolutionary, introduces significant security challenges, particularly in smart contracts. These security issues can lead to substantial financial losses. Current tools and approaches often focus on specific types of vulnerabilities. However, a comprehensive tool capable of detecting a wide range of vulnerabilities with high accuracy is lacking. This paper introduces LLM-SmartAudit, a novel framework leveraging the advanced capabilities of Large Language Models (LLMs) to detect and analyze vulnerabilities in smart contracts. Using a multi-agent conversational approach, LLM-SmartAudit employs a collaborative system with specialized agents to enhance the audit process. To evaluate the effectiveness of LLM-SmartAudit, we compiled two distinct datasets: a labeled dataset for benchmarking against traditional tools and a real-world dataset for assessing practical applications. Experimental results indicate that our solution outperforms all traditional smart contract auditing tools, offering higher accuracy and greater efficiency. Furthermore, our framework can detect complex logic vulnerabilities that traditional tools have previously overlooked. Our findings demonstrate that leveraging LLM agents provides a highly effective method for automated smart contract auditing.

cs.CR↗

Cross-chain Sharing of Personal Health Records: Heterogeneous and Interoperable Blockchains

With the widespread adoption of medical informatics, a wealth of valuable personal health records (PHR) has been generated. Concurrently, blockchain technology has enhanced the security of medical institutions. However, these institutions often function as isolated data silos, limiting the potential value of PHRs. As the demand for data sharing between hospitals on different blockchains grows, addressing the challenge of cross-chain data sharing becomes crucial. When sharing PHRs across blockchains, the limited storage and computational capabilities of medical Internet of Things (IoT) devices complicate the storage of large volumes of PHRs and the handling of complex calculations. Additionally, varying blockchain cryptosystems and the risk of internal attacks further complicate the cross-chain sharing of PHRs. This paper proposes a scheme for sharing PHRs across heterogeneous and interoperable blockchains. Medical IoT devices can encrypt and store real-time PHRs in an InterPlanetary File System, requiring only simple operations for data sharing. An enhanced proxy re-encryption(PRE) algorithm addresses the differences in blockchain cryptosystems. Multi-dimensional analysis demonstrates that this scheme offers robust security and excellent performance.

cs.CR↗

Arrays of one-dimensional conducting channels in minimally twisted bilayer graphene

Minimally twisted bilayer graphene (TBG) with interlayer potential asymmetry host one-dimensional (1D) topological helical states (THSs) at domain walls between AB/BA stacking regions. However, the nature of THS propagation remains elusive. Although it is widely believed that they form a two-dimensional (2D) triangular network, a few argue that they self-organize into 1D topological zigzag modes (TZMs) that propagate independently. In this Letter, we propose a protocol based on a two-terminal TBG nanoflake transport device and resolve this issue. Through rigorous calculations on the differential conductance and the nonequilibrium local density of states, we show that, these THSs indeed self-construct the 1D distorted TZMs, each bypassing the AA-stacking spots and propagating independently. By considering a long TBG nanoflake, we obtain a nearly quantized conductance plateau with its value close to 1, 2, and 3 (in units of $2e^2/h$), which serves as a strong experimental sign for the existence of TZMs. Our work not only clarifies the propagation nature of the THSs, but also realizes an array of 1D conducting channels on a 2D platform. This work provides an unprecedented way to engineering topological states intrinsic in TBG.

cond-mat.mes-hall↗

Towards Large Language Model Aided Program Refinement

Program refinement involves correctness-preserving transformations from formal high-level specification statements into executable programs. Traditional verification tool support for program refinement is highly interactive and lacks automation. On the other hand, the emergence of large language models (LLMs) enables automatic code generations from informal natural language specifications. However, code generated by LLMs is often unreliable. Moreover, the opaque procedure from specification to code provided by LLM is an uncontrolled black box. We propose LLM4PR, a tool that combines formal program refinement techniques with informal LLM-based methods to (1) transform the specification to preconditions and postconditions, (2) automatically build prompts based on refinement calculus, (3) interact with LLM to generate code, and finally, (4) verify that the generated code satisfies the conditions of refinement calculus, thus guaranteeing the correctness of the code. We have implemented our tool using GPT4, Coq, and Coqhammer, and evaluated it on the HumanEval and EvalPlus datasets.

cs.SE↗

Quantized perfect transmission in graphene nanoribbons with random hollow adsorbates

Impurities exist inevitably in two-dimensional materials as they spontaneously adsorb onto the surface during fabrication, usually exerting detrimental effects on electronic transport. Here, we focus on a special type of impurities that preferentially adsorb onto the hollow regions of graphene nanoribbons (GNRs), and study how they affect the quantum transport in GNRs. Contrary to previous knowledge that random adatoms should localize electrons, the so-called Anderson localization, noteworthy quantized conductance peaks (QCPs) are observed at specific electron energies. These QCPs are remarkably robust against variations in system size, GNR edge, and adatom properties, and they can reappear at identical energies following an arithmetic sequence of device width. Further investigation of wavefunction reveals a unique transport mode at each QCP energy which transmits through disordered GNRs reflectionlessly, while all the others become fully Anderson localized, indicating the survival of quantum ballistic transport in the localized regime. Our findings highlight the potential utility of hollow adatoms as a powerful tool to manipulate the conductivity of GNRs, and deepen the understanding of the interplay between impurities and graphene.

cond-mat.mes-hall↗

A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Quantum Teleportation

Boolean satisfiability (SAT) solving is a fundamental problem in computer science. Finding efficient algorithms for SAT solving has broad implications in many areas of computer science and beyond. Quantum SAT solvers have been proposed in the literature based on Grover's algorithm. Although existing quantum SAT solvers can consider all possible inputs at once, they evaluate each clause in the formula one by one sequentially, making the time complexity O(m) -- linear to the number of clauses m -- per Grover iteration. In this work, we develop a parallel quantum SAT solver, which reduces the time complexity in each iteration from linear time O(m) to constant time O(1) by utilising extra entangled qubits. To further improve the scalability of our solution in case of extremely large problems, we develop a distributed version of the proposed parallel SAT solver based on quantum teleportation such that the total qubits required are shared and distributed among a set of quantum computers (nodes), and the quantum SAT solving is accomplished collaboratively by all the nodes. We have proved the correctness of our approaches and demonstrated them in simulations.

quant-ph↗

Moir{é} pattern assisted geometric resonant tunneling in disordered twisted bilayer graphene

We investigate the mesoscopic transport through a twisted bilayer graphene (TBG) consisting of a clean graphene nanoribbon on the bottom and a disordered graphene disc on the top. We show that, with strong top-layer disorder the transmission through such a device shows a sequence of resonant peaks with respect to the rotation angle $θ$, where at the resonance angles $θ_c$ the disc region contains one giant hexagonal moir{é} supercell. A further investigation shows that the value of $θ_c$ shows negligible dependence on the disorder strength, the Fermi energy, and the shape distortion, indicating the resonance is a robust geometric feature of the moir{é} supercell. We explain this geometric resonance based on the bound states formed inside the moir{é} supercell, with their averaged local density of states dominating at the AA stacking region while minimizing at the AB stacking region. By increasing the interlayer distance, the peak becomes less pronounced which further confirms the role of interlayer coupling. The results presented here suggest a new mechanism to tune the quantum transport signal through the twist angle in disordered moir{é} systems.

cond-mat.mes-hall↗