Navigating Emerging Complexities of Modern Systems: Advancements in Automated Verification and Security Techniques

Abstract

The increasing design complexity at the end of Moore’s Law and Dennard Scaling presents a new challenge for implementing modern systems correctly and securely. This dissertation presents focused efforts for advancing automated verification and security techniques to mitigate incorrect implementations and attackers, respectively. It explores two avenues: 1) correctness verification in virtual memory systems, where shared memory interactions occur across hardware and system-level events, and 2) enhancing security of heterogeneous systems-on-a-chip (SoCs) with anomalous activity detection and localization. In the first thrust, this dissertation develops tools for a systematic, end-to-end formalized approach for verifying and validating virtual memory system implementations using memory transistency model (MTM) specifications. First, I propose a novel formal language for reasoning about MTMs, enabling specification of the software-visible impacts of complex hardware- and system-level interactions that occur in parallel systems with virtual memory. Next, I present empirical MTM testing techniques for verification and validation on real system implementations using specialized stress measures to coax out MTM-specific bugs. The proposed techniques can alleviate complex system verification efforts by automating detection of bugs and vulnerabilities at the hardware-system interface of virtual memory systems. The second thrust of this dissertation develops processes to enhance security of heterogeneous SoC designs. Sophisticated attacks can take down parts of the SoC, resulting in diminished performance gains and failed processes. To design built-in defenses against such attacks, this dissertation proposes the use of network-on-chip (NoC) based hardware counters to monitor ongoing SoC activity in a holistic fashion. With these counters, I develop and demonstrate an anomalous activity detection and localization system to detect and pinpoint availability attacks on SoC components, leveraging machine learning techniques and the inherent interpretability offered by the NoC counters. These techniques enable automated attack and failure detection to be built into the SoC, a particularly valuable feature in the fast-changing heterogeneous SoC design space. Overall, this dissertation advocates for the use of formal and empirical modeling tools to effectively capture complex system behaviors such that vulnerabilities, bugs, and threats can be detected at design time and runtime with automated methods that provide elevated coverage and accuracy.