arXiv subjects

Shang-Wei Lin

Publications and source records attributed to Shang-Wei Lin.

At least 19 recordsLinked to original sources

arXiv2026

DeepFWI: Identifying Bug-Sensitive Warnings with Multi-Modal Code-Warning Semantics

Static analysis tools have evolved over time to assist in detecting bugs. However, the excessive false warnings can impede developers' productivity and confidence in the tools. Previous research efforts have explored learning-based approaches to identify bug warnings. Nevertheless, their coarse granularity, focusing on either long-term warnings or function-level alerts, is insensitive to individual bugs. Also, they rely on manually crafted features or solely on source code semantics, which is inadequate for effective learning. In this paper, we propose DeepFWI, a learning-based approach that identifies bug-sensitive warnings at a fine-grained granularity. Specifically, we design a novel LSTM-based model that captures multi-modal semantics of source code and warnings from automated static analysis tools (ASATs) and highlights their correlations with cross-attention. To tackle the data scarcity of training and evaluation, we collected a large-scale dataset of 280,273 warnings. We conducted extensive experiments on the dataset to evaluate DeepFWI. The experimental results demonstrate the effectiveness of our approach, with an F1-score 67.06% for confirming true warnings in a finer-grained manner, significantly outperforming all baselines. Additionally, to validate the practicality of DeepFWI from the perspective of developers, we applied DeepFWI to four popular open-source projects. Our approach filtered out the vast majority of warnings, while still successfully surfacing 25 true bug-related warnings that were confirmed through manual analysis.

cs.SE↗

arXiv2026

Quantangle-SAT: A Quantum SAT Solver Based on Entanglement and Equivalence Checking

Satisfiability (SAT) is a central problem in computer science, and advances in SAT-solving algorithms have a far-reaching impact across many fields. Recent works have proposed quantum SAT solvers based on Grover's algorithm, a quantum search technique. However, Grover-based approaches face a key limitation: they typically require prior knowledge of the number of satisfying assignments of the target Boolean formula. This information is unavailable in most practical settings. Quantum counting can be used to estimate this quantity, but it incurs a computational overhead that is several orders of magnitude higher than Grover search. In this paper, we propose a novel quantum SAT solver based on entanglement and equivalence checking. Our method does not assume prior knowledge of the number of solutions and is computationally more efficient than quantum counting. Although the worst case time complexity is inevitably exponential, we prove that the expected time complexity of our approach is only constant time O(1) over random Boolean functions. Experimental results also support our theoretical claim.

quant-ph↗

arXiv2026

A Modular and T-Gate Efficient Architecture for Quantum Leading-Zero/One Counter

The Quantum Leading-Zero/One Counter (QLZOC) is a fundamental component in quantum arithmetic, playing a critical role in normalization, floating-point units, dynamic range scaling, and logarithmic approximations. Conventional designs primarily rely on direct Boolean-to-quantum mapping, which results in inefficient resource utilization such as irregular gate growth and width-dependent resource overhead. In this work, we propose a scalable, modular, and resource efficient architecture for QLZOC by reformulating the counting process into a sequence of systematic conditional bit-flip operations. Moreover, our design achieves functional polymorphism so that the same design can be easily toggled between zero and one detection, while ensuring seamless scalability to any bit-width without manual re-tuning. We further introduce a Parallel QLZOC (PQLZOC) variant and a Fan-Out optimized (FO-PQLZOC) design. In this work, we evaluate resource efficiency based on the classic criteria about T gates, including the number of total T gates being used (T-count) and the number of sequential T gate layers (T-depth). By exploiting the properties of all-zero/one qubit blocks and a hierarchical merge strategy, the proposed FO-PQLZOC reduces the T-depth from O(m) to O(log m), where m is the input size. Comparative analysis demonstrates that our optimized architecture achieves a 40% reduction in T-count and a 60% reduction in T-depth over state-of-the-art designs, providing a high-performance, T-gate efficient solution for general-purpose quantum arithmetic processors.

quant-ph↗

arXiv2025

SOSAE: Self-Organizing Sparse AutoEncoder

The process of tuning the size of the hidden layers for autoencoders has the benefit of providing optimally compressed representations for the input data. However, such hyper-parameter tuning process would take a lot of computation and time effort with grid search as the default option. In this paper, we introduce the Self-Organization Regularization for Autoencoders that dynamically adapts the dimensionality of the feature space to the optimal size. Inspired by physics concepts, Self-Organizing Sparse AutoEncoder (SOSAE) induces sparsity in feature space in a structured way that permits the truncation of the non-active part of the feature vector without any loss of information. This is done by penalizing the autoencoder based on the magnitude and the positional index of the feature vector dimensions, which during training constricts the feature space in both terms. Extensive experiments on various datasets show that our SOSAE can tune the feature space dimensionality up to 130 times lesser Floating-point Operations (FLOPs) than other baselines while maintaining the same quality of tuning and performance.

cs.LG↗

arXiv2025

Towards Universal & Efficient Model Compression via Exponential Torque Pruning

The rapid growth in complexity and size of modern deep neural networks (DNNs) has increased challenges related to computational costs and memory usage, spurring a growing interest in efficient model compression techniques. Previous state-of-the-art approach proposes using a Torque-inspired regularization which forces the weights of neural modules around a selected pivot point. Whereas, we observe that the pruning effect of this approach is far from perfect, as the post-trained network is still dense and also suffers from high accuracy drop. In this work, we attribute such ineffectiveness to the default linear force application scheme, which imposes inappropriate force on neural module of different distances. To efficiently prune the redundant and distant modules while retaining those that are close and necessary for effective inference, in this work, we propose Exponential Torque Pruning (ETP), which adopts an exponential force application scheme for regularization. Experimental results on a broad range of domains demonstrate that, though being extremely simple, ETP manages to achieve significantly higher compression rate than the previous state-of-the-art pruning strategies with negligible accuracy drop.

cs.CV↗

arXiv2025

Towards Calibration Enhanced Network by Inverse Adversarial Attack

Test automation has become increasingly important as the complexity of both design and content in Human Machine Interface (HMI) software continues to grow. Current standard practice uses Optical Character Recognition (OCR) techniques to automatically extract textual information from HMI screens for validation. At present, one of the key challenges faced during the automation of HMI screen validation is the noise handling for the OCR models. In this paper, we propose to utilize adversarial training techniques to enhance OCR models in HMI testing scenarios. More specifically, we design a new adversarial attack objective for OCR models to discover the decision boundaries in the context of HMI testing. We then adopt adversarial training to optimize the decision boundaries towards a more robust and accurate OCR model. In addition, we also built an HMI screen dataset based on real-world requirements and applied multiple types of perturbation onto the clean HMI dataset to provide a more complete coverage for the potential scenarios. We conduct experiments to demonstrate how using adversarial training techniques yields more robust OCR models against various kinds of noises, while still maintaining high OCR model accuracy. Further experiments even demonstrate that the adversarial training models exhibit a certain degree of robustness against perturbations from other patterns.

cs.CV↗

arXiv2024

Adversarial Exposure Attack on Diabetic Retinopathy Imagery Grading

Diabetic Retinopathy (DR) is a leading cause of vision loss around the world. To help diagnose it, numerous cutting-edge works have built powerful deep neural networks (DNNs) to automatically grade DR via retinal fundus images (RFIs). However, RFIs are commonly affected by camera exposure issues that may lead to incorrect grades. The mis-graded results can potentially pose high risks to an aggravation of the condition. In this paper, we study this problem from the viewpoint of adversarial attacks. We identify and introduce a novel solution to an entirely new task, termed as adversarial exposure attack, which is able to produce natural exposure images and mislead the state-of-the-art DNNs. We validate our proposed method on a real-world public DR dataset with three DNNs, e.g., ResNet50, MobileNet, and EfficientNet, demonstrating that our method achieves high image quality and success rate in transferring the attacks. Our method reveals the potential threats to DNN-based automatic DR grading and would benefit the development of exposure-robust DR grading methods in the future.

cs.CV↗

arXiv2023

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↗

arXiv2023

A Quantum SMT Solver for Bit-Vector Theory

Given a formula $F$ of satisfiability modulo theory (SMT), the classical SMT solver tries to (1) abstract $F$ as a Boolean formula $F_B$, (2) find a Boolean solution to $F_B$, and (3) check whether the Boolean solution is consistent with the theory. Steps~{(2)} and (3) may need to be performed back and forth until a consistent solution is found. In this work, we develop a quantum SMT solver for the bit-vector theory. With the characteristic of superposition in quantum system, our solver is able to consider all the inputs simultaneously and check their consistency between Boolean and the theory domains in one shot.

cs.LO↗

arXiv2022

Enhancing Security Patch Identification by Capturing Structures in Commits

With the rapid increasing number of open source software (OSS), the majority of the software vulnerabilities in the open source components are fixed silently, which leads to the deployed software that integrated them being unable to get a timely update. Hence, it is critical to design a security patch identification system to ensure the security of the utilized software. However, most of the existing works for security patch identification just consider the changed code and the commit message of a commit as a flat sequence of tokens with simple neural networks to learn its semantics, while the structure information is ignored. To address these limitations, in this paper, we propose our well-designed approach E-SPI, which extracts the structure information hidden in a commit for effective identification. Specifically, it consists of the code change encoder to extract the syntactic of the changed code with the BiLSTM to learn the code representation and the message encoder to construct the dependency graph for the commit message with the graph neural network (GNN) to learn the message representation. We further enhance the code change encoder by embedding contextual information related to the changed code. To demonstrate the effectiveness of our approach, we conduct the extensive experiments against six state-of-the-art approaches on the existing dataset and from the real deployment environment. The experimental results confirm that our approach can significantly outperform current state-of-the-art baselines.

cs.CR↗

arXiv2021

Pasadena: Perceptually Aware and Stealthy Adversarial Denoise Attack

Image denoising can remove natural noise that widely exists in images captured by multimedia devices due to low-quality imaging sensors, unstable image transmission processes, or low light conditions. Recent works also find that image denoising benefits the high-level vision tasks, e.g., image classification. In this work, we try to challenge this common sense and explore a totally new problem, i.e., whether the image denoising can be given the capability of fooling the state-of-the-art deep neural networks (DNNs) while enhancing the image quality. To this end, we initiate the very first attempt to study this problem from the perspective of adversarial attack and propose the adversarial denoise attack. More specifically, our main contributions are three-fold: First, we identify a new task that stealthily embeds attacks inside the image denoising module widely deployed in multimedia devices as an image post-processing operation to simultaneously enhance the visual image quality and fool DNNs. Second, we formulate this new task as a kernel prediction problem for image filtering and propose the adversarial-denoising kernel prediction that can produce adversarial-noiseless kernels for effective denoising and adversarial attacking simultaneously. Third, we implement an adaptive perceptual region localization to identify semantic-related vulnerability regions with which the attack can be more effective while not doing too much harm to the denoising. We name the proposed method as Pasadena (Perceptually Aware and Stealthy Adversarial DENoise Attack) and validate our method on the NeurIPS'17 adversarial competition dataset, CVPR2021-AIC-VI: unrestricted adversarial attacks on ImageNet,etc. The comprehensive evaluation and analysis demonstrate that our method not only realizes denoising but also achieves a significantly higher success rate and transferability over state-of-the-art attacks.

cs.CV↗

arXiv2021

A Survey of Smart Contract Formal Specification and Verification

A smart contract is a computer program which allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain, finance, legal and medical services, there is a strong demand for verification and validation techniques. Yet, the vast majority of smart contracts lack any kind of formal specification, which is essential for establishing their correctness. In this survey, we investigate formal models and specifications of smart contracts presented in the literature and present a systematic overview in order to understand the common trends. We also discuss the current approaches used in verifying such property specifications and identify gaps with the hope to recognize promising directions for future work.

cs.SE↗

arXiv2021

Formal Analysis of Composable DeFi Protocols

Decentralized finance (DeFi) has become one of the most successful applications of blockchain and smart contracts. The DeFi ecosystem enables a wide range of crypto-financial activities, while the underlying smart contracts often contain bugs, with many vulnerabilities arising from the unforeseen consequences of composing DeFi protocols together. In this paper, we propose a formal process-algebraic technique that models DeFi protocols in a compositional manner to allow for efficient property verification. We also conduct a case study to demonstrate the proposed approach in analyzing the composition of two interacting DeFi protocols, namely, Curve and Compound. Finally, we discuss how the proposed modeling and verification approach can be used to analyze financial and security properties of interest.

cs.CR↗

arXiv2020

SeqMobile: A Sequence Based Efficient Android Malware Detection System Using RNN on Mobile Devices

With the proliferation of Android malware, the demand for an effective and efficient malware detection system is on the rise. The existing device-end learning based solutions tend to extract limited syntax features (e.g., permissions and API calls) to meet a certain time constraint of mobile devices. However, syntax features lack the semantics which can represent the potential malicious behaviors and further result in more robust model with high accuracy for malware detection. In this paper, we propose an efficient Android malware detection system, named SeqMobile, which adopts behavior-based sequence features and leverages customized deep neural networks on mobile devices instead of the server. Different from the traditional sequence-based approaches on server, to meet the performance demand, SeqMobile accepts three effective performance optimization methods to reduce the time cost. To evaluate the effectiveness and efficiency of our system, we conduct experiments from the following aspects 1) the detection accuracy of different recurrent neural networks; 2) the feature extraction performance on different mobile devices, 3) the detection accuracy and prediction time cost of different sequence lengths. The results unveil that SeqMobile can effectively detect malware with high accuracy. Moreover, our performance optimization methods have proven to improve the performance of training and prediction by at least twofold. Additionally, to discover the potential performance optimization from the SOTA TensorFlow model optimization toolkit for our approach, we also provide an evaluation on the toolkit, which can serve as a guidance for other systems leveraging on sequence-based learning approach. Overall, we conclude that our sequence-based approach, together with our performance optimization methods, enable us to detect malware under the performance demands of mobile devices.

cs.CR↗

arXiv2020

A Performance-Sensitive Malware Detection System Using Deep Learning on Mobile Devices

Currently, Android malware detection is mostly performed on server side against the increasing number of malware. Powerful computing resource provides more exhaustive protection for app markets than maintaining detection by a single user. However, apart from the applications provided by the official market, apps from unofficial markets and third-party resources are always causing serious security threats to end-users. Meanwhile, it is a time-consuming task if the app is downloaded first and then uploaded to the server side for detection, because the network transmission has a lot of overhead. In addition, the uploading process also suffers from the security threats of attackers. Consequently, a last line of defense on mobile devices is necessary and much-needed. In this paper, we propose an effective Android malware detection system, MobiTive, leveraging customized deep neural networks to provide a real-time and responsive detection environment on mobile devices. MobiTive is a preinstalled solution rather than an app scanning and monitoring engine using after installation, which is more practical and secure. Original deep learning models cannot be directly deployed and executed on mobile devices due to various performance limitations, such as computation power, memory size, and energy. Therefore, we evaluate and investigate the following key points:(1) the performance of different feature extraction methods based on source code or binary code;(2) the performance of different feature type selections for deep learning on mobile devices;(3) the detection accuracy of different deep neural networks on mobile devices;(4) the real-time detection performance and accuracy on different mobile devices;(5) the potential based on the evolution trend of mobile devices' specifications; and finally we further propose a practical solution (MobiTive) to detect Android malware on mobile devices.

cs.CR↗

arXiv2020

An Executable Operational Semantics for Rust with the Formalization of Ownership and Borrowing

Rust is an emergent systems programming language highlighting memory safety by its Ownership and Borrowing System (OBS). The existing formal semantics for Rust only covers limited subsets of the major language features of Rust. Moreover, they formalize OBS as type systems at the language-level, which can only be used to conservatively analyze programs against the OBS invariants at compile-time. That is, they are not executable, and thus cannot be used for automated verification of runtime behavior. In this paper, we propose RustSEM, a new executable operational semantics for Rust. RustSEM covers a much larger subset of the major language features than existing semantics. Moreover, RustSEM provides an operational semantics for OBS at the memory-level, which can be used to verify the runtime behavior of Rust programs against the OBS invariants. We have implemented RustSEM in the executable semantics modeling tool K-Framework. We have evaluated the semantics correctness of RustSEM wrt. the Rust compiler using around 700 tests. In particular, we have proposed a new technique for testing semantic consistency to ensure the absence of semantic ambiguities on all possible execution selections. We have also evaluated the potential applications of RustSEM in automated runtime and formal verification for both functional and memory properties. Experimental results show that RustSEM can enhance the memory safety mechanism of Rust, as it is more powerful than OBS in detecting memory errors.

cs.PL↗

arXiv2019

Oracle-Supported Dynamic Exploit Generation for Smart Contracts

Despite the high stakes involved in smart contracts, they are often developed in an undisciplined manner, leaving the security and reliability of blockchain transactions at risk. In this paper, we introduce ContraMaster: an oracle-supported dynamic exploit generation framework for smart contracts. Existing approaches mutate only single transactions; ContraMaster exceeds these by mutating the transaction sequences. ContraMaster uses data-flow, control-flow, and the dynamic contract state to guide its mutations. It then monitors the executions of target contract programs, and validates the results against a general-purpose semantic test oracle to discover vulnerabilities. Being a dynamic technique, it guarantees that each discovered vulnerability is a violation of the test oracle and is able to generate the attack script to exploit this vulnerability. In contrast to rule-based approaches, ContraMaster has not shown any false positives, and it easily generalizes to unknown types of vulnerabilities (e.g., logic errors). We evaluate ContraMaster on 218 vulnerable smart contracts. The experimental results confirm its practical applicability and advantages over the state-of-the-art techniques, and also reveal three new types of attacks.

cs.CR↗

arXiv2018

The language preservation problem is undecidable for parametric event-recording automata

Parametric timed automata (PTA) extend timed automata with unknown constants ("parameters"), at the price of undecidability of most interesting problems. The (untimed) language preservation problem ("given a parameter valuation, can we find at least one other valuation with the same untimed language?") is undecidable for PTAs. We prove that this problem remains undecidable for parametric event-recording automata (PERAs), a subclass of PTAs that considerably restrains the way the language can be used; we also show it remains undecidable even for slightly different definitions of the language, i.e., finite sequences of actions ending in or passing infinitely often through accepting locations, or just all finite untimed words (without accepting locations).

cs.FL↗