Logic locking is an effective approach for protecting integrated circuits against security threats such as Intellectual Property (IP) piracy and malicious design modifications. To defeat SAT attacks, state-of-the-art locking schemes, which are typically constructed using point-function that remains constant when the correct key is applied, while producing a wrong output only under a specific input pattern if an incorrect key is provided. Although this significantly increases the effort required for SAT attack, it introduces a new vulnerability that can be exploited to discover SAT-resilient blocks. Our observation is that pointfunction can lead to control signals, which exhibit significantly lower switching probability and yield clues for identifying anti-SAT cones. This work aims to reveal such clues at the level of FPGA netlist, where switching behavior characteristics can be quantified using the initialization vectors of Look-up-Tables (LUTs). We leverage the switching behavior measurements of LUTs to pinpoint signals with extremely low switching activity to locate control signals associated with SAT-resilient blocks. By forcing the identified control signals to a constant value, the protective function of the SAT-resilient blocks can be neutralized. We validate our attack method on locked circuits with anti-SAT enhancement. Experimental results on six compound logic locking schemes yield an average attack success rate of 99.6% and 100% key recovery rate for each neutralized circuit.

Fault attacks are effective side-channel attack methods for cryptanalysis. However, existing fault attack methods involve manual derivation of complex fault models or computation-intensive statistical analysis of mass faulty ciphertexts to recover the key. In addition, most methods are only applicable to a specific cryptographic algorithm with strict requirements on the type and quantity of faults injected, lacking scalability and generality. Taking inspiration from machine learning and formal verification, we propose an automated fault attack framework, which supports multi-byte fault attacks on both SPN and generalized Feistel structure ciphers. This framework automates the generation of formal fault propagation models, extraction of fault properties, and formal fault analysis. We construct formal fault propagation models for cipher designs to measure the fault propagation precisely, eliminating the requirement of manually deriving fault propagation models. We mine accurate invariable behaviors in fault propagation effects as fault properties using a small number of fault traces and further utilize property constraints to retrieve the key through formal analysis. This method implements a formal fault attack on SM4 in 25th to 28th rounds for the first time. Experimental results on AES, RSM, LED and SM4 demonstrate the effectiveness of our method, with key search complexity lower than or equal to state-of-the-art methods, while requiring only four faulty ciphertexts to recover a round key.

Improving resource utilization in datacenters is vital for reducing costs for cloud service providers (CSPs). Increasing resource utilization must be balanced with maintaining quality of service (QoS) for latency-critical applications. In cloud environments, users often request excessive resources for applications to ensure QoS. To address this issue, CSPs use resource overcommitment - offering users resources that exceed the actual capacity of physical infrastructure. However, if not properly managed, such strategies may result in performance degradation or even request failure. Therefore, to achieve optimal resource utilization while maintaining QoS to applications, it is critical to implement a fine-grained overcommitment strategy.We propose HAPPIES, a History-aware management system with a precise prediction for machine resource demand. HAPPIES uses historical usage to extract resource characteristics and build application portraits that describe their resource demands. Compared to the existing strategy, this is a more aggressive overcommitment strategy that achieves higher resource utilization. We simulated experiments on 3,021 nodes and deployed over 14,000 applications on them. Results show that HAPPIES significantly outperforms Kubernetes Least Request and Peak Oracle in load balancing. Not only does it reduce the number of nodes experiencing high utilization, but it also decreases the peak usage of the most heavily utilized nodes. Therefore, HAPPIES scheduling reduces the risk of a machine being used beyond capacity.

Identifying and managing performance interference in clouds has long been a critical and challenging task for cloud providers. They keep seeking useful performance indicators from underlying systems to monitor cloud applications accurately. However, state-of-the-art indicators are either sensitive to limited applications and resource contention or are unrobust to the continually changing production environments. There still lacks a practical and efficient indicator for production environments.

Ensuring privilege transition integrity during execution context switch is crucial for protecting the processor from unauthorized access and malicious actions. However, existing methods fall short in covering potential attack paths and vectors in a complete manner. In this work, we propose a method for formal verification of privilege correctness targeting privilege escalation attacks, where the program processes on non-privileged mode may access the sensitive information stored in Special purpose registers (SPRs). We specify assertion property and utilize the Klee symbolic execution engine to formally check the consistency in privilege when accessing contents in critical registers. The formal solver performs state space exploration through heuristic search to identify the possible integrity violation test cases that can trigger an illegal privilege escalation, which further allows creating a minimal simulation system consisting of the CPU and Quick Memory (QMEM) modules to replay the privilege violation process. Experimental results have demonstrated that our method can systematically verify the privilege validity to protect the system from privilege escalation attacks on a RISC-V processor.