Intel SGX promises powerful security: an arbitrary number of user-mode enclaves protected against physical attacks and privileged software adversaries. However, to achieve this, Intel extended the x86 architecture with an isolation mechanism approaching the complexity of an OS microkernel, implemented by an inscrutable mix of silicon and microcode. While hardware-based security can offer performance and features that are difficult or impossible to achieve in pure software, hardware-only solutions are difficult to update, either to patch security flaws or introduce new features.
Komodo illustrates an alternative approach to attested, on-demand, user-mode, concurrent isolated execution. We decouple the core hardware mechanisms such as memory encryption, address-space isolation and attestation from the management thereof, which Komodo delegates to a privileged software monitor that in turn implements enclaves. The monitor's correctness is ensured by a machine-checkable proof of both functional correctness and high-level security properties of enclave integrity and confidentiality. We show that the approach is practical and performant with a concrete implementation of a prototype in verified assembly code on ARM TrustZone. Our ultimate goal is to achieve security equivalent to or better than SGX while enabling deployment of new enclave features independently of CPU upgrades.
The Komodo specification, prototype implementation, and proofs are available at https://github.com/Microsoft/Komodo.
more »
« less
Evaluating Security Specification Mining for a CISC Architecture
Security specification mining is a relatively new line of research that aims to develop a set of security properties for use during the design validation phase of the hardware life-cycle. Prior work in this field has targeted open-source RISC architectures and relies on access to the register transfer level design, developers’ repositories, bug tracker databases, and email archives. We develop Astarte, a tool for security specification mining of closed source, CISC architectures. As with prior work, we target properties written at the instruction set architecture (ISA) level. We use a full-system fast emulator with a lightweight extension to generate trace data, and we partition the space of security properties on security-critical signals in the architecture to manage complexity. We evaluate the approach for the x86-64 ISA. The Astarte framework produces roughly 1300 properties. Our automated approach produces a categorization that aligns with prior manual efforts. We study two known security flaws in shipped x86/x86-64 processor implementations and show that our set of properties could have revealed the flaws. Our analysis provides insight into those properties that are guaranteed by the ISA, those that are required of the operating system, and those that have become de facto properties by virtue of many operating systems assuming the behavior.
more »
« less
- Award ID(s):
- 1816637
- NSF-PAR ID:
- 10207543
- Date Published:
- Journal Name:
- 2020 IEEE Hardware Oriented Security and Trust (HOST)
- Page Range / eLocation ID:
- 164 to 175
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Sorting data is needed in many application domains. Traditionally, the data is read from memory and sent to a general-purpose processor or application-specific hardware for sorting. The sorted data is then written back to the memory. Reading/writing data from/to memory and transferring data between memory and processing unit incur significant latency and energy overhead. In this work, we develop the first architectures for in-memory sorting of data to the best of our knowledge. We propose two architectures. The first architecture is applicable to the conventional format of representing data, i.e., weighted binary radix. The second architecture is proposed for developing unary processing systems, where data is encoded as uniform unary bit-streams. As we present, each of the two architectures has different advantages and disadvantages, making one or the other more suitable for a specific application. However, the common property of both is a significant reduction in the processing time compared to prior sorting designs. Our evaluations show on average 37 × and 138 × energy reduction for binary and unary designs, respectively, compared to conventional CMOS off-memory sorting systems in a 45nm technology. We designed a 3 × 3 and a 5 × 5 Median filter using the proposed sorting solutions, which we used for processing 64 × 64 pixel images. Our results show a reduction of 14 × and 634 × in energy and latency, respectively, with the proposed binary, and 5.6 × and 152 × 10 3 in energy and latency with the proposed unary approach compared to those of the off-memory binary and unary designs for the 3 × 3 Median filtering system.more » « less
-
Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. Mozilla, for example, uses SFI to harden the Firefox browser by sandboxing third-party libraries, and companies like Fastly and Cloudflare use SFI to safely co-locate untrusted tenants on their edge clouds. While there have been significant efforts to optimize and verify SFI enforcement, context switching in SFI systems remains largely unexplored: almost all SFI systems use heavyweight transitions that are not only error-prone but incur significant performance overhead from saving, clearing, and restoring registers when context switching. We identify a set of zero-cost conditions that characterize when sandboxed code has sufficient structured to guarantee security via lightweight zero-cost transitions (simple function calls). We modify the Lucet Wasm compiler and its runtime to use zero-cost transitions, eliminating the undue performance tax on systems that rely on Lucet for sandboxing (e.g., we speed up image and font rendering in Firefox by up to 29.7% and 10% respectively). To remove the Lucet compiler and its correct implementation of the Wasm specification from the trusted computing base, we (1) develop a static binary verifier , VeriZero, which (in seconds) checks that binaries produced by Lucet satisfy our zero-cost conditions, and (2) prove the soundness of VeriZero by developing a logical relation that captures when a compiled Wasm function is semantically well-behaved with respect to our zero-cost conditions. Finally, we show that our model is useful beyond Wasm by describing a new, purpose-built SFI system, SegmentZero32, that uses x86 segmentation and LLVM with mostly off-the-shelf passes to enforce our zero-cost conditions; our prototype performs on-par with the state-of-the-art Native Client SFI system.more » « less
-
USB-based attacks have increased in complexity in recent years. Modern attacks now incorporate a wide range of attack vectors, from social engineering to signal injection. To address these challenges, the security community has responded with a growing set of fragmented defenses. In this work, we survey and categorize USB attacks and defenses, unifying observations from both peer-reviewed research and industry. Our systematization extracts offensive and defensive primitives that operate across layers of communication within the USB ecosystem. Based on our taxonomy, we discover that USB attacks often abuse the trust-by-default nature of the ecosystem, and transcend different layers within a software stack; none of the existing defenses provide a complete solution, and solutions expanding multiple layers are most effective. We then develop the first formal verification of the recently released USB Type- C Authentication specification, and uncover fundamental flaws in the specification's design. Based on the findings from our systematization, we observe that while the spec has successfully pinpointed an urgent need to solve the USB security problem, its flaws render these goals unattainable. We conclude by outlining future research directions to ensure a safer computing experience with USB.more » « less
-
null (Ed.)Despite its potential to overcome the design and processing barriers of traditional subtractive and formative manufacturing techniques, the use of laser powder bed fusion (LPBF) metal additive manufacturing is currently limited due to its tendency to create flaws. A multitude of LPBF-related flaws, such as part-level deformation, cracking, and porosity are linked to the spatiotemporal temperature distribution in the part during the process. The temperature distribution, also called the thermal history, is a function of several factors encompassing material properties, part geometry and orientation, processing parameters, placement of supports, among others. These broad range of factors are difficult and expensive to optimize through empirical testing alone. Consequently, fast and accurate models to predict the thermal history are valuable for mitigating flaw formation in LPBF-processed parts. In our prior works, we developed a graph theory-based approach for predicting the temperature distribution in LPBF parts. This mesh-free approach was compared with both non-proprietary and commercial finite element packages, and the thermal history predictions were experimentally validated with in- situ infrared thermal imaging data. It was found that the graph theory-derived thermal history predictions converged within 30–50% of the time of non-proprietary finite element analysis for a similar level of prediction error. However, these prior efforts were based on small prismatic and cylinder-shaped LPBF parts. In this paper, our objective was to scale the graph theory approach to predict the thermal history of large volume, complex geometry LPBF parts. To realize this objective, we developed and applied three computational strategies to predict the thermal history of a stainless steel (SAE 316L) impeller having outside diameter 155 mm and vertical height 35 mm (700 layers). The impeller was processed on a Renishaw AM250 LPBF system and required 16 h to complete. During the process, in-situ layer-by-layer steady state surface temperature measurements for the impeller were obtained using a calibrated longwave infrared thermal camera. As an example of the outcome, on implementing one of the three strategies reported in this work, which did not reduce or simplify the part geometry, the thermal history of the impeller was predicted with approximate mean absolute error of 6% (standard deviation 0.8%) and root mean square error 23 K (standard deviation 3.7 K). Moreover, the thermal history was simulated within 40 min using desktop computing, which is considerably less than the 16 h required to build the impeller part. Furthermore, the graph theory thermal history predictions were compared with a proprietary LPBF thermal modeling software and non-proprietary finite element simulation. For a similar level of root mean square error (28 K), the graph theory approach converged in 17 min, vs. 4.5 h for non-proprietary finite element analysis.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1109/HOST45689.2020.9300291
