Date: Wednesday 11 March 2020
Time: 08:30 - 10:00
Location / Room: Bayard

Chair:
Ylies Falcone, University Grenoble Alpes and Inria, FR

Co-Chair:
Todd Austin, University of Michigan, US

The session explores the use of state-of-the-art model-based analysis and verification techniques to secure and improve the performance of embedded systems. More specifically, it presents the use of satisfiability modulo theory, runtime monitoring, fuzzing, and model-checking to evaluate how secure is a system, prevent, and detect attacks.

Time	Label	Presentation Title Authors
08:30	5.5.1	IS REGISTER TRANSFER LEVEL LOCKING SECURE? Speaker: Chandan Karfa, IIT Guwahati, IN Authors: Chandan Karfa1, Ramanuj Chouksey1, Christian Pilato2, Siddharth Garg3 and Ramesh Karri3 1IIT Guwahati, IN; 2Politecnico di Milano, IT; 3New York University, US Abstract Register Transfer Level (RTL) locking seeks to prevent intellectual property (IP) theft of a design by locking the RTL description that functions correctly on the application of a key. This paper evaluates the security of a state-of-the-art RTL locking scheme using a satisfiability modulo theories (SMT) based algorithm to retrieve the secret key. The attack first obtains the high-level behavior of the locked RTL, and then use an SMT based formulation to find so-called distinguishing input patterns (DIP)/footnote{i.e., inputs that help eliminate incorrect keys from the keyspace.}. The attack methodology has two main advantages over the gate-level attacks. First, since the attack handles the design at the RTL, the method scales to large designs. Second, the attack does not apply separate unlocking strategies for the combinational and sequential parts of design; it handles both styles via a unifying abstraction. We demonstrate the attack on locked RTL generated by TAO, a state-of-the-art RTL locking solution. Empirical results show that we can partially or completely break designs locked by TAO. Download Paper (PDF; Only available from the DATE venue WiFi)
09:00	5.5.2	DESIGN SPACE EXPLORATION FOR MODEL-BASED COMMUNICATION SYSTEMS Speaker: Valentina Richthammer, University of Ulm, DE Authors: Valentina Richthammer, Marcel Rieß, Julian Bestler, Frank Slomka and Michael Glaß, University of Ulm, DE Abstract A main challenge of modem design lies in selecting a suitable combination of subsystems (e.g. Analog Digital/Digital Analog Converters (ADC/DAC), (de)modulators, scramblers, interleavers, and coding and filtering modules) - each of which can be implemented in a multitude of ways. At the same time, the complete modem configuration needs to be tailored to the specific requirements of the intended communication channel or scenario. Therefore, model-based design methodologies have recently been popularized in this field, since their application facilitates the specification of individual modem components that are easily exchanged during the automated synthesization of the modem. However, this development has resulted in a tremendous increase in the number of synthesizable modem options. In fact, the optimal modem configuration for a communication scenario can not readily be determined, since an exhaustive analysis of all configuration possibilities is computationally intractable. To remedy this, we propose a fully automated Design Space Exploration (DSE) methodology for model-based modem design that combines (I) the metaheuristic exploration and optimization of modem-configuration possibilities with (II) a simulative analysis of suitable measures of communication quality. The presented case study for an acoustic underwater communication scenario supports the described need for novel, automated methodologies in the area of model-based design, since the modem configurations discovered during a comparably short DSE are demonstrated to significantly outperform state-of-the-art modems from literature. Download Paper (PDF; Only available from the DATE venue WiFi)
09:30	5.5.3	STATISTICAL TIME-BASED INTRUSION DETECTION IN EMBEDDED SYSTEMS Speaker: Nadir Carreon Rascon, University of Arizona, US Authors: Nadir Carreon Rascon, Allison Gilbreath and Roman Lysecky, University of Arizona, US Abstract This paper presents a statistical method based on cumulative distribution functions (CDF) to analyze an embedded system's behavior to detect anomalous and malicious executions behaviors. The proposed method analyzes the internal timing of the system by monitoring individual operations and sequences of operations, wherein the timing of operations is decomposed into multiple timing subcomponents. Creating the normal model of the system utilizing the internal timing adds resilience to zero-day attacks, and mimicry malware. The combination of CDF-based statistical analysis and timing subcomponents enable both higher detection rates and lower false positives rates. We demonstrate the effectiveness of the approach and compare to several state-of-the-art malware detection methods using two embedded systems benchmarks, namely a network connected pacemaker and an unmanned aerial vehicle, utilizing seven different malware. Download Paper (PDF; Only available from the DATE venue WiFi)
10:00	IP2-14, 637	IFFSET: IN-FIELD FUZZING OF INDUSTRIAL CONTROL SYSTEMS USING SYSTEM EMULATION Speaker: Dimitrios Tychalas, New York University, US Authors: Dimitrios Tychalas1 and Michail Maniatakos2 1New York University, US; 2New York University Abu Dhabi, AE Abstract Industrial Control Systems (ICS) have evolved in the last decade, shifting from proprietary software/hardware to contemporary embedded architectures paired with open-source operating systems. In contrast to the IT world, where continuous updates and patches are expected, decommissioning always-on ICS for security assessment can incur prohibitive costs to their owner. Thus, a solution for routinely assessing the cybersecurity posture of diverse ICS without affecting their operation is essential. Therefore, in this paper we introduce IFFSET, a platform that leverages full system emulation of Linux-based ICS firmware and utilizes fuzzing for security evaluation. Our platform extracts the file system and kernel information from a live ICS device, building an image which is emulated on a desktop system through QEMU. We employ fuzzing as a security assessment tool to analyze ICS specific libraries and find potential security threatening conditions. We test our platform with commercial PLCs, showcasing potential threats with no interruption to the control process. Download Paper (PDF; Only available from the DATE venue WiFi)
10:01	IP2-15, 814	FANNET: FORMAL ANALYSIS OF NOISE TOLERANCE, TRAINING BIAS AND INPUT SENSITIVITY IN NEURAL NETWORKS Speaker: Mahum Naseer, TU Wien, AT Authors: Mahum Naseer1, Mishal Fatima Minhas2, Faiq Khalid1, Muhammad Abdullah Hanif1, Osman Hasan2 and Muhammad Shafique1 1TU Wien, AT; 2National University of Sciences and Technology, PK Abstract With a constant improvement in the network architectures and training methodologies, Neural Networks (NNs) are increasingly being deployed in real-world Machine Learning systems. However, despite their impressive performance on "known inputs", these NNs can fail absurdly on the "unseen inputs", especially if these real-time inputs deviate from the training dataset distributions, or contain certain types of input noise. This indicates the low noise tolerance of NNs, which is a major reason for the recent increase of adversarial attacks. This is a serious concern, particularly for safety-critical applications, where inaccurate results lead to dire consequences. We propose a novel methodology that leverages model checking for the Formal Analysis of Neural Network (FANNet) under different input noise ranges. Our methodology allows us to rigorously analyze the noise tolerance of NNs, their input node sensitivity, and the effects of training bias on their performance, e.g., in terms of classification accuracy. For evaluation, we use a feed-forward fully-connected NN architecture trained for the Leukemia classification. Our experimental results show 11% noise tolerance for the given trained network, identify the most sensitive input nodes, confirm the biasness of the available training dataset, and indicate that the proposed methodology is much more rigorous and yet comparable to validation testing in terms of time and computational resources for larger noise ranges. Download Paper (PDF; Only available from the DATE venue WiFi)
10:00		End of session