Biblio
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.
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.
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.
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.