Wenxi Wang

Yang Hu, Wenxi Wang

IAM misconfigurations are a major cause of privilege escalation (PE) attacks in the cloud, leading to data breaches and major financial losses. Existing PE detectors have two main limits: they cover only some PE types, so many attacks are missed, and they require full access to cloud configurations, which customers may not want to share because of sensitive information. We present TAC, the first IAM PE detection framework that supports both whitebox and greybox analysis for Amazon Web Services (AWS). To improve coverage, we systematically study how permissions are acquired in AWS IAM and identify five PE categories. All five share one pattern: permissions spread across entities. We define this as permission flows and manually extract 219 templates from more than 14,000 AWS operations. Based on this, we build TAC-WB, a whitebox detector with broad PE coverage. We also build TAC-GB, the first greybox PE detector, which works with partial configurations. Customers can choose which entities to reveal and whether to answer questions about permissions. TAC-GB uses a dynamic query process that adapts to each response and uses reinforcement learning with graph neural networks to ask the most useful questions while reducing interaction. We also create TAC-Bench, a benchmark with 2,500 tasks reflecting real-world IAM misconfigurations. Experiments show that TAC-WB finds all PEs missed by prior tools, while TAC-GB outperforms other greybox methods and often matches whitebox methods even with limited query budgets.

Zichen Xie, Wenxi Wang

As Large Language Models (LLMs) increasingly assist secure software development, their ability to meet the rigorous demands of Rust program verification remains unclear. Existing evaluations treat Rust verification as a black box, assessing models only by binary pass or fail outcomes for proof hints. This obscures whether models truly understand the logical deductions required for verifying nontrivial Rust code. To bridge this gap, we introduce VCoT-Lift, a framework that lifts low-level solver reasoning into high-level, human-readable verification steps. By exposing solver-level reasoning as an explicit Verification Chain-of-Thought, VCoT-Lift provides a concrete ground truth for fine-grained evaluation. Leveraging VCoT-Lift, we introduce VCoT-Bench, a comprehensive benchmark of 1,988 VCoT completion tasks for rigorously evaluating LLMs' understanding of the entire verification process. VCoT-Bench measures performance along three orthogonal dimensions: robustness to varying degrees of missing proofs, competence across different proof types, and sensitivity to the proof locations. Evaluation of ten state-of-the-art models reveals severe fragility, indicating that current LLMs fall well short of the reasoning capabilities exhibited by automated theorem provers.

Huansheng Ning, Zhangfeng Pi, Wenxi Wang et al.

Human beings have been affected by disasters from the beginning of life, bringing them many sad memories. In the long struggle against disaster, people have devised a variety of methods to train relevant participants in disaster relief capabilities. However, many traditional training methods, such as disaster exercises may not provide effective training to meet the need of today. Serious games provide an innovative approach to train participants in disaster relief, and a large number of Serious Games for Disaster Relief (SGDRs) have been developed to train disaster planning and rescue capabilities. At the same time, there is no systematics phase description for disaster relief, which cannot effectively guide participants' work and training in disaster relief. Therefore, this paper proposes a comprehensive and professional disaster relief classification framework according to different relief work in each stage of the disaster. Based on this framework, we review the functions and technologies of serious games in each classification, which can offer reliable guidance for researchers to better understand and use SGDRs. In addition, we analyze the serious games in each category, point out the limitations, and provide some valuable advice for developers on game design.

Huansheng Ning, Hang Wang, Wenxi Wang et al.

E-learning is a widely used learning method, but with the development of society, traditional E-learning method has exposed some shortcomings, such as the boring way of teaching, so that it is difficult to increase the enthusiasm of students and raise their attention in class. The application of serious games in E-learning can make up for these shortcomings and effectively improve the quality of teaching. When applying serious games to E-learning, there are two main considerations: educational goals and game design. A successful serious game should organically combine the two aspects and balance the educational and entertaining nature of serious games. This paper mainly discusses the role of serious games in E-learning, various elements of game design, the classification of the educational goals of serious games and the relationship between educational goals and game design. In addition, we try to classify serious games and match educational goals with game types to provide guidance and assistance in the design of serious games. This paper also summarizes some shortcomings that serious games may have in the application of E-learning.

Wenxi Wang, Yang Hu, Mohit Tiwari et al.

Propositional satisfiability (SAT) is an NP-complete problem that impacts many research fields, such as planning, verification, and security. Mainstream modern SAT solvers are based on the Conflict-Driven Clause Learning (CDCL) algorithm. Recent work aimed to enhance CDCL SAT solvers using Graph Neural Networks (GNNs). However, so far this approach either has not made solving more effective, or required substantial GPU resources for frequent online model inferences. Aiming to make GNN improvements practical, this paper proposes an approach called NeuroBack, which builds on two insights: (1) predicting phases (i.e., values) of variables appearing in the majority (or even all) of the satisfying assignments are essential for CDCL SAT solving, and (2) it is sufficient to query the neural model only once for the predictions before the SAT solving starts. Once trained, the offline model inference allows NeuroBack to execute exclusively on the CPU, removing its reliance on GPU resources. To train NeuroBack, a new dataset called DataBack containing 120,286 data samples is created. NeuroBack is implemented as an enhancement to a state-of-the-art SAT solver called Kissat. As a result, it allowed Kissat to solve up to 5.2% and 7.4% more problems on two recent SAT competition problem sets, SATCOMP-2022 and SATCOMP-2023, respectively. NeuroBack therefore shows how machine learning can be harnessed to improve SAT solving in an effective and practical manner.