156 citations · 297 across the 16 of their papers we have counts for
17 papers
Libra: Architectural Support For Principled, Secure And Efficient Balanced Execution On High-End Processors (Extended Version)
Hans Winderix, Marton Bognar, Lesly-Ann Daniel +1
Control-flow leakage (CFL) attacks enable an attacker to expose control-flow decisions of a victim program via side-channel observations. Linearization (i.e., elimination) of secre…
ProSpeCT: Provably Secure Speculation for the Constant-Time Policy (Extended version)
Lesly-Ann Daniel, Marton Bognar, Job Noorman +3
We propose ProSpeCT, a generic formal processor model providing provably secure speculation for the constant-time policy. For constant-time programs under a non-speculative semanti…
End-to-End Security for Distributed Event-Driven Enclave Applications on Heterogeneous TEEs
Gianluca Scopelliti, Sepideh Pouyanrad, Job Noorman +4
This paper presents an approach to provide strong assurance of the secure execution of distributed event-driven applications on shared infrastructures, while relying on a small Tru…
Automated Fuzzing of Automotive Control Units
Timothy Werquin, Roos Hubrechtsen, Ashok Thangarajan +2
Modern vehicles are governed by a network of Electronic Control Units (ECUs), which are programmed to sense inputs from the driver and the environment, to process these inputs, and…
Abstract Congruence Criteria for Weak Bisimilarity
Stelios Tsampas, Christian Williams, Andreas Nuyts +2
We introduce three general compositionality criteria over operational semantics and prove that, when all three are satisfied together, they guarantee weak bisimulation being a cong…
CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle
Akram El-Korashy, Stelios Tsampas, Marco Patrignani +3
Capability machines such as CHERI provide memory capabilities that can be used by compilers to provide security benefits for compiled code (e.g., memory safety). The existing C to…
A categorical approach to secure compilation
Stelios Tsampas, Andreas Nuyts, Dominique Devriese +1
We introduce a novel approach to secure compilation based on maps of distributive laws. We demonstrate through four examples that the coherence criterion for maps of distributive l…
Gavial: Programming the web with multi-tier FRP
Bob Reynders, Frank Piessens, Dominique Devriese
Developing web applications requires dealing with their distributed nature and the natural asynchronicity of user input and network communication. For facilitating this, different…
CopyCat: Controlled Instruction-Level Attacks on Enclaves
Daniel Moghimi, Jo Van Bulck, Nadia Heninger +2
The adversarial model presented by trusted execution environments (TEEs) has prompted researchers to investigate unusual attack vectors. One particularly powerful class of controll…
Provably Secure Isolation for Interruptible Enclaved Execution on Small Microprocessors: Extended Version
Matteo Busi, Job Noorman, Jo Van Bulck +4
Computer systems often provide hardware support for isolation mechanisms like privilege levels, virtual memory, or enclaved execution. Over the past years, several successful softw…
Fallout: Reading Kernel Writes From User Space
Marina Minkin, Daniel Moghimi, Moritz Lipp +7
Recently, out-of-order execution, an important performance optimization in modern high-end processors, has been revealed to pose a significant security threat, allowing information…
A Systematic Evaluation of Transient Execution Attacks and Defenses
Claudio Canella, Jo Van Bulck, Michael Schwarz +6
Research on transient execution attacks including Spectre and Meltdown showed that exception or branch misprediction events might leave secret-dependent traces in the CPU's microar…
The Heisenberg Defense: Proactively Defending SGX Enclaves against Page-Table-Based Side-Channel Attacks
Raoul Strackx, Frank Piessens
Protected-module architectures (PMAs) have been proposed to provide strong isolation guarantees, even on top of a compromised system. Unfortunately, Intel SGX -- the only publicly…
Modular, Fully-abstract Compilation by Approximate Back-translation
Dominique Devriese, Marco Patrignani, Frank Piessens +1
A compiler is fully-abstract if the compilation from source language programs to target language programs reflects and preserves behavioural equivalence. Such compilers have import…
On Modular and Fully-Abstract Compilation -- Technical Appendix
Marco Patrignani, Dominique Devriese, Frank Piessens
Secure compilation studies compilers that generate target-level components that are as secure as their source-level counterparts. Full abstraction is the most widely-proven propert…
Featherweight VeriFast
Bart Jacobs, Frédéric Vogels, Frank Piessens
VeriFast is a leading research prototype tool for the sound modular verification of safety and correctness properties of single-threaded and multithreaded C and Java programs. It h…
On the effectiveness of virtualization-based security
Francesco Gadaleta, Raoul Strackx, Nick Nikiforakis +2
Protecting commodity operating systems and applications against malware and targeted attacks has proven to be difficult. In recent years, virtualization has received attention from…