Publications (44)
Making Agents' Abilities Explicit
Yedi Zhang, Fu Song, Taolue Chen
Alternating-time temporal logics (ATL/ATL*) represent a family of modal logics for reasoning about agents' strategic abilities in multiagent systems (MAS). The interpretations of A…
Verification of Bit-Flip Attacks against Quantized Neural Networks
Yedi Zhang, Lei Huang, Pengfei Gao +3
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 amo…
Reasoning about Strategic Abilities in Stochastic Multi-agent Systems
Yedi Zhang, Fu Song, Taolue Chen +1
Reasoning about strategic abilities is key to AI systems comprising multiple agents, which provide a unified framework for formalizing various problems in game theory, social choic…
SimCert: Probabilistic Certification for Behavioral Similarity in Deep Neural Network Compression
Jingyang Li, Fu Song, Guoqiang Li
Deploying Deep Neural Networks (DNNs) on resource-constrained embedded systems requires aggressive model compression techniques like quantization and pruning. However, ensuring tha…
Can LLM Aid in Solving Constraints with Inductive Definitions?
Weizhi Feng, Shidong Shen, Jiaxiang Liu +3
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…
An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks
Ye Tao, Wanwei Liu, Fu Song +3
Deep neural networks, (DNNs, a.k.a. NNs), have been widely used in various tasks and have been proven to be successful. However, the accompanied expensive computing and storage cos…
KRust: A Formal Executable Semantics of Rust
Feng Wang, Fu Song, Min Zhang +2
Rust is a new and promising high-level system programming language. It provides both memory safety and thread safety through its novel mechanisms such as ownership, moves and borro…
Don't Complete It! Preventing Unhelpful Code Completion for Productive and Sustainable Neural Code Completion Systems
Zhensu Sun, Xiaoning Du, Fu Song +4
Currently, large pre-trained language models are widely applied in neural code completion systems. Though large code models significantly outperform their smaller counterparts, aro…
NCCR: to Evaluate the Robustness of Neural Networks and Adversarial Examples
Shi Pu, Fu Song, Wenjie Wang
Neural networks have received a lot of attention recently, and related security issues have come with it. Many studies have shown that neural networks are vulnerable to adversarial…
Attack as Defense: Characterizing Adversarial Examples using Robustness
Zhe Zhao, Guangke Chen, Jingyi Wang +3
As a new programming paradigm, deep learning has expanded its application to many real-world problems. At the same time, deep learning based software are found to be vulnerable to…
Who is Real Bob? Adversarial Attacks on Speaker Recognition Systems
Guangke Chen, Sen Chen, Lingling Fan +4
Speaker recognition (SR) is widely used in our daily life as a biometric authentication or identification mechanism. The popularity of SR brings in serious security concerns, as de…
AudioJailbreak: Jailbreak Attacks against End-to-End Large Audio-Language Models
Guangke Chen, Fu Song, Zhe Zhao +7
Jailbreak attacks to Large audio-language models (LALMs) are studied recently, but they exclusively focused on the attack scenario where the adversary can fully manipulate user pro…
QEBVerif: Quantization Error Bound Verification of Neural Networks
Yedi Zhang, Fu Song, Jun Sun
To alleviate the practical constraints for deploying deep neural networks (DNNs) on edge devices, quantization is widely regarded as one promising technique. It reduces the resourc…
CodeMark: Imperceptible Watermarking for Code Datasets against Neural Code Completion Models
Zhensu Sun, Xiaoning Du, Fu Song +1
Code datasets are of immense value for training neural-network-based code completion models, where companies or organizations have made substantial investments to establish and pro…
SEC4SR: A Security Analysis Platform for Speaker Recognition
Guangke Chen, Zhe Zhao, Fu Song +3
Adversarial attacks have been expanded to speaker recognition (SR). However, existing attacks are often assessed using different SR models, recognition tasks and datasets, and only…
SongBsAb: A Dual Prevention Approach against Singing Voice Conversion based Illegal Song Covers
Guangke Chen, Yedi Zhang, Fu Song +3
Singing voice conversion (SVC) automates song covers by converting a source singing voice from a source singer into a new singing voice with the same lyrics and melody as the sourc…
Counterexample Guided Branching via Directional Relaxation Analysis in Complete Neural Network Verification
Jingyang Li, Fu Song, Guoqiang Li
Deep Neural Networks demonstrate exceptional performance but remain vulnerable to adversarial perturbations, necessitating formal verification for safety-critical deployment. To ad…
SLMIA-SR: Speaker-Level Membership Inference Attacks against Speaker Recognition Systems
Guangke Chen, Yedi Zhang, Fu Song
Membership inference attacks allow adversaries to determine whether a particular example was contained in the model's training dataset. While previous works have confirmed the feas…
A Comprehensive Empirical Study of Bugs in Open-Source Federated Learning Frameworks
Weijie Shao, Yuyang Gao, Fu Song +3
Federated learning (FL) is a distributed machine learning (ML) paradigm, allowing multiple clients to collaboratively train shared machine learning (ML) models without exposing cli…
AS2T: Arbitrary Source-To-Target Adversarial Attack on Speaker Recognition Systems
Guangke Chen, Zhe Zhao, Fu Song +3
Recent work has illuminated the vulnerability of speaker recognition systems (SRSs) against adversarial attacks, raising significant security concerns in deploying SRSs. However, t…
SAT-based Formal Fault-Resistance Verification of Cryptographic Circuits
Huiyu Tan, Pengfei Gao, Taolue Chen +2
Fault injection attacks represent a type of active, physical attack against cryptographic circuits. Various countermeasures have been proposed to thwart such attacks, the design an…
Accelerating Robustness Verification of Deep Neural Networks Guided by Target Labels
Wenjie Wan, Zhaodi Zhang, Yiwei Zhu +2
Deep Neural Networks (DNNs) have become key components of many safety-critical applications such as autonomous driving and medical diagnosis. However, DNNs have been shown sufferin…
Advanced Evasion Attacks and Mitigations on Practical ML-Based Phishing Website Classifiers
Yusi Lei, Sen Chen, Lingling Fan +2
Machine learning (ML) based approaches have been the mainstream solution for anti-phishing detection. When they are deployed on the client-side, ML-based classifiers are vulnerable…
When Neural Code Completion Models Size up the Situation: Attaining Cheaper and Faster Completion through Dynamic Model Inference
Zhensu Sun, Xiaoning Du, Fu Song +2
Leveraging recent advancements in large language models, modern neural code completion models have demonstrated the capability to generate highly accurate code suggestions. However…
LTL Model-Checking for Dynamic Pushdown Networks Communicating via Locks
Fu Song, Tayssir Touili
A Dynamic Pushdown Network (DPN) is a set of pushdown systems (PDSs) where each process can dynamically create new instances of PDSs. DPNs are a natural model of multi-threaded pro…
Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks
Jiaxiang Liu, Yunhan Xing, Xiaomu Shi +3
As a new programming paradigm, deep neural networks (DNNs) have been increasingly deployed in practice, but the lack of robustness hinders their applications in safety-critical dom…
A Formally Verified Procedure for Width Inference in FIRRTL
Keyin Wang, Xiaomu Shi, Jiaxiang Liu +4
FIRRTL is an intermediate representation language for Register Transfer Level (RTL) hardware designs. In FIRRTL programs, the bit widths of many components are not specified explic…
Automated Verification of Correctness for Masked Arithmetic Programs
Mingyang Liu, Fu Song, Taolue Chen
Masking is a widely-used effective countermeasure against power side-channel attacks for implementing cryptographic algorithms. Surprisingly, few formal verification techniques hav…
FDI: Attack Neural Code Generation Systems through User Feedback Channel
Zhensu Sun, Xiaoning Du, Xiapu Luo +3
Neural code generation systems have recently attracted increasing attention to improve developer productivity and speed up software development. Typically, these systems maintain a…
LaserGuider: A Laser Based Physical Backdoor Attack against Deep Neural Networks
Yongjie Xu, Guangke Chen, Fu Song +1
Backdoor attacks embed hidden associations between triggers and targets in deep neural networks (DNNs), causing them to predict the target when a trigger is present while maintaini…
QFA2SR: Query-Free Adversarial Transfer Attacks to Speaker Recognition Systems
Guangke Chen, Yedi Zhang, Zhe Zhao +1
Current adversarial attacks against speaker recognition systems (SRSs) require either white-box access or heavy black-box queries to the target SRS, thus still falling behind pract…
Preventing Timing Side-Channels via Security-Aware Just-In-Time Compilation
Qi Qin, JulianAndres JiYang, Fu Song +2
Recent work has shown that Just-In-Time (JIT) compilation can introduce timing side-channels to constant-time programs, which would otherwise be a principled and effective means to…
Training Verification-Friendly Neural Networks via Neuron Behavior Consistency
Zongxin Liu, Zhe Zhao, Fu Song +4
Formal verification provides critical security assurances for neural networks, yet its practical application suffers from the long verification time. This work introduces a novel m…
Decision Procedure for A Theory of String Sequences
Denghang Hu, Taolue Chen, Philipp Rümmer +2
The theory of sequences, supported by many SMT solvers, can model program data types including bounded arrays and lists. Sequences are parameterized by the element data type and pr…
Taking Care of The Discretization Problem: A Comprehensive Study of the Discretization Problem and A Black-Box Adversarial Attack in Discrete Integer Domain
Lei Bu, Yuchao Duan, Fu Song +1
Numerous methods for crafting adversarial examples were proposed recently with high success rate. Since most existing machine learning based classifiers normalize images into some…
Model-based Automated Testing of JavaScript Web Applications via Longer Test Sequences
Pengfei Gao, Fu Song, Taolue Chen +2
JavaScript has become one of the most widely used languages for Web development. However, it is challenging to ensure the correctness and reliability of Web applications written in…
Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks
Pengfei Gao, Hongyi Xie, Jun Zhang +2
Power side-channel attacks, which can deduce secret data via statistical analysis, have become a serious threat. Masking is an effective countermeasure for reducing the statistical…
QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks
Yedi Zhang, Zhe Zhao, Fu Song +3
Deep learning has become a promising programming paradigm in software development, owing to its surprising performance in solving many challenging tasks. Deep neural networks (DNNs…
CoProtector: Protect Open-Source Code against Unauthorized Training Usage with Data Poisoning
Zhensu Sun, Xiaoning Du, Fu Song +2
Github Copilot, trained on billions of lines of public code, has recently become the buzzword in the computer science research and practice community. Although it is designed to he…
Towards Efficient Verification of Constant-Time Cryptographic Implementations
Luwei Cai, Fu Song, Taolue Chen
Timing side-channel attacks exploit secret-dependent execution time to fully or partially recover secrets of cryptographic implementations, posing a severe threat to software secur…
Optimal Circuit Synthesis of Linear Codes for Error Detection and Correction
Xi Yang, Taolue Chen, Yuqi Chen +3
Fault injection attacks deliberately inject faults into a device via physical channels to disturb its regular execution. Adversaries can effectively deduce secrets by analyzing bot…
A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs
Pengfei Gao, Hongyi Xie, Fu Song +1
Side-channel attacks, which are capable of breaking secrecy via side-channel information, pose a growing threat to the implementation of cryptographic algorithms. Masking is an eff…
Towards Understanding and Mitigating Audio Adversarial Examples for Speaker Recognition
Guangke Chen, Zhe Zhao, Fu Song +4
Speaker recognition systems (SRSs) have recently been shown to be vulnerable to adversarial attacks, raising significant security concerns. In this work, we systematically investig…
BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks
Yedi Zhang, Zhe Zhao, Guangke Chen +2
Verifying and explaining the behavior of neural networks is becoming increasingly important, especially when they are deployed in safety-critical applications. In this paper, we st…