Prof. Christopher Fletcher (UIUC), Dr. Frank McKeen (Intel), Prof. Edward Suh (Cornell), and I served as panelists for the 2020 ISCA Security Mini-Panel. This blog post reflects on our panel discussion.
The security of modern applications is underpinned by the security of the hardware on which these applications are run. Thus, there has been a rise in hardware security papers appearing in architecture and security conferences in recent years (Figures 1 and 2). Given the current scope and distribution of architecture security research topics (discussed below), the panel voiced several claims regarding future important architecture research directions.
Claim 1: Computer architects have the most authority when it comes to discovering new hardware exploits and should devote more attention to novel attack research.
Figure 3 illustrates that hardware security research in the security community is largely attack-based. During the panel discussion, Prof. Fletcher quoted a colleague in the security community whose research is devoted to attack discovery, saying “Right now we are engaged in pure science, akin to dissecting a frog. But, in this case, this frog actually is the product of intelligent design.” This exposes a couple key features of security community attack research. First, it highlights a dependency on reverse engineering black-box hardware designs. Second, and more subtly, it implies that mainstream products are generally the target of attack development.
The panelists argued that the creators of the “frog” in the above analogy are the most well-equipped to identify new fundamental hardware vulnerabilities (in contrast to the blackbox approach). Moreover, vulnerabilities that are discovered post-fabrication, are difficult if not impossible to patch. Thus, computer architects should engage in offensive attack research and seek to identify fundamentally new vulnerabilities [1] [2] in contrast to the current defense-focused trends summarized in Figure 4.
Claim 2: Security should be a first-order hardware design constraint, alongside performance and power.
For a given hardware implementation, we must be able to detect the presence of hardware security vulnerabilities that are capable of violating application-level security requirements. Taking confidentiality as an example of a security requirement, this amounts to determining whether or not a particular hardware implementation can induce application-level information leakage. Furthermore, once a vulnerability is identified and isolated, we must determine the extent to which the vulnerability may be exploited by an adversary to compromise victim application security. This involves considering, for example, the probability of attack success or the fidelity of a side channel [3] and is necessary if designers wish to trade off security for performance in a reasonable way.
Researchers are actively exploring ways in which hardware susceptibility to exploits can be detected, through artisanal exploit generation, novel benchmark suites (e.g., [4]), and formal methods approaches (e.g., [5] [6] [7] [8]). However, reasoning about the second question above is critical for high-performance security and for reasoning about the validity of security solutions that enable users to adjust a security-performance knob.
Claim 3: Formal methods techniques are paramount in enabling hardware architects to discover new attacks and to evaluate the security of their proposed designs.
Figures 3 and 4 show that from 2015-2019, only about 19% hardware security research in both the architecture and security communities focused on verification, including heuristic- and testing-based approaches. Due to the complexity of modern hardware systems and the sophistication of modern exploits, amplifying verification efforts, particularly with the aid of formal automated reasoning tools, is crucial.
Architects should devote attention to solving challenges surrounding efficiently (and ideally automatically) constructing accurate formalisms of hardware systems and security properties which are a prerequisite for using automated reasoning in hardware security verification. These efforts are also applicable to Claim 1, which specifies that architects should focus on developing novel attacks. Formal methods support directly comparing attacks and defining attack uniqueness based on the security properties that a given attack violates.
Finally, the panelists agreed that the importance of formal verification for security is great enough that architects should be designing hardware and hardware security solutions that are amenable to efficient analysis with formal techniques. Moreover, the algorithmic requirements of hardware security verification can and should inspire the design of new formal analysis approaches (e.g., new domain-specific theories for SMT solvers).
Claim 4: Architects should be developing new hardware-software contracts for security.
There is a current gap in understanding between hardware security guarantees and application-level security requirements. Most notably, a variety of side-channel attacks have demonstrated that architecturally-visible state is not limited to state that can be accessed directly via user-facing instructions, but rather also includes state that can be detected. This observation motivates the development of new interface specifications that facilitate more precise security reasoning at higher levels of the hardware software stack.
Given some of my own prior work on memory consistency model verification, I have observed many commonalities between memory consistency models and what we would want in a security counterpart. First, both are necessary due to the combination of particular hardware optimizations—e.g., out-of-order execution in the case of memory models and data/control-dependent fast and slow paths in the case of security—in the presence of shared system resources. Moreover, both expose hardware-specific execution behaviors that must be prevented in the (likely) uncommon case when they are required for application reliability and security—e.g., event reordering for memory models and information leakage for security.
Researchers are exploring potential architectural interfaces for security [9] [10] [11] [12] [13], some of which expose a notion of execution time to software. Regardless of the mechanism, robust interface specifications that expose security-critical hardware behaviors to software, along with appropriate safety-nets to regain “strong” security guarantees when necessary, are essential. Furthermore, if we can formally define interface specifications for security, these can serve as verification properties for hardware and even secure compilation.
Claim 5: Just as when optimizing for performance and power, architects should consider the features and requirements of important applications when designing hardware security solutions.
The implications of this final claim are two-fold. First, there is an opportunity for hardware security researchers to develop performance- and power-optimal security solutions by closely tailoring hardware threat model support to application threat model requirements. Different applications might have different security requirements depending on what data they process, how they process that data, and how they might interact with other applications during their deployment. Interface specifications for reasoning about security guarantees of programs will likely play a major role in facilitating reasoning about application-specific security whereby system security protections are deployed in a way that optimally supports application security requirements.
Second, modern heterogeneous cloud deployment scenarios present new challenges to hardware security support and verification. For example, data center disaggregation and serverless computing paradigms provide more opportunities for applications to interact during their execution on cloud platforms. Current models of attestation used by commercial enclave technologies were not designed to operate in this setting. Moreover, heterogeneous computing devices such as accelerators were not designed with security in mind and present new challenges regarding verifying their interaction with software and other system components [14]. Finally, processors have a long shelf life. Hardware security solutions should ideally be amenable to an evolving threat model and new adversaries.
About the Author: Caroline Trippel is an Assistant Professor of Computer Science and Electrical Engineering at Stanford University. Her research on architectural concurrency and security verification has been recognized with IEEE Top Picks distinctions and the 2020 ACM SIGARCH/IEEE CS TCCA Outstanding Dissertation Award.
Data Disclaimer: The data featured in Figures 1-4 in this blog post was collected by parsing paper titles from ISCA, ASPLOS, MICRO, HPCA, USENIX Security, CCS, and S&P conference proceedings from 2015-2019. Since not all conferences have released 2020 proceedings, 2020 was not included. Paper titles were parsed automatically for hardware security keywords and then manually inspected for accuracy. While the data represents useful estimates, it is possible some relevant papers were missed or misclassified due to the human-in-the-loop. This further motivates the need for fully-automated formal hardware security verification 🙂
Disclaimer: These posts are written by individual contributors to share their thoughts on the Computer Architecture Today blog for the benefit of the community. Any views or opinions represented in this blog are personal, belong solely to the blog author and do not represent those of ACM SIGARCH or its parent organization, ACM.