Abstract:In DevOps continuous integration practices, the high-frequency code iteration of Web applications poses significant challenges to traditional static analysis tools: full analysis techniques cause computational resource waste and delays, while existing incremental analysis techniques struggle to meet practical requirements due to limitations in detecting diverse vulnerabilities and inherent trade-offs between accuracy, efficiency, and consistency. To address these challenges, this study proposes AWTaint, an incremental static analysis framework for Web application vulnerability detection. The framework features field-, context-, and flow-sensitivity, leveraging function summaries to characterize relationships between input and output variables, generating taint propagation information associated with various detection rules. A fine-grained incremental computation approach is adopted in this framework: first, a conservative incremental change scope is estimated through call graph analysis, and then function summary changes are utilized to determine impact ranges. This effectively satisfies the three core requirements of industrial Web application vulnerability detection: precision, efficiency, and consistency. Experimental results on a dataset containing 10 real-world Java Web applications demonstrate that AWTaint supports multiple Web application vulnerability detection requirements. Compared to full analysis, its incremental analysis achieves an average speedup of 3.63×, with memory peak kept within 8 GB, while maintaining complete consistency in vulnerability detection results. This framework provides an engineering solution for shift-left security practices, significantly optimizing resource utilization and development iteration efficiency without compromising detection accuracy.

Abstract:Traditional program analysis methods, when dealing with large-scale software, often require explicit construction of dependency graphs (such as system dependency graphs and program dependency graphs). However, as the number of program entities and dependency relationships grows exponentially with the scale of software, these methods face performance bottlenecks of “graph construction difficulty” and redundant computation. To address this challenge, this study proposes a parallel program analysis framework based on on-demand slicing computation. The framework integrates symbolic slicing and higher-order function summary techniques, and its core ideas are as follows. (1) By abstracting the impact of function calls into reusable higher-order function summaries and replacing explicit dependency graph storage and traversal with dynamic function evaluation, the graph construction bottleneck is fundamentally avoided. (2) An on-demand instantiation mechanism for higher-order function summaries is designed, which dynamically and lazily instantiates summaries based on user-specified slicing criteria (e.g., key variables), computing only dependencies directly relevant to the analysis target, thereby significantly reducing computational redundancy. Through the independence of sub-analysis summaries and the lazy instantiation feature, this framework enables fine-grained task partitioning, demonstrating good parallelization potential. Experimental results show that the on-demand slicing computation under this framework reduces analysis time by 65.3% and peak memory usage by 68.2% compared to the symbolic slicing tool SymPas. Its parallel version (6 threads) further reduces analysis time by 93.8%, with parallel efficiency approaching 90%. To verify the practicality and effectiveness of the framework in large-scale program analysis, it is applied to out-of-bounds access defect detection, successfully identifying 132 true positive instances, providing a new formal solution for addressing performance bottlenecks in large-scale software analysis.

Abstract:Formalized mathematics represents a revolution in mathematics. The combination of theorem provers with machine verification of mathematical theorems establishes not only a new standard for mathematical rigor but also a novel approach to developing mathematics. As mathematical challenges worldwide are increasingly solved with computer assistance and various formalization projects are launched by experts, the influence of formalized mathematics continues to grow. It generated significant impact across both the mathematical and computer science communities. This study introduces a formal system for mathematical analysis based on the Coq theorem prover. The formalization is guided by the textbook Mathematical Analysis compiled by the School of Mathematical Sciences at East China Normal University. Developed within the framework of naive set theory and elementary number theory and algebra, the system has formalized the content related to single-variable calculus from the first volume of the textbook. It includes topics such as real numbers and functions, sequence limits, function limits, continuity of functions, derivatives and differentials, indefinite integrals, and definite integrals. The proposed system strictly corresponds to the textbook content, where all theorems are provided with machine-verifiable Coq proofs. The entire formalization is verified by Coq and executed successfully on a computer. Readers can learn mathematics by following the code and can also understand the code by comparing it with the mathematics, which demonstrates the readability, interactivity, and intelligence of Coq-based machine theorem proving. It represents an attempt to enable readers to follow the computer in learning, understanding, constructing, educating, and even developing modern mathematics, thereby enhancing their ability to understand, experience, and appreciate mathematics.

Abstract:Compared with original microkernels, L4 greatly improves performance and flexibility and is widely used in various fields. The correctness and reliability of the operating system kernel play a decisive role in the stable operation of the system. This study presents formal specifications and verification for thread management, a key mechanism of L4. First, a safety specification is developed to describe safety properties, a standard L4 API specification is reused to define functional correctness, and an implementation specification based on the C++ source code is automatically generated. To alleviate the significant differences between the requirement specification and the implementation specification, an intermediate specification is introduced. The first two specifications are formalized in Isabelle/HOL, and the latter two are expressed in Python. The consistency among these specifications is guaranteed through refinement proofs, such as interpretation and the establishment of forward simulation. During the proofs, interactive verification and Auto-active verification are integrated, which improves the level of automation while reducing manual proof obligations. Eventually, three issues that violate correctness and safety properties are identified in the source code, and solutions are proposed for these issues.

Abstract:Hybrid communicating sequential process (HCSP) is a formal modeling language widely used for hybrid systems. It integrates logic-driven state transitions, typical of digital computation, with continuous evolution governed by differential equations that capture physical dynamics. This dual nature makes HCSP particularly suitable for modeling safety-critical cyber-physical system (CPS). However, practical verification of hybrid systems remains challenging due to their complex implementations and intricate synchronization behaviors. This study introduces hybrid refinement logic (HRL), a formal logic framework for verifying the refinement relation between abstract models and concrete implementations. HRL promotes modular and reusable verification by structuring proofs hierarchically according to the structure of the system. To further reduce verification complexity, HRL also supports refinement reasoning between parallel synchronous processes and sequential processes, significantly alleviating the proof burden.

Abstract:In the development of complex software systems, effective integration between the design phase and the verification phase is crucial for ensuring system reliability and functional correctness. However, heterogeneity in modeling languages, semantics, and data structures across design and verification tools often leads to semantic inconsistencies during model transformation, insufficient toolchain interoperability, and inadequate verification coverage. To address these challenges, this study proposes a layered transformation and multi-perspective cross-verification mechanism based on a unified intermediate representation (UIR). Starting from the design model, systems-theoretic process analysis (STPA) is applied to conduct hazard analysis and identify unsafe control actions, from which safety constraints are extracted and cross-checked against existing functional, timing, and safety properties. Subsequently, a mapping from the design model to the UIR is constructed, and the structure, behavior, timing, and safety constraints are formally specified within a unified syntactic and semantic domain. On this basis, layered transformation rules, together with traceability metadata, are defined to cover the above elements. Based on the UIR, complementary verification models, such as temporal, logical, and probabilistic models, are derived, and the safety constraints produced by STPA are systematically translated into verifiable properties. Multi-perspective cross-verification is then conducted, including consistency checking among source, intermediate, and target models, temporal and logical property verification, probabilistic analysis, and satisfiability checking of safety constraints. Case studies on an autonomous vehicle control system and a multi-domain collaborative unmanned aerial vehicle (UAV) control system demonstrate that the proposed method improves verification coverage and accuracy, enhances traceability throughout transformation and verification, and provides a consistent and provable technical pathway for safety-driven development of complex systems.

Abstract:Deep reinforcement learning has achieved excellent results in many complex tasks, but its policies still lack real-time safety guarantees in dynamic, high-dimensional environments. It is therefore urgent to introduce a safety monitoring mechanism during deployment that can evaluate and correct agent decisions in real time. Existing data-driven black-box monitoring methods focus on discrete or binary decisions and are hard to transfer directly to continuous action spaces. To address the above issue, this study proposes a fuzzy-mapping-entropy-driven safety monitoring framework, which can be constructed solely from state, action, and cost data without requiring any environment model. Specifically, the method first uses a Gaussian mixture model (GMM) to perform hard partitioning of states and soft membership of actions on the offline collected safe trajectories, and proposes fuzzy mapping entropy to adaptively determine the optimal number of action clusters under the premise of balancing uniformity and model complexity. Next, fuzzy logic rules are built in the Mamdani framework, and cluster centers are jointly fine-tuned with a residual network and an adversarial discriminator to make the generated actions closer to the real safe distribution. In the online phase, the monitor computes a cluster consistency measure for each pending state-action pair based on GMM posterior probabilities. If this measure falls below a threshold, fuzzy inference is used to generate a smooth safe replacement action, thus correcting the action before a risk occurs. PPO-Lag, TRPO-Lag, and CPPO-PID policies are evaluated under the proposed monitoring framework on three navigation tasks in Safety-Gymnasium. The results show that the framework significantly reduces cumulative safety costs while keeping almost the same or slightly higher task returns and maintains a high warning coverage rate, which confirms its effectiveness and practicality in continuous action scenarios.

Abstract:Active learning of timed automata is an important research topic. Active learning of multi-clock timed automata is one of the important research directions. However, the existing learning algorithms for multi-clock timed automata have relatively slow learning speed. This study proposes an improved active learning algorithm based on a timed observation tree. A data structure called the timed observation tree is defined to store the information obtained during the learning process. Based on the special structure of the timed observation tree, binary search techniques can be used to analyze counterexamples. By using this counterexample analysis technique, the number of membership queries and reset information queries can be reduced, thereby improving the efficiency of the proposed algorithm. Experimental results demonstrate the effectiveness of the method.

Abstract:In recent years, code generation based on large language models has been widely applied in software development. However, due to the inherent stochasticity of model outputs, ensuring the correctness of generated code remains a critical challenge. Formal verification provides a rigorous means to guarantee software correctness, but it requires both source code and corresponding requirements to be formalized into the specification language of verification tools. Dafny is a verification-oriented programming language equipped with automated verification support. From this perspective, this study explores the ability of large language models (LLMs) to translate Python code into Dafny. To this end, a prompt-based translation generation method is proposed, which consists of static translation and dynamic repair, together with a program-testing-based evaluation method. The static translation method employs three progressively refined prompting templates-namely, a basic template, a Dafny example-based template, and a Python-to-Dafny contrastive example-based template—to generate translations in a single step. The dynamic repair method iteratively invokes LLMs to refine translations by incorporating error messages produced during the previous round of code testing into the prompt. For evaluation, when no existing test suites are available, test cases are automatically generated using LLMs. The translated Dafny programs are then verified using Dafny testing tools in conjunction with the generated test cases to assess translation correctness. Experiments are conducted on HumanEval, MBPP, and LeetCode datasets using representative large language models, including GPT-4o and DeepSeek-V3. Experimental results demonstrate that the contrastive example-based prompting template and the dynamic repair method effectively improve the performance of LLMs on the Python-to-Dafny code translation task. Furthermore, factors influencing translation quality are analyzed based on experimental observations, and the evaluation methodology and criteria are discussed.

Abstract:Web 3.0 is a new-generation Internet framework based on blockchain technology, which facilitates data assetization and enables the formation of tradable digital assets, thus promoting the development of the digital economy. However, Web 3.0 still faces several challenges in user ecosystem construction and digital asset circulation: (1) The diversity of user trust mechanisms in Web 3.0 poses challenges to digital identity management. (2) The low cost of digital asset infringement and coarse-grained authentication in Web 3.0 hinder the efficient circulation of digital assets. (3) The open and autonomous nature of Web 3.0, together with the diversity of participating entities, leads to difficulties in user ecosystem governance. (4) The openness and transparency of data, along with diverse attack surfaces in Web 3.0, make it difficult to balance privacy protection and security regulation. To address these four challenges, a Web 3.0 technology architecture oriented toward data assetization is proposed. Focusing on the requirements of data assetization in identity management, asset circulation, ecosystem governance, and security regulation, and in combination with the technical characteristics of Web 3.0, relevant Web 3.0 research work at home and abroad is summarized, classified, analyzed, and reviewed. Specifically, this study includes (1) distributed digital identity management mechanisms, including technologies such as digital identity creation, identifier authentication, and privacy protection; (2) Web 3.0 digital asset circulation mechanisms, including technologies such as digital asset ownership confirmation, authentication, and circulation; (3) Web 3.0 ecosystem governance mechanisms, including technologies such as user reputation evaluation and incentive mechanisms; (4) Web 3.0 digital asset security protection and regulation technologies, including proactive regulation, on-chain data monitoring, and application front-end security analysis. Finally, future research directions of Web 3.0 technologies are discussed.

Abstract:Unlearning has significant application value in safeguarding privacy, mitigating the impact of contaminated samples, and processing redundant data. However, existing unlearning methods are mostly applied to black-box models such as neural networks, while achieving efficient single-class and multi-class unlearning in interpretable TSK fuzzy classification systems remains challenging. To address this, this study proposes a TSK fuzzy unlearning method for classification (TSK-FUC). First, the rule base is divided into three subsets using the normalized activation strengths of rule antecedent parameters on the (single/multi-class) forgotten data: 1) a deleted rule set that is highly relevant to the forgotten data, 2) a retained rule set with low relevance to the forgotten data, and 3) an updated rule set showing overlapping relevance to both the retained and forgotten data. Subsequently, differential processing strategies are applied: the deleted rule set is directly removed to eliminate major information residues and reduce the number of system parameters; the retained rule set is fully preserved to reduce parameter adjustment scope during unlearning; and for the updated rules, class-specific noise is added to the consequent parameters to further eliminate information related to the forgotten data, thus achieving single-class and multi-class unlearning. Experimental results on 16 benchmark datasets demonstrate that TSK-FUC accurately partitions the rule space and exhibits effective single-class and multi-class unlearning performance through differentiated processing in both 0-order and 1-order established TSK fuzzy classification systems. This method maintains the interpretability of the rule base while rendering the TSK fuzzy classification system more lightweight in terms of structure after unlearning.

Abstract:Spatio-temporal logical analysis refers to accurately expressing spatio-temporal relationships between entities using logical symbols. Traditional spatio-temporal logical analysis adopts two paradigms: closed-domain and open-domain approaches. Closed-domain methods predefine symbolic systems for representing spatio-temporal logic and then translate natural language into logical expressions. While ensuring accurate representation of spatio-temporal relationships, such methods face limitations in handling complex relationships due to the constraints of artificial definitions. Open-domain approaches extract keywords to represent spatio-temporal relationships using natural language itself. Although capable of covering complex relationships, these methods suffer from the semantic ambiguity inherent in natural language, resulting in imprecise logical representations. The purpose of this study is to convert natural language expressions of spatio-temporal relationships into logical language, enabling more precise representation of spatio-temporal information. To address the forementioned issues, this study considered the linguistic observation that spatio-temporal relationships in language are primarily expressed through localizers. By defining the semantics of localizers through logical symbols, the proposed framework aims to overcome both the insufficiency of coverage and the lack of precision. Accordingly, a spatio-temporal logical framework for localizers is established, including 1) the design of annotation specifications that define the logical expression scope of localizers and provide detailed annotation guidelines; 2) manual annotation of 6190 samples from the People’s Daily and CTB datasets to construct a task-specific corpus based on the proposed specifications; 3) application of large language models to perform logical reasoning on localizer-triggered spatio-temporal expressions, achieving an accuracy exceeding 70% based on corpus-driven inference.

Abstract:As a kind of graph structure with timestamps when nodes interact with each other, temporal graphs have more modeling advantages than static graphs. For example, they can detect money laundering, order brushing, equity relationships, financial fraud, and circular guarantees within a certain time interval. The cycle is the modeling of the behavior that forms a cycle in a temporal graph. Existing temporal cycle detection or mining methods mostly focus on the detection of non-decreasing complete cycles in time, but overlook the analysis and discovery of approximate cycles within a certain time interval. The discovery of such approximate cycles can detect fraudulent behavior with stronger cheating techniques. To address the problem of discovering approximate cycles that have already appeared within a certain time interval but are not fully displayed in a single source of data, this study first proposes an approximate cycle detection method based on the depth-first search, which is referred to as the baseline method (Baseline). It first mines complete cycles composed of edges satisfying non-decreasing order in each window, and then employs nodes that meet certain criteria as the start and end points of approximate cycles. In the subsequent windows, paths composed of edges within a certain time interval are mined, namely time-interval approximate cycles. To address the problems of Baseline, this study subsequently proposes an improved method for approximate cycle detection, referred to as the improved method (Improved). It first utilizes the node activity to enhance the possibility of start and end points, then improves the index features by adopting active paths and hotspots, and finally accelerates detection by employing the bidirectional search and connection from start and end points to hotspots. Extensive experiments on real and synthetic data demonstrate the efficiency and effectiveness of the proposed method.

Abstract:With the rapid development of 5G technology, the 5G-AKA protocol, as the core security mechanism of 5G technology, has caught widespread attention. Although the deployment of the 5G-AKA protocol has promoted the high-speed interconnection of communication networks, it has also raised users’ concerns about privacy leakage. During the protocol interaction, operators will collect a large amount of data, and once the data is leaked, it will pose a serious threat to users. Therefore, this study proposes an anonymous authentication and key agreement protocol based on SM2 to enhance the privacy of the user authentication process and minimize the disclosure of user information. It extends the Chinese cryptographic SM2 digital signature algorithm to achieve the signature of multiple messages, combines the ElGamal algorithm to encrypt the user’s identity, and adopts zero-knowledge proof technology to ensure the anonymity of the user credentials, thereby achieving the anonymous authentication of the user’s identity. The protocol protects the identity privacy of legitimate users in network activities and effectively blocks the illegal acquisition of user information. Additionally, the protocol holds the accountability for malicious users, allowing authorized regulatory agencies to restore the user’s identity in a legal process. Finally, protocol experimental evaluations are conducted, with deployment and implementation carried out on Windows and Raspberry Pi 4B platforms. The evaluation results show that the consumed time of the anonymous authentication and key agreement process is at the millisecond level, fully demonstrating the efficiency and practicality of this protocol.

Abstract:With the rapid advancement of deep learning and computer vision, grayscale image colorization has evolved from traditional handcrafted feature-based methods to data-driven deep neural network paradigms. However, existing evaluation systems for grayscale image colorization models face the following two challenges: First, due to the limitations of evaluation metrics and the highly ill-posed nature of the colorization task, traditional quantitative metrics such as PSNR, SSIM, and FID cannot effectively quantify the performance of grayscale image colorization models. Second, it is time-consuming, laborious, and infeasible to conduct qualitative analyses through large-scale subjective experiments. To address these issues, a new evaluation method for grayscale image colorization models based on hard sample mining is proposed. The method aims to efficiently identify representative samples for model comparison through multi-dimensional evaluation (including image quality, aesthetics epression, and color difference), and then conduct a controlled small-scale subjective experiment to reliably compare different models. Subsequently, the advantages and shortcomings of the models are revealed. Experimental results show that the proposed method can efficiently and accurately find hard samples, and reveal the strengths and weaknesses of the models while drastically reducing the scale of subjective experiments, providing a new paradigm for grayscale image colorization model evaluation and indicating the direction for model optimization.