Shifts in the IC supply chain have necessitated outsourcing design or fabrication to third-party vendors, introducing various hardware security issues, notably Hardware Trojans (HTs) as a prominent risk. The research in detecting and preventing HTs faces challenges due to the lack of standardized benchmarks and measurements. This paper introduces a framework to automatically generate dynamic functional HTs in a configurable and systematical manner at Register Transfer Level (RTL). The objective is not to produce HTs that are difficult to activate but to systematically create a diverse set of HT designs. This approach serves dual purposes: it aids the research community in testing their detection frameworks and facilitates buggy design benchmark creation for competitive exercises between blue and red teams. Our framework accepts RTL designs and configuration parameters, automating the generation of HT-inserted designs at RTL. We present an evaluation of the generated HT designs focusing on hardware cost overhead and post-synthesis survivability by verifying HT presence at both RT and gate levels. Results indicate that HTs employing only combinational logic are easier to optimize away but result in lower overhead compared to HTs that incorporate additional sequential logic.

We present an automated approach for detecting two types of Hardware Trojans (HTs) in hardware designs. Malicious adversaries often hide HTs under rare triggering conditions such as timing-based or input-based conditions to avoid their detection by state-of-the-art analysis techniques. Our Trojan detection method employs fuzzing and static analysis to generate models of suspicious hardware elements that are used as oracles to guide symbolic execution. Experimental evaluation on diverse hardware designs demonstrates significant speed-ups compared to existing approaches, achieving on average a 445X speed-up for timing-based HTs and on average 27X speed-up for input-dependent HTs.

Confidential computing aims to secure the code and data in use by providing a Trusted Execution Environment (TEE) for applications using hardware features such as Intel SGX. Timing and cache side-channel attacks, however, are often outside the scope of the threat model, although once exploited they are able to break all the default security guarantees enforced by hardware. Unfortunately, tools detecting potential side-channel vulnerabilities within applications are limited and usually ignore the strong attack model and the unique programming model imposed by Intel SGX. This article proposes a precise side-channel analysis tool, ENCIDER, detecting both timing and cache side-channel vulnerabilities within SGX applications via inferring potential timing observation points and incorporating the SGX programming model into analysis. ENCIDER uses dynamic symbolic execution to decompose the side-channel requirement based on the bounded non-interference property and implements byte-level information flow tracking via API modeling. We have applied ENCIDER to 4 real-world SGX applications, 2 SGX crypto libraries, and 3 widely-used crypto libraries, and found 29 timing side channels and 73 code and data cache side channels. We also compare ENCIDER with three state-of-the-art side channel analysis tools using their benchmarks. ENCIDER does not only report most of the bugs with 20%-50% run time improvement and 65%-92% memory usage improvement, but also detects 9 missing bugs from these tools. We have reported our findings to the corresponding parties, e.g., Intel and ARM, who have confirmed most of the vulnerabilities detected.

Due to the globalization of Integrated Circuit supply chain, hardware Trojans and the attacks that can trigger them have become an important security issue. One type of hardware Trojans leverages the “don’t care transitions” in Finite-state Machines (FSMs) of hardware designs. In this article, we present a symbolic approach to detecting don’t care transitions and the hidden Trojans. Our detection approach works at both register-transfer level (RTL) and gate level, does not require a golden design, and works in three stages. In the first stage, it explores the reachable states. In the second stage, it performs an approximate analysis to find the don’t care transitions and any discrepancies in the register values or output lines due to don’t care transitions. The second stage can be used for both predicting don’t care triggered Trojans and for guiding don’t care aware reachability analysis. In the third stage, it performs a state-space exploration from reachable states that have incoming don’t care transitions to explore the Trojan payload and to find behavioral discrepancies with respect to what has been observed in the first stage. We also present a pruning technique based on the reachability of FSM states. We present a methodology that leverages both RTL and gate-level for soundness and efficiency. Specifically, we show that don’t care transitions and Trojans that leverage them must be detected at the gate-level, i.e., after synthesis has been performed, for soundness. However, under specific conditions, Trojan payload exploration can be performed more efficiently at RTL. Additionally, the modular design of our approach also provides a fast Trojan prediction method even at the gate level when the reachable states of the FSM is known a priori . Evaluation of our approach on a set of benchmarks from OpenCores and TrustHub and using gate-level representation generated by two synthesis tools, YOSYS and Synopsis Design Compiler (SDC), shows that our approach is both efficient (up to 10× speedup w.r.t. no pruning) and precise (0% false positives both at RTL and gate-level netlist) in detecting don’t care transitions and the Trojans that leverage them. Additionally, the total analysis time can achieve up to 1.62× (using YOSYS) and 1.92× (using SDC) speedup when synthesis preserves the FSM structure, the foundry is trusted, and the Trojan detection is performed at RTL.

Internet of Things (IoT) frameworks are designed to facilitate provisioning and secure operation of IoT devices. A typical IoT framework consists of various software layers and components including third-party libraries, communication protocol stacks, the Hardware Abstraction Layer (HAL), the kernel, and the apps. IoT frameworks have implicit data flows in addition to explicit data flows due to their event-driven nature. In this paper, we present a static taint tracking framework, IFLOW, that facilitates the security analysis of system code by enabling specification of data-flow queries that can refer to a variety of software entities. We have formulated various security relevant data-flow queries and solved them using IFLOW to analyze the security of several popular IoT frameworks: Amazon FreeRTOS SDK, SmartThings SDK, and Google IoT SDK. Our results show that IFLOW can both detect real bugs and localize security analysis to the relevant components of IoT frameworks.

The rapid growth of the Internet of Things (IoT) industry has increased the demand for intellectual property (IP) cores. Increasing numbers of third-party vendors have raised security concerns for System-on-Chip (SoC) designers. With the growing complexity of SoC design, the workload is overwhelming for SoC designers to diagnose security vulnerabilities manually. Almost all existing SoC platforms are developed using SystemVerilog. However, there is a lack of reliable security static analysis tools for directly processing the SystemVerilog program. Due to its open-source, flexibility and extendability, RISC-V CPU has become an ideal platform for the IoT applications such as wearable devices, entertainment, smart thermostats, etc. As a result, assuring the trustworthiness of a given RISC-V system is highly desired. This paper proposes a graph neural network-based Trojan detection framework to protect the RISC-V SoC platform written in SystemVerilog from intruding malicious logic. The study is under-construction and planned to be validated on the Ariane RISC-V CPU with several peripheral IPs in the experimental section.

Analyzing multithreaded programs is notoriously hard due to the exponential number of thread interleavings. Although race detectors can help developers find and fix such bugs before the code is deployed, multithreaded code may still be buggy due to memory errors and assertion violations that are not due to race conditions. This paper presents a property directed symbolic execution of multithreaded code. Our approach, named SIFT, differs from previous work on detecting errors in multithreaded code by being property directed and by handling both memory safety and assertion checking that can be further customized by the user. SIFT can detect bugs that may or may not be due to data races, and works in an iterative way. In each step, it explores the state space using selective scheduling based on a set of interleaving points that have been inferred in the previous step. We have developed three partitioning strategies for improved effectiveness and performance. We have implemented SIFT on top of the KLEE symbolic execution engine and applied it to various real-world and academic benchmarks. SIFT could detect more vulnerabilities than a state-of-the-art memory vulnerability detector.

As the number of Internet of Things (IoT) devices proliferate, an in-depth understanding of the IoT attack surface has become quintessential for dealing with the security and reliability risks. IoT devices and components execute implementations of various communication protocols. Vulnerabilities in the protocol stack implementations form an important part of the IoT attack surface. Therefore, finding memory errors in such implementations is essential for improving the IoT security and reliability. This paper presents a tool, SEESAW, that is built on top of a static analysis tool and a symbolic execution engine to achieve scalable analysis of protocol stack implementations. SEESAW leverages the API model of the analyzed code base to perform component-level analysis. SEESAW has been applied to the USB and Bluetooth modules within the Linux kernel. SEESAW can reproduce known memory vulnerabilities in a more scalable way compared to baseline symbolic execution.

The number of Internet of Things (IoT) has reached 7 billion globally in early 2018 and are nearly ubiquitous in daily life. Knowing whether or not these devices are safe and secure to use is becoming critical. IoT devices usually implement communication protocols such as USB and Bluetooth within firmware to allow a wide range of functionality. Thus analyzing firmware using domain knowledge from these protocols is vital to understand device behavior, detect implementation bugs, and identify malicious components. Unfortunately, due to the complexity of these protocols, there is usually no formal specification available that can help automate the firmware analysis; as a result significant manual effort is currently required to study these protocols and to reverse engineer the device firmware. In this paper, we propose a new firmware analysis methodology using symbolic execution called ProXray, which can learn a protocol model from known firmware, and apply the model to recognize the protocol relevant fields and detect functionality within unknown firmware automatically. After the training phase, ProXray can fully automate the firmware analysis process while supporting user's queries in the form of protocol relevant constraints. We have applied ProXray to the USB and the Bluetooth protocols by learning protocol constraint models from firmware that implement these protocols. We are then able to map protocol fields and identify USB functionality automatically within all 6 unknown USB firmware while achieving more than an order of magnitude speedup in reaching protocol relevant targets in unknown Bluetooth firmware. Our model achieved high coverage of the USB and Bluetooth specifications for several important protocol fields. ProXray provides a new method to apply domain knowledge to firmware analysis automatically.

Device drivers are critical components of operating systems. However, due to their interactions with the hardware and being embedded in complex programming models implemented by the operating system, ensuring reliability of device drivers remains to be a challenge. In this paper, we focus on the interaction of the driver with the device and present an approach for modeling this interaction and verifying absence of hardware-software data races. Specifically, we use the counting abstraction technique to abstract dynamic process creation in response to I/O acknowledgements sent by the device. We present the results of our approach on the modeling and verification of several Linux device driver models.

The USB protocol has become ubiquitous, supporting devices from high-powered computing devices to small embedded devices and control systems. USB's greatest feature, its openness and expandability, is also its weakness, and attacks such as BadUSB exploit the unconstrained functionality afforded to these devices as a vector for compromise. Fundamentally, it is virtually impossible to know whether a USB device is benign or malicious. This work introduces FirmUSB, a USB-specific firmware analysis framework that uses domain knowledge of the USB protocol to examine firmware images and determine the activity that they can produce. Embedded USB devices use microcontrollers that have not been well studied by the binary analysis community, and our work demonstrates how lifters into popular intermediate representations for analysis can be built, as well as the challenges of doing so. We develop targeting algorithms and use domain knowledge to speed up these processes by a factor of 7 compared to unconstrained fully symbolic execution. We also successfully find malicious activity in embedded 8051 firmwares without the use of source code. Finally, we provide insights into the challenges of symbolic analysis on embedded architectures and provide guidance on improving tools to better handle this important class of devices.

Complex software systems come with a huge number of configuration parameters for tuning their performance as well as functionality. It is a challenge for the users of such systems to understand how various parameters interact, and causing them to use the default configuration settings to avoid problems. Studies show that a lot of performance optimization opportunities are missed when complex software systems are run with the default configuration settings. This paper proposes a graph-based representation of configuration parameter interactions that are extracted using a scaleable static analysis approach. Experimental results obtained with a case study on a data analysis framework, Apache Hadoop, suggest that the proposed approach is effective in capturing some of the interactions at the component level.

In this paper we extend state machine diagrams with a programming concept that is highly utilized in real software: the callback mechanism. A callback is a way to interact with a library and can be instantiated in the form of synchronous or asynchronous mode. Using callbacks speeds up software development at the expense of complicating program comprehension. Introducing the callback concept to a modeling formalism preserves structural similarity between the model and the implementation. This paper presents a formal semantics for this extended formalism to make it amenable to formal verification and concurrency synthesis and to help developers avoid implementation mistakes such as race conditions and deadlocks. We report specification, verification, and synthesis case studies on a device driver.

According to Java's relaxed memory model, programs that contain data races need not be sequentially consistent. Executions that are not sequentially consistent may exhibit surprising behavior such as operations on a thread occurring in a different order than indicated by the source code or different threads having inconsistent views of updates of shared variables. Java Racefinder (JRF) is an extension of Java Pathfinder (JPF), a model checker for Java bytecode. JRF precisely detects data races as defined by the memory model and can thus be used to verify sequential consistency. We describe an extension to JRF, JRF-Eliminator (JRF-E), that analyzes information collected during model checking, specifically counterexample traces and acquiring histories, and provides advice to the programmer on how to eliminate detected data races from a program. If data races have been eliminated, standard model checking and other verification techniques that implicitly assume sequential consistency can be soundly employed to verify additional properties.

Most approaches to reasoning about multithreaded programs, including model checking, make the implicit assumption that the system being considered is sequentially consistent. This is, however, invalid in most modern computer architectures and results in unsound reasoning for programs that contain data races, where data races are defined by the memory model of the programming environment. We describe an extension to the model checker Java PathFinder that incorporates knowledge of the Java Memory Model to precisely detect data races in Java byte code. Our tool incorporates special purpose heuristic algorithms that result in shorter counterexample paths. Once data races have been eliminated from a program, Java PathFinder can be soundly employed to verify additional properties.

Action language verifier (ALV) is an infinite-state symbolic model checker. ALV can verify (or falsify, by generating counter-examples) temporal logic properties of systems that can be modeled using a combination of Boolean logic and linear arithmetic expressions on Boolean, enumerated and (possibly unbounded) integer variables and parameterized integer constants. In this paper, we apply ALV to the verification of parameterized hierarchical state machine specifications. We extend the standard notation for hierarchical state machines by introducing primitives for explicit specification of asynchronous processes and their finite and parameterized instantiations. We define the formal semantics of these primitives, where the states of the parameterized processes are mapped to integer variables using the counting abstraction technique. We apply the presented approach to the specification and analysis of an airport ground traffic controller and verify several correctness properties of this specification using ALV.

Run-time errors in concurrent programs are generally due to the wrong usage of synchronization primitives such as monitors. Conventional validation techniques such as testing become ineffective for concurrent programs since the state space increases exponentially with the number of concurrent processes. In this paper, we propose an approach in which 1) the concurrency control component of a concurrent program is formally specified, 2) it is verified automatically using model checking, and 3) the code for concurrency control component is automatically generated. We use monitors as the synchronization primitive to control access to a shared resource by multipleconcurrent processes. Since our approach decouples the concurrency control component from the rest of the implementation it is scalable. We demonstrate the usefulness of our approach by applying it to a case study on Airport Ground Traffic Control.We use the Action Language to specify the concurrency control component of a system. Action Language is a specification language for reactive software systems. It is supported by an infinite-state model checker that can verify systems with boolean, enumerated and udbounded integer variables. Our code generation tool automatically translates the verified Action Language specification into a Java monitor. Our translation algorithm employs symbolic manipulation techniques and the specific notification pattern to generate an optimized monitor class by eliminating the context switch overhead introduced as a result of unnecessary thread notification. Using counting abstraction, we show that we can automatically verify the monitor specifications for arbitrary number of threads.

Action Language is a specification language for reactive software systems. We present the Action Language Verifier which consists of: 1) a compiler that converts Action Language specifications to composite symbolic representations, and 2) an infinite-state symbolic model checker which verifies (or falsifies) CTL properties of Action Language specifications. Our symbolic manipulator (Composite Symbolic Library) combines a BDD manipulator (for boolean and enumerated types) and a Presburger arithmetic manipulator (for integers) to handle multiple variable types. Since we allow unbounded integer variables, model checking queries become undecidable. We present several heuristics used by the Action Language Verifier to achieve convergence.