Abstract Deep learning excels in detecting source code vulnerabilities, where image-based detection methods overcome ignoring deep code semantic information in token-based methods and the inefficiency of graph-based methods. Unfortunately, current image-based methods cannot sufficiently extract vulnerability-related features due to three key limitations: (1) the inappropriateness of the construction of node centrality for sequential Program Dependency Graphs (PDGs), (2) the ineffective code analysis of traditional embedding models, and (3) the poor existing truncation/padding methods. Moreover, they fail to achieve effective vulnerability localization due to the irregular output of their interpretation method. In response, we propose a novel image-based line-level source code vulnerability detection system VulSCC. Firstly, VulSCC constructs a novel centrality combination and leverages a code large language model to capture richer vulnerability-related features. Secondly, we integrate an SPP layer to convert PDGs into images without distortion, as it adaptively aggregates arbitrary sizes into fixed-length vectors without truncation/padding. Finally, we use the occlusion technique to interpret the model predictions, which locate specific vulnerability lines, enabling effective vulnerability localization. Experimental results of VulSCC against seven SoTA methods show optimal detection performance in function-level detection. Additionally, we evaluate the effectiveness of the occlusion technique in localizing vulnerabilities, with interpretation success rate exceeding 90%.

As cloud services become increasingly integral to modern IT infrastructure, ensuring hardware reliability is essential to sustain high-quality service. Memory failures pose a significant threat to overall system stability, making accurate failure prediction through the analysis of memory error logs (i.e., Correctable Errors) imperative. Existing memory failure prediction approaches have notable limitations: rule-based expert models suffer from limited generalizability and low recall rates, while automated feature extraction methods exhibit suboptimal performance. To address these limitations, we propose M2-MFP: a Multi-scale and Multi-Level Memory Failure Prediction framework designed to enhance the reliability and availability of cloud infrastructure. M2-MFP converts correctable errors (CEs) into multi-level binary matrix representations and introduces a Binary Spatial Feature Extractor (BSFE) to automatically extract high-order features at both DIMM-level and bit-level. Building upon the BSFE outputs, we develop a dual-path temporal modeling architecture: 1) a time-patch module that aggregates multi-level features within observation windows, and 2) a time-point module that employs interpretable rule-generation trees trained on bit-level patterns. Experiments on both benchmark datasets and real-world deployment show the superiority of M2-MFP as it outperforms existing state-of-the-art methods by significant margins. Code and data are available at this repository: https://github.com/hwcloud-RAS/M2-MFP.

This paper investigates the attitude tracking problem for spacecraft with limited communication, network congestion, unknown model parameters, actuator saturation, and external disturbances. To alleviate communication load, a novel sigmoid event-triggered mechanism is proposed with the special ability to guarantee a high minimum inter-execution time to avoid network congestion like package loss or time delay effectively. A neural network-based adaptive control algorithm is designed to deal with unknown model parameters. Besides, the problem of actuator saturation is tackled by introducing a dynamic loop gain function-based approach. System stability is proved by Lyapunov stability analysis and the high minimum inter-event time is substantiated by Zeno Behavior analysis with explanatory remarks. Numerical simulation results also show that a high minimum inter-event time and a high average inter-event time can be realized on the premise of high attitude tracking accuracy. Compared with all the previous studies, the ratio of the minimum inter-execution time to the average minimum inter-execution time has been improved by nearly 10 times with the proposed approach. Note to Practitioners—This paper was motivated by the problem of spacecraft attitude takeover control, but it also applies to other aperiodic discrete-time control systems. Existing event-triggered control methods have solved the problem of limited communication for attitude takeover control of spacecraft by reducing the number of times wireless communication is required. This paper proposes a new method for realizing quasi-periodic control with a large time gap between any two consistent control impulses using a hyperbolic tangent function or another sigmoid function in an event-triggered mechanism. The proposed sigmoid event-triggered mechanism (ETM) can magnify the event-triggered threshold dozens of times in a short time to avoid unnecessary frequent triggering without decreasing the precision of control. It’s feasible to employ the proposed sigmoid ETM to deal with limited communication and network congestion in other network control systems that are constructed with similar dynamic structures. Furthermore, it would be marvelous if we could transform this sigmoid ETM into a high-efficiency decision-making mechanism in some control systems without using a wireless network. Now we are studying how to realize orbital-attitude (maneuver) control with a relatively average time interval and fewer times of orbit transfer by using the proposed sigmoid ETM. Besides, to further improve the system performance, we are also seeking to further increase the ratio of the minimum inter-execution time to the average inter-execution time. For the purpose of a more even distribution of the triggering events on the time axis, we may modify the proposed sigmoid event-triggered method or associate it with other methods.

Cryptographic algorithms are widely used to protect data privacy in many aspects of daily lives from smart card to cyber-physical systems. Unfortunately, programs implementing cryptographic algorithms may be vulnerable to practical power side-channel attacks, which may infer private data via statistical analysis of the correlation between power consumptions of an electronic device and private data. To thwart these attacks, several masking schemes have been proposed, giving rise to effective countermeasures for reducing the statistical correlation between private data and power consumptions. However, programs that rely on secure masking schemes are not secure a priori. Indeed, designing effective masking programs is a labor intensive and error-prone task. Although some techniques have been proposed for formally verifying masking countermeasures and for quantifying masking strength, they are currently limited to Boolean programs and suffer from low accuracy. In this work, we propose an approach for formally verifying masking countermeasures of arithmetic programs. Our approach is more accurate for arithmetic programs and more scalable for Boolean programs comparing to the existing approaches. It is essentially a synergistic integration of type inference and model-counting based methods, armed with domain specific heuristics. The type inference system allows a fast deduction of leakage-freeness of most intermediate computations, the model-counting based methods accounts for completeness, namely, to eliminate spurious flaws, and the heuristics facilitate both type inference and model-counting based reasoning, which improve scalability and efficiency in practice. In case that the program does contain leakage, we provide a method to quantify its masking strength. A distuiguished feature of our type sytem lies in its support of compositonal reasoning when verifying programs with procedure calls, so the need of inlining procedures can be significantly reduced. We have implemented our methods in a verification toolQMVerifwhich has been extensively evaluated on cryptographic benchmarks including full AES, DES and MAC-Keccak. The experimental results demonstrate the effectiveness and efficiency of our approach, especially for compositional reasoning. In particular, our tool is able to automatically prove leakage-freeness of arithmetic programs for which only manual proofs exist so far; it is also significantly faster than the state-of-the-art tools: EasyCrypt on common arithmetic programs,QMSInfer, SC Sniffer and maskVerif on Boolean programs.

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 effective countermeasure against side-channel attacks by removing the statistical dependence between secrecy and power consumption via randomization. However, designing efficient and effective masked implementations turns out to be an error-prone task. Current techniques for verifying whether masked programs are secure are limited in their applicability and accuracy, especially when they are applied. To bridge this gap, in this article, we first propose a sound type system, equipped with an efficient type inference algorithm, for verifying masked arithmetic programs against higher-order attacks. We then give novel model-counting-based and pattern-matching-based methods that are able to precisely determine whether the potential leaky observable sets detected by the type system are genuine or simply spurious. We evaluate our approach on various implementations of arithmetic cryptographic programs. The experiments confirm that our approach outperforms the state-of-the-art baselines in terms of applicability, accuracy, and efficiency.

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 dependence between secret data and side-channel information. However, designing masking algorithms is an error-prone process. In this paper, we propose a hybrid approach combing type inference and model-counting to verify masked arithmetic programs against side-channel attacks. The type inference allows an efficient, lightweight procedure to determine most observable variables whereas model-counting accounts for completeness. In case that the program is not perfectly masked, we also provide a method to quantify the security level of the program. We implement our methods in a tool QMVerif and evaluate it on cryptographic benchmarks. The experiment results show the effectiveness and efficiency of our approach.