LIVIVO - The Search Portal for Life Sciences

zur deutschen Oberfläche wechseln
Advanced search

Search results

Result 1 - 10 of total 11

Search options

  1. Book ; Online: Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors

    Mohr, Gideon / Guarnieri, Marco / Reineke, Jan

    2024  

    Abstract: Microarchitectural attacks compromise security by exploiting software-visible artifacts of microarchitectural optimizations such as caches and speculative execution. Defending against such attacks at the software level requires an appropriate abstraction ...

    Abstract Microarchitectural attacks compromise security by exploiting software-visible artifacts of microarchitectural optimizations such as caches and speculative execution. Defending against such attacks at the software level requires an appropriate abstraction at the instruction set architecture (ISA) level that captures microarchitectural leakage. Hardware-software leakage contracts have recently been proposed as such an abstraction. In this paper, we propose a semi-automatic methodology for synthesizing hardware-software leakage contracts for open-source microarchitectures. For a given ISA, our approach relies on human experts to (a) capture the space of possible contracts in the form of contract templates and (b) devise a test-case generation strategy to explore a microarchitecture's potential leakage. For a given implementation of an ISA, these two ingredients are then used to automatically synthesize the most precise leakage contract that is satisfied by the microarchitecture. We have instantiated this methodology for the RISC-V ISA and applied it to the Ibex and CVA6 open-source processors. Our experiments demonstrate the practical applicability of the methodology and uncover subtle and unexpected leaks.
    Keywords Computer Science - Cryptography and Security
    Subject code 004
    Publishing date 2024-01-17
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  2. Book ; Online: Hide and Seek with Spectres

    Oleksenko, Oleksii / Guarnieri, Marco / Köpf, Boris / Silberstein, Mark

    Efficient discovery of speculative information leaks with random testing

    2023  

    Abstract: Attacks like Spectre abuse speculative execution, one of the key performance optimizations of modern CPUs. Recently, several testing tools have emerged to automatically detect speculative leaks in commercial (black-box) CPUs. However, the testing process ...

    Abstract Attacks like Spectre abuse speculative execution, one of the key performance optimizations of modern CPUs. Recently, several testing tools have emerged to automatically detect speculative leaks in commercial (black-box) CPUs. However, the testing process is still slow, which has hindered in-depth testing campaigns, and so far prevented the discovery of new classes of leakage. In this paper, we identify the root causes of the performance limitations in existing approaches, and propose techniques to overcome these limitations. With these techniques, we improve the testing speed over the state-of-the-art by up to two orders of magnitude. These improvements enable us to run a testing campaign of unprecedented depth on Intel and AMD CPUs. As a highlight, we discover two types of previously unknown speculative leaks (affecting string comparison and division) that have escaped previous manual and automatic analyses.

    Comment: To appear in IEEE S&P 2023
    Keywords Computer Science - Cryptography and Security
    Publishing date 2023-01-18
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  3. Thesis ; Online: Formal Foundations for Access and Inference Control in Databases

    Guarnieri, Marco

    2017  

    Keywords info:eu-repo/classification/ddc/4 ; Data processing ; computer science
    Language English
    Publisher ETH Zurich
    Publishing country ch
    Document type Thesis ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  4. Book ; Online: Contract-Aware Secure Compilation

    Guarnieri, Marco / Patrignani, Marco

    2020  

    Abstract: Microarchitectural attacks exploit the abstraction gap between the Instruction Set Architecture (ISA) and how instructions are actually executed by processors to compromise the confidentiality and integrity of a system. To secure systems against ... ...

    Abstract Microarchitectural attacks exploit the abstraction gap between the Instruction Set Architecture (ISA) and how instructions are actually executed by processors to compromise the confidentiality and integrity of a system. To secure systems against microarchitectural attacks, programmers need to reason about and program against these microarchitectural side-effects. However, we cannot -- and should not -- expect programmers to manually tailor programs for specific processors and their security guarantees. Instead, we could rely on compilers (and the secure compilation community), as they can play a prominent role in bridging this gap: compilers should target specific processors microarchitectural security guarantees and they should leverage these guarantees to produce secure code. To achieve this, we outline the idea of Contract-Aware Secure COmpilation (CASCO) where compilers are parametric with respect to a hardware/software security-contract, an abstraction capturing a processor's security guarantees. That is, compilers will automatically leverage the guarantees formalized in the contract to ensure that program-level security properties are preserved at microarchitectural level.
    Keywords Computer Science - Cryptography and Security ; Computer Science - Programming Languages
    Subject code 005
    Publishing date 2020-12-28
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  5. Book ; Online: A Turning Point for Verified Spectre Sandboxing

    Cauligi, Sunjay / Guarnieri, Marco / Moghimi, Daniel / Stefan, Deian / Vassena, Marco

    2022  

    Abstract: Spectre attacks enable an attacker to access restricted data in an application's memory. Both the academic community and industry veterans have developed several mitigations to block Spectre attacks, but to date, very few have been formally vetted; most ... ...

    Abstract Spectre attacks enable an attacker to access restricted data in an application's memory. Both the academic community and industry veterans have developed several mitigations to block Spectre attacks, but to date, very few have been formally vetted; most are "best effort" strategies. Formal guarantees are particularly crucial for protecting isolated environments like sandboxing against Spectre attacks. In such environments, a subtle flaw in the mitigation would allow untrusted code to break out of the sandbox and access trusted memory regions. In our work, we develop principled foundations to build isolated environments resistant against Spectre attacks. We propose a formal framework for reasoning about sandbox execution and Spectre attacks. We formalize properties that sound mitigation strategies must fulfill and we show how various existing mitigations satisfy (or fail to satisfy!) these properties.
    Keywords Computer Science - Cryptography and Security
    Publishing date 2022-08-02
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  6. Book ; Online: Exorcising Spectres with Secure Compilers

    Patrignani, Marco / Guarnieri, Marco

    2019  

    Abstract: Attackers can access sensitive information of programs by exploiting the side-effects of speculatively-executed instructions using Spectre attacks. To mitigate theses attacks, popular compilers deployed a wide range of countermeasures. The security of ... ...

    Abstract Attackers can access sensitive information of programs by exploiting the side-effects of speculatively-executed instructions using Spectre attacks. To mitigate theses attacks, popular compilers deployed a wide range of countermeasures. The security of these countermeasures, however, has not been ascertained: while some of them are believed to be secure, others are known to be insecure and result in vulnerable programs. To reason about the security guarantees of these compiler-inserted countermeasures, this paper presents a framework comprising several secure compilation criteria characterizing when compilers produce code resistant against Spectre attacks. With this framework, we perform a comprehensive security analysis of compiler-level countermeasures against Spectre attacks implemented in major compilers. This work provides sound foundations to formally reason about the security of compiler-level countermeasures against Spectre attacks as well as the first proofs of security and insecurity of said countermeasures.
    Keywords Computer Science - Programming Languages
    Subject code 005
    Publishing date 2019-10-18
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  7. Book ; Online: Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts

    Wang, Zilong / Mohr, Gideon / von Gleissenthall, Klaus / Reineke, Jan / Guarnieri, Marco

    2023  

    Abstract: Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Such contracts aim to faithfully capture the information processors may leak through side effects of their microarchitectural ... ...

    Abstract Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Such contracts aim to faithfully capture the information processors may leak through side effects of their microarchitectural implementations. However, so far, we lack a verification methodology to check that a processor actually satisfies a given leakage contract. In this paper, we address this problem by developing LeaVe, the first tool for verifying register-transfer-level (RTL) processor designs against ISA-level leakage contracts. To this end, we introduce a decoupling theorem that separates security and functional correctness concerns when verifying contract satisfaction. LeaVe leverages this decoupling to make verification of contract satisfaction practical. To scale to realistic processor designs LeaVe further employs inductive reasoning on relational abstractions. Using LeaVe, we precisely characterize the side-channel security guarantees provided by three open-source RISC-V processors, thereby obtaining the first contract satisfaction proofs for RTL processor designs.

    Comment: Technical report containing full formalization and proofs of all results. A short version of this report (with the same title) appears in the proceedings of the 30th ACM SIGSAC Conference on Computer and Communication Security (CCS 2023)
    Keywords Computer Science - Cryptography and Security
    Subject code 005
    Publishing date 2023-05-11
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  8. Book ; Online: Hardware-Software Contracts for Secure Speculation

    Guarnieri, Marco / Köpf, Boris / Reineke, Jan / Vila, Pepe

    2020  

    Abstract: 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 ... ...

    Abstract 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.

    Comment: Camera ready version that will appear in the proceedings of the 42nd IEEE Symposium on Security and Privacy (IEEE S&P 2021). A technical report containing a full formalization and proofs of all results is available at arXiv:2006.03841v2
    Keywords Computer Science - Cryptography and Security
    Subject code 005
    Publishing date 2020-06-06
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  9. Book ; Online: Testing side-channel security of cryptographic implementations against future microarchitectures

    Barthe, Gilles / Böhme, Marcel / Cauligi, Sunjay / Chuengsatiansup, Chitchanok / Genkin, Daniel / Guarnieri, Marco / Romero, David Mateos / Schwabe, Peter / Wu, David / Yarom, Yuval

    2024  

    Abstract: How will future microarchitectures impact the security of existing cryptographic implementations? As we cannot keep reducing the size of transistors, chip vendors have started developing new microarchitectural optimizations to speed up computation. A ... ...

    Abstract How will future microarchitectures impact the security of existing cryptographic implementations? As we cannot keep reducing the size of transistors, chip vendors have started developing new microarchitectural optimizations to speed up computation. A recent study (Sanchez Vicarte et al., ISCA 2021) suggests that these optimizations might open the Pandora's box of microarchitectural attacks. However, there is little guidance on how to evaluate the security impact of future optimization proposals. To help chip vendors explore the impact of microarchitectural optimizations on cryptographic implementations, we develop (i) an expressive domain-specific language, called LmSpec, that allows them to specify the leakage model for the given optimization and (ii) a testing framework, called LmTest, to automatically detect leaks under the specified leakage model within the given implementation. Using this framework, we conduct an empirical study of 18 proposed microarchitectural optimizations on 25 implementations of eight cryptographic primitives in five popular libraries. We find that every implementation would contain secret-dependent leaks, sometimes sufficient to recover a victim's secret key, if these optimizations were realized. Ironically, some leaks are possible only because of coding idioms used to prevent leaks under the standard constant-time model.
    Keywords Computer Science - Cryptography and Security
    Subject code 005
    Publishing date 2024-02-01
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  10. Book ; Online: Flushgeist

    Vila, Pepe / Abel, Andreas / Guarnieri, Marco / Köpf, Boris / Reineke, Jan

    Cache Leaks from Beyond the Flush

    2020  

    Abstract: Flushing the cache, using instructions like clflush and wbinvd, is commonly proposed as a countermeasure against access-based cache attacks. In this report, we show that several Intel caches, specifically the L1 caches in some pre-Skylake processors and ... ...

    Abstract Flushing the cache, using instructions like clflush and wbinvd, is commonly proposed as a countermeasure against access-based cache attacks. In this report, we show that several Intel caches, specifically the L1 caches in some pre-Skylake processors and the L2 caches in some post-Broadwell processors, leak information even after being flushed through clflush and wbinvd instructions. That is, security-critical assumptions about the behavior of clflush and wbinvd instructions are incorrect, and countermeasures that rely on them should be revised.

    Comment: 6 pages, 4 figures
    Keywords Computer Science - Cryptography and Security
    Publishing date 2020-05-28
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

To top