상세정보
Export to Refworks부가기능
Concurrency and Security Verification in Heterogeneous Parallel Systems
상세 프로파일
| 자료유형 | 학위논문 |
|---|---|
| 서명/저자사항 | Concurrency and Security Verification in Heterogeneous Parallel Systems. |
| 개인저자 | Trippel, Caroline June. |
| 단체저자명 | Princeton University. Computer Science. |
| 발행사항 | [S.l.]: Princeton University., 2019. |
| 발행사항 | Ann Arbor: ProQuest Dissertations & Theses, 2019. |
| 형태사항 | 215 p. |
| 기본자료 저록 | Dissertations Abstracts International 81-06B. Dissertation Abstract International |
| ISBN | 9781392771198 |
| 학위논문주기 | Thesis (Ph.D.)--Princeton University, 2019. |
| 일반주기 |
Source: Dissertations Abstracts International, Volume: 81-06, Section: B.
Advisor: Martonosi, Margaret. |
| 이용제한사항 | This item must not be sold to any third party vendors. |
| 요약 | To achieve performance scaling at manageable power and thermal levels, modern systems architects employ parallelism along with high degrees of hardware specialization and heterogeneity. Unfortunately, the power and performance improvements afforded by heterogeneous parallelism come at the cost of significantly increased design complexity, with different components being programmed differently and accessing shared resources differently. This design complexity in turn presents challenges for architects who need to devise mechanisms for orchestrating, enforcing, and verifying the correctness and security of executing applications. As it turns out, software-level correctness and security problems can result from problematic hardware event orderings and interleavings that take place when an application executes on a particular hardware implementation. Since hardware designs are complex, and since a single user-facing instruction can exhibit a variety of different hardware execution event sequences, analyzing and verifying systems for correct and secure orderings and interleavings of these events is challenging. To address this issue, this dissertation combines hardware systems architecture approaches with formal methods techniques to support the specification, analysis, and verification of implementation-aware event ordering scenarios. The specific goal here is enabling automatic synthesis of implementation-aware programs capable of violating correctness or security guarantees when such programs exist. First, this dissertation presents TriCheck, an approach and tool for conducting full-stack memory consistency model verification (from high-level programming languages down through hardware implementations). Using rigorous and efficient formal approaches, TriCheck identified flaws in the 2016 RISC-V memory model specification and two counterexamples to a previously proven-correct compiler mapping scheme from C11 onto Power and ARMv7. Second, after making the important observation that memory consistency model and security analyses are amenable to similar approaches, this thesis presents CheckMate, an approach and tool for conducting hardware security verification. CheckMate uses formal techniques to evaluate susceptibility of a hardware system design to formally-specified security exploit classes. When a design is susceptible, proof-of-concept exploit codes are synthesized. CheckMate automatically synthesized programs representative of Meltdown and Spectre and new exploits, MeltdownPrime and SpectrePrime. Third, this dissertation presents approaches for handling memory model heterogeneity in hardware systems, focusing on correctness and highlighting applicability of the proposed techniques to security. |
| 일반주제명 | Computer science. Computer engineering. |
| 언어 | 영어 |
| 바로가기 | 
: 이 자료의 원문은 한국교육학술정보원에서 제공합니다. |
