55 research outputs found
Developing secure SGX enclaves: New challenges on the horizon
No full textThe combination of (1) hard to eradicate low-level vulnerabilities, (2) a large trusted computing base written in a memory-unsafe language and (3) a desperate need to provide strong software security guarantees, led to the development of protected-module architectures. Such architectures provide strong isolation of protected modules: Security of code and data depends only on a module's own implementation.
In this paper we discuss how such protected modules should be written. From an academic perspective it is clear that the future lies with memory-safe languages. Unfortunately, from a business and management perspective, that is a risky path and will remain so in the near future. The use of well-known but memory-unsafe languages such as C and C++ seem inevitable.
We argue that the academic world should take another look at the automatic hardening of software written in such languages to mitigate low-level security vulnerabilities. This is a well-studied topic for full applications, but protected-module architectures introduce a new, and much more challenging environment. Porting existing security measures to a protected-module setting without a thorough security analysis may even harm security of the protected modules they try to protect.sponsorship: Raoul Strackx holds a Postdoctoral mandate from the Research Foundation Flanders (FWO). This research is partially funded by the Research Fund KU Leuven, and by the Research Fund -Flanders (FWO). (Research Foundation Flanders (FWO) - Research Fund KU Leuven, Research Fund -Flanders (FWO))status: Publishe
Nemesis: Studying microarchitectural timing leaks in rudimentary CPU interrupt logic
No full text© 2018 Copyright held by the owner/author(s). Recent research on transient execution vulnerabilities shows that current processors exceed our levels of understanding. The prominent Meltdown and Spectre attacks abruptly revealed fundamental design flaws in CPU pipeline behavior and exception handling logic, urging the research community to systematically study attack surface from microarchitectural interactions. We present Nemesis, a previously overlooked side-channel attack vector that abuses the CPU’s interrupt mechanism to leak microarchitectural instruction timings from enclaved execution environments such as Intel SGX, Sancus, and TrustLite. At its core, Nemesis abuses the same subtle microarchitectural behavior that enables Meltdown, i.e., exceptions and interrupts are delayed until instruction retirement. We show that by measuring the latency of a carefully timed interrupt, an attacker controlling the system software is able to infer instruction-granular execution state from hardware-enforced enclaves. In contrast to speculative execution vulnerabilities, our novel attack vector is applicable to the whole computing spectrum, from small embedded sensor nodes to high-end commodity x86 hardware. We present practical interrupt timing attacks against the open-source Sancus embedded research processor, and we show that interrupt latency reveals microarchitectural instruction timings from off-the-shelf Intel SGX enclaves. Finally, we discuss challenges for mitigating Nemesis-type attacks at the hardware and software levels.sponsorship: We thank Job Noorman for guidance on the Sancus secure interrupt extensions, and Pieter Maene for valuable feedback on early versions of this text. The research presented in this paper was partially supported by the Research Fund KU Leuven, and by a gift from Intel Corporation. Jo Van Bulck and Raoul Strackx are supported by a grant of the Research Foundation - Flanders (FWO). (Research Fund KU Leuven, Research Foundation - Flanders (FWO))status: Publishe
Automatically generating secure wrappers for SGX enclaves from separation logic specifications
No full textIntel Software Guard Extensions (SGX) is a recent technology from Intel that makes it possible to execute security-critical parts of an application in a so-called SGX enclave, an isolated area of the system that is shielded from all other software (including the OS and/or hypervisor). SGX was designed with the objective of making it relatively straightforward to take a single module of an existing C application, and put that module in an enclave. The SGX SDK includes tooling to semi-automatically generate wrappers for an enclaved C module. The wrapped enclave can then easily be linked to the legacy application that uses the module.
However, when the enclaved module and the surrounding application share a part of the heap and exchange pointers (a very common case in C programs), the generation of these wrappers requires programmer annotations and is error-prone – it is easy to introduce security vulnerabilities or program crashes.
This paper proposes a separation logic based language for specifying the interface of the enclaved C module, and shows how such an interface specification can be used to automatically generate secure wrappers that avoid these vulnerabilities and crashes.sponsorship: Raoul Strackx holds a Postdoctoral mandate from the Research Foundation - Flanders (FWO). This research is partially funded by project grants from the Research Fund KU Leuven, and from the Research Foundation - Flanders (FWO). (Research Fund KU Leuven, Research Foundation - Flanders (FWO))status: Publishe
Mitigating password database breaches with Intel SGX
No full textIn order to prevent rainbow attacks against a stolen password database, most passwords are appended with a unique salt before hashing them as to make the password random and more secure. However, the decreasing cost of hardware has made it feasible to perform brute force attacks by guessing the passwords (even when extended with their salt).
Recently Intel has made processors with Intel SGX commercially available. This security technology enables developers to (1) completely isolate code and data running in an SGX enclave from untrusted code running at any privilege layer and (2) prevent data sealed to an enclave from being accessed on any other machine.
We propose to add a key to the password (and salt) before they are hashed. By calculating the hash within an enclave, the key never leaves the enclave. This provides much stronger protection; offline attacks are infeasible without knowledge of the key. Online attacks on the other hand are much easier to defend against.sponsorship: Raoul Strackx holds a Postdoctoral mandate from the Research Foundation Flanders (FWO). This research is partially funded by the Research Fund KU Leuven, and by the Research Fund -Flanders (FWO). (Research Foundation Flanders (FWO) - Research Fund KU Leuven, Research Fund -Flanders (FWO))status: Publishe
Off-limits: Abusing legacy x86 memory segmentation to spy on enclaved execution
No full text© Springer International Publishing AG, part of Springer Nature 2018. Enclaved execution environments, such as Intel SGX, enable secure, hardware-enforced isolated execution of critical application components without having to trust the underlying operating system or hypervisor. A recent line of research, however, explores innovative controlled-channel attacks mounted by untrusted system software to partially compromise the confidentiality of enclave programs. Apart from exploiting relatively well-known side-channels like the CPU cache and branch predictor, these attacks have so far focused on tracking side-effects from enclaved address translations via the paging unit. This paper shows, however, that for 32-bit SGX enclaves the unacclaimed x86 segmentation unit can be abused as a novel controlled-channel to reveal enclaved memory accesses at a page-level granularity, and in restricted circumstances even at a very precise byte-level granularity. While the x86 paging unit has been extensively studied from both an attack as well as a defense perspective, we are the first to show that address translation side-channels are not limited to paging. Our findings furthermore confirm that largely abandoned legacy x86 processor features, included for backwards compatibility, suggest new and unexpected side-channels.sponsorship: This work was partially supported by the Research Fund KU Leuven. Jo Van Bulck and Raoul Strackx are supported by a grant of the Research Foundation - Flanders (FWO). (Research Fund KU Leuven, Research Foundation - Flanders (FWO))status: Publishe
Securely deploying distributed computation systems on peer-to-peer networks
No full text© 2019 Association for Computing Machinery. More and more off-the-shelf processors support the dynamic construction of Trusted Execution Environments. For instance, Intel Software Guard Extensions (Intel SGX) supports the construction of so-called enclaves on modern Intel Core processors. Hence, it is interesting to design and evaluate practical security architectures that leverage this new technology. One of the possibilities of this new technology is that it enables deployment of traditional distributed applications that require a group of mutually trusting machines, on top of a group of mutually distrusting machines such as a peer-to-peer network. This paper proposes and evaluates an Intel SGX based approach to securely deploy a subset of distributed systems called distributed computation systems in a peer-to-peer fashion, with strong confidentiality and integrity guarantees and without modification of the original system. The approach is evaluated by applying it to distcc, a distributed compiler. This result of this process is a new program called p2pcc, a distributed peer-to-peer compiler. We created two different versions of p2pcc. In the first version, any process spawned on one of the untrusted peers runs in its own enclave, thus providing a very fine-grained form of isolation. Our evaluation shows that the performance cost on today's Intel SGX implementation is too high. The second version of p2pcc groups all processes running on behalf of the same user within the same enclave, thus providing coarser isolation, but still providing strong isolation on all security boundaries. Our evaluation shows that the second approach has good performance while providing strong security guarantees even on current SGX processors. Our results provide evidence that deploying existing distributed computation systems in a peer-to-peer fashion is practical.sponsorship: The research presented in this paper was partially supported by the Research Fund KU Leuven, and by a gift from Intel Corporation. Raoul Strackx is supported by a grant of the Research Foundation - Flanders (FWO). (Research Fund KU Leuven, Research Foundation - Flanders (FWO))status: Publishe
Secure compilation to modern processors
No full textWe present a secure (fully abstract) compilation scheme to compile an object-based high-level language to low-level machine code. Full abstraction is achieved by relying on a fine-grained program counter-based memory access protection scheme, which is part of our low-level target language. We discuss why standard compilers fail to provide full abstraction and introduce enhancements needed to achieve this goal. We prove that our enhanced compilation scheme provides full abstraction from our high-level source language to our low-level target language. Lastly, we show by means of a prototype implementation that our low-level language with fine-grained memory access control can be realized efficiently on modern commodity platforms.sponsorship: This research is partially funded by the Research Fund
K.U.Leuven and the EU-funded FP7-project NESSoS. Pieter
Agten is a Ph.D. fellow of the Fund for Scientific Research
- Flanders (FWO). Raoul Strackx is a Ph.D. fellow of the
agency for Innovation by Science and Technology (IWT).status: Publishe
Security guarantees for the execution infrastructure of software applications
No full text© 2016 IEEE. Software applications run on top of infrastructure consisting of hardware (processors, devices, communication networks,⋯) and software (operating systems, compilers, virtual machines, language runtimes, databases,⋯). In many cases, attacks against application software rely at least to some extent on aspects of that infrastructure, and in some cases vulnerabilities can be fixed by strengthening the infrastructure, as well as by patching the application code. This paper argues that it is beneficial for secure software development if the security guarantees offered by the execution infrastructure are explicit and precisely defined. More specifically, a developer writing source code that will be executed on the infrastructure should know what guarantees the infrastructure offers against what class of attackers. We survey existing proposals for precise statements of such security guarantees, and argue that the notion of full abstraction proposed by Martin Abadi as a correctness condition for secure implementation of abstractions is the key notion for specifying security guarantees of execution infrastructure. We give a brief overview of how full abstraction has already been used to specify and prove security for important building blocks of an execution infrastructure, and we sketch a research agenda identifying several interesting open research problems that, when solved, could contribute to a more secure design of execution infrastructure for distributed software applications, and to a better understanding of the security properties of these infrastructures.sponsorship: This research is partially funded by the Research Fund KU Leuven and by the Research Foundation Flanders (FWO). Dominique Devriese and Raoul Strackx hold postdoctoral mandates from the Research Foundation Flanders (FWO). (Research Fund KU Leuven, Research Foundation Flanders (FWO))status: Publishe
Compiler-Assisted Hardening of Embedded Software Against Interrupt Latency Side-Channel Attacks
No full textsponsorship: We thank Jo Van Bulck, Raoul Strackx and Job Noorman for helpful discussions about this work. We thank Jo Van Bulck and Raoul Strackx for comments on an early draft of this paper. We thank the anonymous reviewers for helpful comments that helped improving the paper. This research is partially funded by the Research Fund KU Leuven, and by the Flemish Research Programme Cybersecurity. This work was partially supported by a gift from Intel Corporation. (Research Fund KU Leuven, Flemish Research Programme Cybersecurity, Intel Corporation)status: Publishe
Secure compilation to protected module architectures
No full textA fully abstract compiler prevents security features of the source language from being bypassed by an at- tacker operating at the target language level. Unfortunately, developing fully abstract compilers is very complex, and it is even more so when the target language is an untyped assembly language. To provide a fully abstract compiler that targets untyped assembly, it has been suggested to extend the target language with a protected module architecture — an assembly-level isolation mechanism which can be found in next- generation processors. This paper provides a fully abstract compilation scheme whose source language is an object-oriented, high-level language and whose target language is such an extended assembly language. The source language enjoys features such as dynamic memory allocation and exceptions. Secure compilation of first-order method references, cross-package inheritance and inner classes is also presented. Moreover, this paper contains the formal proof of full abstraction of the compilation scheme. Measurements of the overhead introduced by the compilation scheme indicate that it is negligible.sponsorship: This work has been supported in part by the Intel Lab’s University Research Office. This research is also partially funded by the Research Fund KU Leuven, and by the EU FP7 project NESSoS. With the financial support from the Prevention of and Fight against Crime Programme of the European Union (B-CCENTRE). Marco Patrignani and Pieter Agten hold a Ph.D. fellowship from the Research Foundation Flanders (FWO). Raoul Strackx is a Ph.D. fellow of the agency for Innovation by Science and Technology (IWT).status: Publishe
- …
