Visible to the public Biblio

Filters: Author is Wang, Yu  [Clear All Filters]
A B C D E F G H I J K L M N O P Q R S T U V W X Y Z 
C
Gao, Fengjuan, Chen, Tianjiao, Wang, Yu, Situ, Lingyun, Wang, Linzhang, Li, Xuandong.  2016.  Carraybound: Static Array Bounds Checking in C Programs Based on Taint Analysis. Proceedings of the 8th Asia-Pacific Symposium on Internetware. :81–90.

C programming language never performs automatic bounds checking in order to speed up execution. But bounds checking is absolutely necessary in any program. Because if a variable is out-of-bounds, some serious errors may occur during execution, such as endless loop or buffer overflows. When there are arrays used in a program, the index of an array must be within the boundary of the array. But programmers always miss the array bounds checking or do not perform a correct array bounds checking. In this paper, we perform static analysis based on taint analysis and data flow analysis to detect which arrays do not have correct array bounds checking in the program. And we implement an automatic static tool, Carraybound. And the experimental results show that Carraybound can work effectively and efficiently.

Huang, Zhenqi, Wang, Yu, Mitra, Sayan, Dullerud, Geir.  2016.  Controller Synthesis for Linear Dynamical Systems with Adversaries. Proceedings of the Symposium and Bootcamp on the Science of Security. :53–62.

We present a controller synthesis algorithm for a reach-avoid problem in the presence of adversaries. Our model of the adversary abstractly captures typical malicious attacks envisioned on cyber-physical systems such as sensor spoofing, controller corruption, and actuator intrusion. After formulating the problem in a general setting, we present a sound and complete algorithm for the case with linear dynamics and an adversary with a budget on the total L2-norm of its actions. The algorithm relies on a result from linear control theory that enables us to decompose and compute the reachable states of the system in terms of a symbolic simulation of the adversary-free dynamics and the total uncertainty induced by the adversary. With this decomposition, the synthesis problem eliminates the universal quantifier on the adversary's choices and the symbolic controller actions can be effectively solved using an SMT solver. The constraints induced by the adversary are computed by solving second-order cone programmings. The algorithm is later extended to synthesize state-dependent controller and to generate attacks for the adversary. We present preliminary experimental results that show the effectiveness of this approach on several example problems.

Huang, Zhenqi, Wang, Yu, Mitra, Sayan, Dullerud, Geir.  2016.  Controller Synthesis for Linear Dynamical Systems with Adversaries. Proceedings of the {Symposium} and {Bootcamp} on the {Science} of {Security}. :53–62.
We present a controller synthesis algorithm for a reach-avoid problem in the presence of adversaries. Our model of the adversary abstractly captures typical malicious attacks envisioned on cyber-physical systems such as sensor spoofing, controller corruption, and actuator intrusion. After formulating the problem in a general setting, we present a sound and complete algorithm for the case with linear dynamics and an adversary with a budget on the total L2-norm of its actions. The algorithm relies on a result from linear control theory that enables us to decompose and compute the reachable states of the system in terms of a symbolic simulation of the adversary-free dynamics and the total uncertainty induced by the adversary. With this decomposition, the synthesis problem eliminates the universal quantifier on the adversary's choices and the symbolic controller actions can be effectively solved using an SMT solver. The constraints induced by the adversary are computed by solving second-order cone programmings. The algorithm is later extended to synthesize state-dependent controller and to generate attacks for the adversary. We present preliminary experimental results that show the effectiveness of this approach on several example problems.
D
Liu, Shigang, Zhang, Jun, Wang, Yu, Zhou, Wanlei, Xiang, Yang, Vel., Olivier De.  2018.  A Data-driven Attack Against Support Vectors of SVM. Proceedings of the 2018 on Asia Conference on Computer and Communications Security. :723–734.
Machine learning (ML) is commonly used in multiple disciplines and real-world applications, such as information retrieval, financial systems, health, biometrics and online social networks. However, their security profiles against deliberate attacks have not often been considered. Sophisticated adversaries can exploit specific vulnerabilities exposed by classical ML algorithms to deceive intelligent systems. It is emerging to perform a thorough security evaluation as well as potential attacks against the machine learning techniques before developing novel methods to guarantee that machine learning can be securely applied in adversarial setting. In this paper, an effective attack strategy for crafting foreign support vectors in order to attack a classic ML algorithm, the Support Vector Machine (SVM) has been proposed with mathematical proof. The new attack can minimize the margin around the decision boundary and maximize the hinge loss simultaneously. We evaluate the new attack in different real-world applications including social spam detection, Internet traffic classification and image recognition. Experimental results highlight that the security of classifiers can be worsened by poisoning a small group of support vectors.
L
Huo, Dongdong, Wang, Yu, Liu, Chao, Li, Mingxuan, Wang, Yazhe, Xu, Zhen.  2020.  LAPE: A Lightweight Attestation of Program Execution Scheme for Bare-Metal Systems. 2020 IEEE 22nd International Conference on High Performance Computing and Communications; IEEE 18th International Conference on Smart City; IEEE 6th International Conference on Data Science and Systems (HPCC/SmartCity/DSS). :78—86.

Unlike traditional processors, Internet of Things (IoT) devices are short of resources to incorporate mature protections (e.g. MMU, TrustZone) against modern control-flow attacks. Remote (control-flow) attestation is fast becoming a key instrument in securing such devices as it has proven the effectiveness on not only detecting runtime malware infestation of a remote device, but also saving the computing resources by moving the costly verification process away. However, few control-flow attestation schemes have been able to draw on any systematic research into the software specificity of bare-metal systems, which are widely deployed on resource-constrained IoT devices. To our knowledge, the unique design patterns of the system limit implementations of such expositions. In this paper, we present the design and proof-of-concept implementation of LAPE, a lightweight attestation of program execution scheme that enables detecting control-flow attacks for bare-metal systems without requiring hardware modification. With rudimentary memory protection support found in modern IoT-class microcontrollers, LAPE leverages software instrumentation to compartmentalize the firmware functions into several ”attestation compartments”. It then continuously tracks the control-flow events of each compartment and periodically reports them to the verifier. The PoC of the scheme is incorporated into an LLVM-based compiler to generate the LAPE-enabled firmware. By taking experiments with several real-world IoT firmware, the results show both the efficiency and practicality of LAPE.

S
Xia, Lixue, Tang, Tianqi, Huangfu, Wenqin, Cheng, Ming, Yin, Xiling, Li, Boxun, Wang, Yu, Yang, Huazhong.  2016.  Switched by Input: Power Efficient Structure for RRAM-based Convolutional Neural Network. Proceedings of the 53rd Annual Design Automation Conference. :125:1–125:6.

Convolutional Neural Network (CNN) is a powerful technique widely used in computer vision area, which also demands much more computations and memory resources than traditional solutions. The emerging metal-oxide resistive random-access memory (RRAM) and RRAM crossbar have shown great potential on neuromorphic applications with high energy efficiency. However, the interfaces between analog RRAM crossbars and digital peripheral functions, namely Analog-to-Digital Converters (ADCs) and Digital-to-Analog Converters (DACs), consume most of the area and energy of RRAM-based CNN design due to the large amount of intermediate data in CNN. In this paper, we propose an energy efficient structure for RRAM-based CNN. Based on the analysis of data distribution, a quantization method is proposed to transfer the intermediate data into 1 bit and eliminate DACs. An energy efficient structure using input data as selection signals is proposed to reduce the ADC cost for merging results of multiple crossbars. The experimental results show that the proposed method and structure can save 80% area and more than 95% energy while maintaining the same or comparable classification accuracy of CNN on MNIST.