Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userMining Secure Behavior of Hardware Designs
79
0
0.0
(
0
)
Added by
Calvin Deutschbein
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Authors
Calvin Deutschbein
Ask ChatGPT about the research
No Arabic abstract
Specification mining offers a solution by automating security specification for hardware. Specification miners use a form of machine learning to specify behaviors of a system by studying a system in execution. However, specification mining was first developed for use with software. Complex hardware designs offer unique challenges for this technique. Further, specification miners traditionally capture functional specifications without a notion of security, and may not use the specification logics necessary to describe some security requirements. This work demonstrates specification mining for hardware security. On CISC architectures such as x86, I demonstrate that a miner partitioning the design state space along control signals discovers a specification that includes manually defined properties and, if followed, would secure CPU designs against Memory Sinkhole and SYSRET privilege escalation. For temporal properties, I demonstrate that a miner using security specific linear temporal logic (LTL) templates for specification detection may find properties that, if followed, would secure designs against historical documented security vulnerabilities and against potential future attacks targeting system initialization. For information--flow hyperproperties, I demonstrate that a miner may use Information Flow Tracking (IFT) to develop output properties containing designer specified information--flow security properties as well as properties that demonstrate a design does not contain certain Common Weakness Enumerations (CWEs).
rate research
Read More
We present a methodology for creating information flow specifications of hardware designs. Such specifications can help designers better understand their design and are necessary for security validation processes. By combining information flow tracking and specification mining, we are able to produce information flow properties of a design without prior knowledge of security agreements or specifications. We develop a tool, Isadora, to evaluate our methodology. We demonstrate Isadora may define the information flows within an access control module in isolation and within an SoC and over a RISC-V design. Over the access control module, Isadora mined output completely covers an assertion based security specification of the design provided by the designers. For both the access control module and RISC-V, we sample Isadora output properties and find 10 out of 10 and 8 out of 10 properties, respectively, define the design behavior to relevant to a Common Weakness Enumeration (CWE). We find our methodology may independently mine security properties manually developed by hardware designers, automatically generate properties describing CWEs over a design, and scale to SoC and CPU designs.
Since the discovery of Spectre, a large number of hardware mechanisms for secure speculation has been proposed. Intuitively, more defensive mechanisms are less efficient but can securely execute a larger class of programs, while more permissive mechanisms may offer more performance but require more defensive programming. Unfortunately, there are no hardware-software contracts that would turn this intuition into a basis for principled co-design. In this paper, we put forward a framework for specifying such contracts, and we demonstrate its expressiveness and flexibility. On the hardware side, we use the framework to provide the first formalization and comparison of the security guarantees provided by a representative class of mechanisms for secure speculation. On the software side, we use the framework to characterize program properties that guarantee secure co-design in two scenarios traditionally investigated in isolation: (1) ensuring that a benign program does not leak information while computing on confidential data, and (2) ensuring that a potentially malicious program cannot read outside of its designated sandbox. Finally, we show how the properties corresponding to both scenarios can be checked based on existing tools for software verification, and we use them to validate our findings on executable code.
The widening availability of hardware-based trusted execution environments (TEEs) has been accelerating the adaptation of new applications using TEEs. Recent studies showed that a cloud application consists of multiple distributed software modules provided by mutually distrustful parties. The applications use multiple TEEs (enclaves) communicating through software-encrypted memory channels. Such execution model requires bi-directional protection: protecting the rest of the system from the enclave module with sandboxing and protecting the enclave module from a third-part module and operating systems. However, the current TEE model, such as Intel SGX, cannot efficiently represent such distributed sandbox applications. To overcome the lack of hardware supports for sandboxed TEEs, this paper proposes an extended enclave model called Stockade, which supports distributed sandboxes hardened by hardware. Stockade proposes new three key techniques. First, it extends the hardware-based memory isolation in SGX to confine a user software module only within its enclave. Second, it proposes a trusted monitor enclave that filters and validates systems calls from enclaves. Finally, it allows hardware-protected memory sharing between a pair of enclaves for efficient protected communication without software-based encryption. Using an emulated SGX platform with the proposed extensions, this paper shows that distributed sandbox applications can be effectively supported with small changes of SGX hardware.
Privacy and security-related concerns are growing as machine learning reaches diverse application domains. The data holders want to train with private data while exploiting accelerators, such as GPUs, that are hosted in the cloud. However, Cloud systems are vulnerable to attackers that compromise the privacy of data and integrity of computations. This work presents DarKnight, a framework for large DNN training while protecting input privacy and computation integrity. DarKnight relies on cooperative execution between trusted execution environments (TEE) and accelerators, where the TEE provides privacy and integrity verification, while accelerators perform the computation heavy linear algebraic operations.
Secure Function Evaluation (SFE) has received recent attention due to the massive collection and mining of personal data, but remains impractical due to its large computational cost. Garbled Circuits (GC) is a protocol for implementing SFE which can evaluate any function that can be expressed as a Boolean circuit and obtain the result while keeping each partys input private. Recent advances have led to a surge of garbled circuit implementations in software for a variety of different tasks. However, these implementations are inefficient and therefore GC is not widely used, especially for large problems. This research investigates, implements and evaluates secure computation generation using a heterogeneous computing platform featuring FPGAs. We have designed and implemented SIFO: Secure computational Infrastructure using FPGA Overlays. Unlike traditional FPGA design, a coarse grained overlay architecture is adopted which supports mapping SFE problems that are too large to map to a single FPGA. Host tools provided include SFE problem generator, parser and automatic host code generation. Our design allows re-purposing an FPGA to evaluate different SFE tasks without the need for reprogramming, and fully explores the parallelism for any GC problem. Our system demonstrates an order of magnitude speedup compared with an existing software platform.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
