EDBT 2026 Demo / reviewers in the wild / expert
Michael LeMay
dblp:81/178
· DBLP profile ↗
14ranked-venue papers
4as first author
6since 2021 · last 2025
0000-0001-6206-9642ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Security and privacy · 5 · 2 first-author · 2 since 2021Computer networks · 4 · 1 first-authorSystems, architecture and hardware · 3 · 1 first-author · 3 since 2021Software engineering, systems software and programming languages · 3 · 3 since 2021Human-computer interaction and ubiquitous computing · 1Applied, interdisciplinary, general and emerging computing · 1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | Segue & ColorGuard: Optimizing SFI Performance and Scalability on Modern ArchitecturesabstractSoftware-based fault isolation (SFI) enables in-process isolation through compiler instrumentation of memory accesses, and is a critical part of WebAssembly (Wasm). We present two optimizations that improve SFI performance and scalability: Segue uses x86-64 segmentation to reduce the cost of instrumentation on memory accesses, e.g., it eliminates 44.7% of Wasm's overhead on a Wasm-compatible subset of SPEC CPU 2006, and reduces overhead of Wasm-sandboxed font rendering in Firefox by 75%; ColorGuard leverages memory tagging (e.g., MPK), to enable up to a 15× increase in the number of Wasm instances that can run concurrently in a single address space, improving efficiency for high scale server-side workloads. We also explore the challenges of deploying these optimizations in three production toolchains: Wasm2c, WAMR and Wasmtime. Shravan Narayan, Tal Garfinkel, Evan Johnson 0001, Zachary Yedidia, Yingchen Wang, Anjo Vahldiek-Oberwagner, Michael LeMay, Wenyong Huang, Xin Wang 0240, Mingqiu Sun, Dean M. Tullsen, Deian Stefan |
ASPLOS (1) | 8 |
| 2024 | Memory Tagging using Cryptographic Integrity on Commodity x86 CPUsabstractMemory tagging allows to establish memory safety for software developed in unsafe languages like C/C++. Since it is an effective mechanism with low architectural complexity, ISA extensions, like ARM MTE or SPARC ADI, already integrate memory tagging on the architectural level for commodity computer systems. However, despite being in high demand, memory tagging features are currently absent in modern x86 processors. This work presents IntegriTag, a hardware-enforced memory tagging solution for existing commodity x86 CPUs. We leverage the Intel® Total Memory Encryption-Multi-Key (Intel® TME-MK) hardware feature that was initially envisioned for virtual machine isolation to instead provide memory tagging capabilities on off-the-shelf x86 processors. Unlike ARM MTE and SPARC ADI, this does not require the integration of a separate tagged memory architecture, which would increase the overall system complexity. Instead, our solution allows us to implicitly enforce the desired security policies by incorporating them into the existing memory encryption integrity checks. In addition, our design addresses security issues that affect tagged memory architectures with small tag spaces. Intel® TME-MK allows for a greater number of key identifier bits, thus offering significantly stronger security compared to the 4-bit tags of ARM MTE and SPARC ADI. We implement a holistic open-source software framework based on Intel® TME-MK, supporting several software-controlled and hardware-enforced memory safety policies. Moreover, we evaluate our design's performance overhead and security properties, underlining the practicability and efficacy of our approach. Our design is binary-compatible with existing software and provides both temporal and spatial memory safety while imposing an overhead of 32–41%, which is significantly lower than the overheads of memory safety schemes in software on commodity hardware that provide comparable security properties. David Schrammel, Martin Unterguggenberger, Lukas Lamster, Salmin Sultana, Karanvir Grewal, Michael LeMay, David Durham, Stefan Mangard |
EuroS&P | 6 |
| 2023 | Going beyond the Limits of SFI: Flexible and Secure Hardware-Assisted In-Process Isolation with HFIabstractWe introduce Hardware-assisted Fault Isolation (HFI), a simple extension to existing processors to support secure, flexible, and efficient in-process isolation. HFI addresses the limitations of existing software-based isolation (SFI) systems including: runtime overheads, limited scalability, vulnerability to Spectre attacks, and limited compatibility with existing code. HFI can seamlessly integrate with current SFI systems (e.g., WebAssembly), or directly sandbox unmodified native binaries. To ease adoption, HFI relies only on incremental changes to the data and control path of existing high-performance processors. We evaluate HFI for x86-64 using the gem5 simulator and compiler-based emulation on a mix of real and synthetic workloads. Shravan Narayan, Tal Garfinkel, Mohammadkazem Taram, Joey Rudek, Daniel Moghimi, Evan Johnson 0001, Chris Fallin, Anjo Vahldiek-Oberwagner, Michael LeMay, Ravi Sahita, Dean M. Tullsen, Deian Stefan |
ASPLOS (3) | 9 |
| 2023 | MEMES: Memory Encryption-Based Memory Safety on Commodity Hardware
David Schrammel, Salmin Sultana, Karanvir Grewal, Michael LeMay, David Durham, Martin Unterguggenberger, Pascal Nasahl, Stefan Mangard |
SECRYPT | 4 |
| 2022 | Isolation without taxation: near-zero-cost transitions for WebAssembly and SFIabstractSoftware 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. Matthew Kolosick, Shravan Narayan, Evan Johnson 0001, Conrad Watt, Michael LeMay, Deepak Garg 0001, Ranjit Jhala, Deian Stefan |
Proc. ACM Program. Lang. | 5 |
| 2021 | Cryptographic Capability ComputingabstractCapability architectures for memory safety have traditionally required expanding pointers and radically changing microarchitectural structures throughout processors, while only providing superficial hardening. We hence propose Cryptographic Capability Computing (C3) - the first memory safety mechanism that is stateless to avoid requiring extra metadata storage. C3 retains 64-bit pointer sizes providing legacy binary compatibility while imposing minimal touchpoints. Pointers are encrypted to unforgeably (within cryptographic bounds) reference each object. Data is encrypted even in caches and entangled with pointers for both spatial and temporal object-granular protection. Pointers become like unique keys for each allocation. C3 deploys a novel form of prediction for address translation that mitigates performance overheads even when addresses are partially encrypted. Use of a low-latency, low-area cipher from the NIST Lightweight Cryptography project avoids delaying loads by readying a data keystream by the time data is returned from the L1 cache. C3 is compatible with legacy binaries. Simulated performance overhead on SPEC CPU2006 is negligible with no memory overhead, which is a big leap forward compared to the overheads imposed by past memory safety approaches. C3 effectively replaces inefficient metadata with efficient cryptography. Michael LeMay, Joydeep Rakshit, Sergej Deutsch, David Durham, Santosh Ghosh, Anant Nori, Jayesh Gaur, Andrew Weiler, Salmin Sultana, Karanvir Grewal, Sreenivas Subramoney |
MICRO | 1 |
| 2015 | Power-Based Diagnosis of Node Silence in Remote High-End Sensing SystemsabstractTroubleshooting unresponsive sensor nodes is a significant challenge in remote sensor network deployments. While prior work often targets low-end sensor networks, this article introduces a novel diagnostic tool, called the telediagnostic powertracer, geared for remote high-end sensing systems. Leveraging special properties of high-end systems, this in situ troubleshooting tool uses external power measurements to determine the internal health condition of an unresponsive node and the most likely cause of its failure. We develop our own low-cost power meter with low-bandwidth radio, propose both passive and active sampling schemes to measure the power consumption of the host node, and then report the measurements to a base station, hence allowing remote (i.e., tele-) diagnosis. The tool was deployed and tested in a remote solar-powered sensing system for acoustic and visual environmental monitoring. It was shown to successfully distinguish between several categories of failures that cause unresponsive behavior including energy depletion, antenna damage, radio disconnection, system crashes, and anomalous reboots. It was also able to determine the internal health conditions of an unresponsive node, such as the presence or absence of sensing and data storage activities (for each of multiple applications). The article explores the feasibility of building such a remote diagnostic tool from the standpoint of economy, scale, and diagnostic accuracy. The main novelty lies in its use of power consumption as a side channel, which has more availability than other I/O ports, to diagnose sensing system failures. Yong Yang 0009, Lu Su 0001, Mohammad Maifi Hasan Khan, Michael LeMay, Tarek F. Abdelzaher, Jiawei Han 0001 |
ACM Trans. Sens. Networks | 4 |
| 2011 | Reliable telemetry in white spaces using remote attestationabstractWe consider reliable telemetry in white spaces in the form of protecting the integrity of distributed spectrum measurements against coordinated misreporting attacks. Our focus is on the case where a subset of the sensors can be remotely attested. We propose a practical framework for using statistical sequential estimation coupled with machine learning classifiers to deter attacks and achieve quantifiably precise outcome. We provide an application-oriented case study in the context of spectrum measurements in the white spaces. The study includes a cost analysis for remote attestation, as well as an evaluation using real transmitter and terrain data from the FCC and NASA for Southwest Pennsylvania. The results show that with as low as 15% penetration of attestation-capable nodes, more than 94% of the attempts from omniscient attackers can be thwarted. Omid Fatemieh, Michael LeMay, Carl A. Gunter |
ACSAC | 2 |
| 2011 | Power watermarking: Facilitating power-based diagnosis of node silence in remote high-end sensing systems
Yong Yang 0009, Lu Su 0001, Mohammad Maifi Hasan Khan, Michael LeMay, Tarek F. Abdelzaher, Jiawei Han 0001 |
IPSN | 4 |
| 2010 | Diagnostic powertracing for sensor node failure analysisabstractTroubleshooting unresponsive sensor nodes is a significant challenge in remote sensor network deployments. This paper introduces the tele-diagnostic powertracer, an in-situ troubleshooting tool that uses external power measurements to determine the internal health condition of an unresponsive host and the most likely cause of its failure. We developed our own low-cost power meter with low-bandwidth radio to report power measurements and findings, hence allowing remote (i.e., tele-) diagnosis. The tool was deployed and tested in a remote solar-powered sensing network for acoustic and visual environmental monitoring. It was shown to successfully distinguish between several categories of failures that cause unresponsive behavior including energy depletion, antenna damage, radio disconnection, system crashes, and anomalous reboots. It was also able to determine the internal health conditions of an unresponsive node, such as the presence or absence of sensing and data storage activities (for each of multiple sensors). The paper explores the feasibility of building such a remote diagnostic tool from the standpoint of economy, scale and diagnostic accuracy. To the authors' knowledge, this is the first paper that presents a remote diagnostic tool that uses power measurements to diagnose sensor system failures. Mohammad Maifi Hasan Khan, Hieu Khac Le, Michael LeMay, Paria Moinzadeh, Lili Wang 0006, Yong Yang 0009, Dong Kun Noh, Tarek F. Abdelzaher, Carl A. Gunter, Jiawei Han 0001, Xin Jin 0001 |
IPSN | 3 |
| 2009 | Cumulative Attestation Kernels for Embedded Systems
Michael LeMay, Carl A. Gunter |
ESORICS | 1 |
| 2009 | Sh@re: Negotiated Audit in Social NetworksabstractWith the growth in the popularity of social networking sites like Facebook and MySpace, there is an increasing concern about privacy of content posted by users. Many users enter personal details about themselves but have poor understanding of theats such as identity theft and stalking. There is a need to educate and assist users in understanding how their personal data is exposed to other users. In this paper, we introduce the concept of negotiated audit which gives users of social networks valuable feedback about how their data is being used. Our design has three levels of auditing for both sharing and browsing data: no audit, complete audit and anonymous audit. Users can classify their data as requiring some level of auditing and can also set their browsing preference to one of the auditing levels. Users can only see some data if their browsing preference is compatible with the data's audit level thus giving rise to negotiation of how much users are willing to reveal about their activities and how much data they will be able to access. We provide a mathematical model and describe a simple social networking prototype called Sh@re that implements negotiated audit. Alejandro Gutierrez, Apeksha Godiyal, Matt Stockton, Michael LeMay, Carl A. Gunter, Roy H. Campbell |
SMC | 4 |
| 2007 | Supporting Emergency-Response by Retasking Network Infrastructures
Michael LeMay, Carl A. Gunter |
HotNets | 1 |
| 2007 | PolicyMorph: interactive policy transformations for a logical attribute-based access control frameworkabstractConstraint systems provide techniques for automatically analyzing the conformance of low-level access control policies to high-level business rules formalized as logical constraints. However, there are likely to be priorities for solutions that are not easy to encode formally, so administrator input is often important. This paper introduces PolicyMorph, a constraint system that supports interactive development and maintenance of access control policies that respect both formalized and un-formalized business rules and priorities. We provide a mathematical description of the system and an architecture for implementing it. We constructed a prototype that is validated using a case study in which constraints are imposed on a building automation system that controls door locks. PolicyMorph advances the state-of-the-art in constraint systems by suggesting predictable policy model modifications that will resolve specific constraint violations and then allowing policy administrators to select the appropriate modifications using knowledge that is not formally encoded in the constraint system. Michael LeMay, Omid Fatemieh, Carl A. Gunter |
SACMAT | 1 |