Adversarial examples have become a critical focus in ensuring the security and robustness of deep learning (DL) systems. In this paper, we introduce an innovative approach for generating adversarial examples, designed to identify and diagnose common errors in DL models. Specifically, our method targets two key issues: Oscillating Loss (OL) and Slow Convergence (SC), providing valuable insight into model performance and fault detection. Using a reinforcement learning framework, we generate test data that effectively distinguishes between models with and without these errors. We consider the MNIST and CIFAR-10 datasets and test our approach on neural networks with various architectures, demonstrating significant improvements in error detection across different types of models. These results highlight the substantial effectiveness of our proposed method in improving the reliability of DL models. Furthermore, we demonstrate the scalability of our approach, showing that it can be used to diagnose various common errors in DL models with minimal modifications.

MedTiny is a multi-level, component-based modeling language designed for specifying software systems and provides support for arbitrary-depth automaton hierarchies.This paper presents the high-level operational semantics of MedTiny's core components-Function and Automaton-which enforce strict encapsulation.A port-and-link mechanism enables arbitrary-depth component composition in MedTiny, thereby enhancing model reusability.To demonstrate MedTiny's expressiveness, we establish a formal correspondence between MedTiny and labeled transition systems (LTS).From a model interaction perspective, we contrast MedTiny's port synchronization with the label synchronization, which inherently supports only two-level composition, typically employed in LTS-based models.

Large language models (LLMs) have demonstrated remarkable performance in various tasks, but they also face challenges in intellectual property (IP) protection. Traditional training-based watermarking techniques are computationally expensive, while function invariant transformations (FITs) offer a lightweight alternative. Nevertheless, FIT-based watermarking methods are vulnerable to adaptive attacks, where adversaries can exploit the same transformation to remove or forge watermarks. We propose a novel white-box watermarking scheme that combines error correction codes (ECCs) with weight permutations. By encoding model identifiers using ECCs, our approach guarantees reliable watermark extraction under various attacks. Additionally, we develop a linear assignment-based extraction algorithm to enhance its efficiency. Evaluations on six LLMs show that our method offers robust watermarking capabilities. It has a minimal impact on model performance while effectively defending against removal and forgery attacks. Overall, our approach provides a scalable and secure solution for safeguarding the copyrights of LLMs.

Federated learning (FL), as a powerful learning paradigm, trains a shared model by aggregating model updates from distributed clients. However, the decoupling of model learning from local data makes FL highly vulnerable to backdoor attacks, where a single compromised client can poison the shared model. While recent progress has been made in backdoor detection, existing methods face challenges with detection accuracy and runtime effectiveness, particularly when dealing with complex model architectures. In this work, we propose a novel approach to detecting malicious clients in an accurate, stable, and efficient manner. Our method utilizes a sampling-based network representation method to quantify dissimilarities between clients, identifying model deviations caused by backdoor injections. We also propose an iterative algorithm to progressively detect and exclude malicious clients as outliers based on these dissimilarity measurements. Evaluations across a range of benchmark tasks demonstrate that our approach outperforms state-of-the-art methods in detection accuracy and defense effectiveness. When deployed for runtime protection, our approach effectively eliminates backdoor injections with marginal overheads.

Model reuse techniques can reduce the resource requirements for training high-performance deep neural networks (DNNs) by leveraging existing models. However, unauthorized reuse and replication of DNNs can lead to copyright infringement and economic loss to the model owner. This underscores the need to analyze the reuse relation between DNNs and develop copyright protection techniques to safeguard intellectual property rights. Existing DNN copyright protection approaches suffer from several inherent limitations hindering their effectiveness in practical scenarios. For instance, existing white-box fingerprinting approaches cannot address the common heterogeneous reuse case where the model architecture is changed, and DNN fingerprinting approaches heavily rely on generating adversarial examples with good transferability, which is known to be challenging in the black-box setting. To bridge the gap, we propose a neuron functionality analysis-based reuse detector (NFARD), a neuron functionality (NF) analysis-based reuse detector, which only requires normal test samples to detect reuse relations by measuring the models' differences on a newly proposed model characterization, i.e., NF. A set of NF-based distance metrics is designed to make NFARD applicable to both white-box and black-box settings. Moreover, we devise a linear transformation method to handle heterogeneous reuse cases by constructing the optimal projection matrix for dimension consistency, significantly extending the application scope of NFARD. To the best of our knowledge, this is the first adversarial example-free method that exploits NF for DNN copyright protection. As a side contribution, we constructed a reuse detection benchmark named Reuse Zoo that covers various practical reuse techniques and popular datasets. Extensive evaluations on this comprehensive benchmark show that NFARD achieves $F1$ scores of 0.984 and 1.0 for detecting reuse relationships in black-box and white-box settings, respectively, while generating test suites $2{\sim } 99$ times faster than previous methods.

Since the rapid development of Large Language Models (LLMs) has achieved remarkable success, understanding and rectifying their internal complex mechanisms has become an urgent issue. Recent research has attempted to interpret their behaviors through the lens of inner representation. However, developing practical and efficient methods for applying these representations for general and flexible model editing remains challenging. In this work, we explore how to leverage insights from representation engineering to guide the editing of LLMs by deploying a representation discriminator as an editing oracle. We first identify the importance of a robust and reliable discriminator during editing, then propose an \textbf{A}dversarial \textbf{R}epresentation \textbf{E}ngineering (\textbf{ARE}) framework to provide a unified and interpretable approach for conceptual model editing without compromising baseline performance. Experiments on multiple tasks demonstrate the effectiveness of ARE in various model editing scenarios. Our code and data are available at \url{https://github.com/Zhang-Yihao/Adversarial-Representation-Engineering}.

Statistical model checking (SMC) is a simulation-based formal verification technique to deal with the scalability problem faced by traditional model checking. The main workflow of SMC is to perform iterative simulations. The number of simulations depends on users’ requirement for the verification results, which can be very large if users require a high level of confidence and precision. Therefore, how to perform as fewer simulations as possible while achieving the same level of confidence and precision is one of the core problems of SMC. In this paper, we consider the estimation problem of SMC. Most existing statistical model checkers use the Okamoto bound to decide the simulation number. Although the Okamoto bound is sound, it is well known to be overly conservative. The simulation number decided by the Okamoto bound is usually much higher than it actually needs, which leads to a waste of time and computation resources. To tackle this problem, we propose an efficient, sound and lightweight estimation algorithm using the Clopper-Pearson confidence interval. We perform comprehensive numerical experiments and case studies to evaluate the performance of our algorithm, and the results show that our algorithm uses 40%-60% fewer simulations than the Okamoto bound. Our algorithm can be directly integrated into existing model checkers to reduce the verification time of SMC estimation problems.

Since the discovery of adversarial examples, the local robustness of deep neural networks (DNNs) has received much attention. Moreover, researchers find that DNNs are also sensitive to semantic perturbations like fog, contrast and Gaussian noise. Due to the complexity of semantic perturbations, existing works only focus on local robustness towards some specific perturbations such as brightness and rotation. In this paper, we propose a statistics-based method to certify DNN’s local robustness towards general semantic perturbations. First, we give the formal definitions of semantic perturbations and local semantic robustness. Our definitions are general enough to cover almost all perturbations of concern. Then we develop a statistical certification algorithm. Our evaluations on CIFAR-10 and ImageNet show that compared with the state-of-the-art statistical certification algorithm, our method can provide the same theoretical guarantees using only 3.32%-6.55% of running time.

Measuring robustness of deep neural networks (DNNs) is an important topic for trustworthy AI. Existing methods for verifying local robustness of DNNs usually face the scalability problem and have difficulties to deal with non-linear activation functions and complex semantic perturbations. Existing methods for measuring global robustness usually rely on large datasets, so it is difficult for users without a large dataset to compare the global robustness of different networks. In this paper, we propose two algorithms to measure the local and global robustness of DNNs from the lens of statistical model checking. Compared with the local robustness estimation method using the Okamoto bound, our method can provide the same theoretical guarantee using only 48.6%-74.1% of running time. Our global robustness estimation algorithm can provide high-quality estimation using only 10 images for CIFAR-10 and 50 images for ImageNet, thus can be used in a wider range of scenarios.

While Feedforward Neural Networks (FNNs) have achieved remarkable success in various tasks, they are vulnerable to adversarial examples.Several techniques have been developed to verify the adversarial robustness of FNNs, but most of them focus on robustness verification against the local perturbation neighborhood of a single data point.There is still a large research gap in global robustness analysis.The global-robustness verifiable framework DeepGlobal has been proposed to identify all possible Adversarial Dangerous Regions (ADRs) of FNNs, not limited to data samples in a test set.In this paper, we propose a complete specification and implementation of DeepGlobal utilizing the SMT solver Z3 for more explicit definition, and propose several improvements to DeepGlobal for more efficient verification.To evaluate the effectiveness of our implementation and improvements, we conduct extensive experiments on a set of benchmark datasets.Visualization of our experiment results shows the validity and effectiveness of the approach.

Recurrent Neural Networks (RNNs) have demonstrated their effectiveness in learning and processing sequential data (e.g., speech and natural language). However, due to the black-box nature of neural networks, understanding the decision logic of RNNs is quite challenging. Some recent progress has been made to approximate the behavior of an RNN by weighted automata. They provide better interpretability, but still suffer from poor scalability. In this paper, we propose a novel approach to extracting weighted automata with the guidance of a target RNN's decision and context information. In particular, we identify the patterns of RNN's step-wise predictive decisions to instruct the formation of automata states. Further, we propose a state composition method to enhance the context-awareness of the extracted model. Our in-depth evaluations on typical RNN tasks, including language model and classification, demonstrate the effectiveness and advantage of our method over the state-of-the-arts. The evaluation results show that our method can achieve accurate approximation of an RNN even on large-scale tasks.

The wide deployment of Deep Neural Networks (DNNs), though achieving great success in many domains, has severe safety concerns. Inspired by testing criteria from traditional software engineering, various coverage criteria have been proposed to ensure the safety of DNNs. However, the validity of coverage criteria was questioned in related researches. In this paper, we evaluate the performance of dominating coverage criteria in two aspects: 1) distinguishing different qualities of test sets, 2) improving the safety and robustness of DNNs. The evaluation result confirms that coverage criteria are meaningful metrics for DNNs. Specifically, the way for improving robustness is contrary to the previous assumption: the higher coverage criterion score, the better. In addition, we propose a new coverage criterion called Independence Neuron Coverage (INC) which is finer grained to capture DNNs' subtle behaviour. Experiments show that INC is efficient and performs better than other evaluated coverage criteria in both aspects.

The Nervos CKB (Common Knowledge Base) is a public permissionless blockchain designed for a peer-to-peer crypto-economy network.The CKB Consensus Protocol is a key part of the Nervos CKB blockchain that improves the Consensus's performance limit of Bitcoin.In this paper, we develop a formal model of the CKB Consensus Protocol and verify some important properties of the protocol using the UPPAAL model checker.Based on the formal model, the reliability of CKB Consensus Protocol can be guaranteed.

Deep Learning (DL) offers a data-driven programming paradigm in which Deep Neural Networks (DNNs) can be constructed through a set of training data.It has been widely adopted in many real-world applications.However, many studies have shown that DL systems suffer from adversarial attacks, especially when they are applied to security-and safetycritical domains.Given that formal verification has proved a great success in many areas such as software engineering, using it to achieve a high-level security assurance in DL systems is considered promising.In this paper, we design and implement DeepAuto which makes the significant bridge between automata and DNNs.With the aid of DeepAuto, we demonstrate how DNNs can be modeled as automata and be verified formally in the widely used model checker UPPAAL.The potential usefulness of DeepAuto shows the connection between DNNs and automata and provides a solution for the construction of more trustworthy DL systems.

Quality assurance of rapidly evolving systems is increasingly important for their deployment to real-life applications.Despite the challenges posed by the increasing complexity of these systems, various techniques have been developed to check their correctness, such as theorem proving, which is a powerful formal verification method that can provide a complete guarantee.However, the proving process in the interactive theorem provers like Coq highly relies on human interactions, making the proving process difficult and time-consuming.To automate the proving process in Coq, we present a framework for predicting tactics in Coq by using Long Short Term Memory (LSTM).We take into account the effect of the dataset proof style on machine learning and create a new dataset following a specific proof style.We use the generated data to train an LSTM-based neural network that could give tactic predictions based on the proof context.This neural network reaches an accuracy of 58% if we only use the first predicted tactic and reaches an accuracy of 87% if we select the first three tactic suggestions, achieving a 15.2% and 12.8% improvement rate, respectively, compared to the methods in previous work.

As a quantum counterpart of labeled transition system (LTS), quantum labeled transition system (QLTS) is a powerful formalism for modeling quantum programs or protocols, and gives a categorical understanding for quantum computation. With the help of quantum branching monad, QLTS provides a framework extending some ideas in non-deterministic or probabilistic systems to quantum systems. On the other hand, quantum finite automata (QFA) emerged as a very elegant and simple model for resolving some quantum computational problems. In this paper, we propose the notion of reactive quantum system (RQS), a variant of QLTS capturing reactive system behavior, and develop a coalgebraic semantics for QLTS, RQS and QFA by an endofunctor on the category of convex sets, which has a final coalgebra. Such a coalgebraic semantics provides a unifying abstract interpretation for QLTS, RQS and QFA. The notions of bisimulation and simulation can be employed to compare the behavior of different types of quantum systems and judge whether a coalgebra can be behaviorally simulated by another.

Over the past decade, deep learning (DL) has been successfully applied to many industrial domain-specific tasks. However, the current state-of-the-art DL software still suffers from quality issues, which raises great concern especially in the context of safety- and security-critical scenarios. Adversarial examples (AEs) represent a typical and important type of defects needed to be urgently addressed, on which a DL software makes incorrect decisions. Such defects occur through either intentional attack or physical-world noise perceived by input sensors, potentially hindering further industry deployment. The intrinsic uncertainty nature of deep learning decisions can be a fundamental reason for its incorrect behavior. Although some testing, adversarial attack and defense techniques have been recently proposed, it still lacks a systematic study to uncover the relationship between AEs and DL uncertainty.

Given a family of independent and identically distributed samples extracted from the input region and their corresponding outputs, in this paper we propose a method to under-approximate the set of safe inputs that lead the black-box system to respect a given safety specification. Our method falls within the framework of probably approximately correct (PAC) learning. The computed under-approximation comes with statistical soundness provided by the underlying PAC learning process. Such a set, which we call a PAC under-approximation, is obtained by computing a PAC model of the black-box system with respect to the specified safety specification. In our method, the PAC model is computed based on the scenario approach, which encodes as a linear program. The linear program is constructed based on the given family of input samples and their corresponding outputs. The size of the linear program does not depend on the dimensions of the state space of the black-box system, thus providing scalability. Moreover, the linear program does not depend on the internal mechanism of the black-box system, thus being applicable to systems that existing methods are not capable of dealing with. Some case studies demonstrate these properties, general performance and usefulness of our approach.

Component-Based Software Engineering (CBSE) has played an important role in software industry for several decades.The Mediator language is proposed to formally model complex hierarchical component-based systems, which provides a proper automata-based formalism for specifying both high-level system layouts and low-level behavior units.In this paper, we develop a framework for translating Mediator models into the model checker PRISM, and build such a "translator" which can generate PRISM codes from Mediator models automatically and cooperates with PRISM to verify properties of Mediator models.

Distributed systems have been widely used in various domains. However, the concurrent and asynchronous nature makes their safety and reliability hard to guarantee, especially in the design phase. In this paper, we extend Mediator and its semantics to capture the inherent real-time and asynchronous behavior in distributed systems. As a component-based language, Mediator provides a compositional modeling framework and corresponding precise formal semantics, making it able to reuse reliable components in different contexts.

Formal modeling and verification of component connectors in complex software systems are getting more interests with recent advancements and evolution in modern software techniques. Various properties of connectors can be specified as high-order logic propositions and verified using theorem proving techniques. However, most high-order logic provers still highly rely on human interactions and thus make the proving process difficult and time-consuming. In this paper, we propose an approach based on recurrent neural networks (RNNs) to predict the correct tactics in the proving process. Recurrent layers consisting of Long-Short-Term-Memory (LSTM) units provide a better correctness rate comparing with simple RNN units. Under this framework, properties of connectors can be naturally formalized and semi-automatically proved in Coq.

IEEE 802.11i is the IEEE standard that provides enhanced MAC security and has been widely used in wireless networks and Internet of Things.It improves IEEE 802.11(1999) by providing a Robust Security Network (RSN) with two new protocols: the 4-way handshake and the Group-key handshake.These protocols utilize the authentication services and port access control described in IEEE 802.1X to establish and change the appropriate cryptographic keys.In this paper, we carry out a formal modeling and verification approach based on timed automata for IEEE 802.11i protocol, using the UPPAAL model checker, to check correctness of the changes in IEEE 802.11i protocol and provide better security.

Compositional coordination models such as Reo provide powerful support for the development of large-scale distributed systems by allowing construction of complex connectors that coordinate behavior among different components.The reliability of such distributed systems highly depends on the correctness of connectors.In this paper, we use the proof assistant PVS for formal modeling, analysis and verification of component connectors.We first present the modeling of primitive channels and the composition operators that are used to combine channels for building complex connectors.Furthermore, we show how to model and analyze connector's behavior in PVS and prove some interesting connector properties.The model reflects the original topological structure of connectors simply and clearly.With the provided approach, different kinds of connector properties can be naturally formalized and proved in PVS.

The coordination language Reo has played an important role in organizing the interactions among different components in large-scale distributed applications.A probabilistic extension on classical Reo is necessary to deal with the uncertainty of the real world.In this paper we developed a framework in Coq for formalizing probabilistic connectors and reasoning about their probabilistic properties.Different types of probabilistic channels are characterized by the relations on their input and output timed data distribution streams.More complex probabilistic connectors can be further constructed based on the probabilistic channels and composition operators.Within such a framework, properties under analysis and refinement / equivalence relations between probabilistic connectors can be naturally established as theorems and proved using tactics in Coq.

IEEE 802.11i is the IEEE standard that provides enhanced MAC security and has been widely used in wireless networks and Internet of Things. It improves IEEE 802.11 (1999) by providing a Robust Security Network (RSN) with two new protocols: the Four-Way Handshake and the Group Key Handshake. These protocols utilize the authentication services and port access control described in IEEE 802.1X to establish and change the appropriate cryptographic keys. In this paper, we carry out a formal modeling and verification approach based on timed automata for IEEE 802.11i protocol, using the UPPAAL model checker, to check correctness of the changes in IEEE 802.11i protocol and provide better security.

Nowadays, protocols often use time to provide better security. For instance, critical credentials are often associated with expiry dates in system designs. However, using time correctly in protocol design is challenging, due to the lack of time related formal specification and verification techniques. Thus, we propose a comprehensive analysis framework to formally specify as well as automatically verify timed security protocols. A parameterized method is introduced in our framework to handle timing parameters whose values cannot be decided in the protocol design stage. In this work, we first propose timed applied p-calculus as a formal language for specifying timed security protocols. It supports modeling of continuous time as well as application of cryptographic functions. Then, we define its formal semantics based on timed logic rules, which facilitates efficient verification against various authentication and secrecy properties. Given a parameterized security protocol, our method either produces a constraint on the timing parameters which guarantees the security property satisfied by the protocol, or reports an attack that works for any parameter value. The correctness of our verification algorithm has been formally proved. We evaluate our framework with multiple timed and untimed security protocols and successfully find a previously unknown timing attack in Kerberos V.

Coordination models and languages play a key role in formally specifying the communication and interaction among different components in large-scale concurrent systems. In this paper, we use active learning to extract timed connector models from black-box system implementations. Firstly, parameterized Mealy machine (PMM) is introduced as an operational semantic model for channel-based coordination language Reo. With product and link operators defined, we can construct complex connectors by joining basic ones in form of PMM. Moreover, with a concretize mapping function, PMMs can be easily transformed into Mealy machines, and the latter can be extracted by an optimized L* algorithm.

Coordination is playing a key role in complex cyber-physicalsystems (CPSs). The complexity and importance of coordination models and languages for CPSs necessarily lead to a higher relevance of testing during development of CPSs. Model-based testing is a promising technology to test the conformance or non-conformance relation between the implementation-under-test (IUT) and its specification. In this paper, we present an approach to test the conformance relation tiococ(Timed Input-Output Conformance) between the implementation of a timed Reo connector and its specification given by a timed constraint automaton (TCA). An algorithm to generate test cases from a TCA is proposed and the testing approach is implemented in UPPAAL.