Publications

  • Cage: Hardware-Accelerated Safe WebAssembly. CGO'25.
    Martin Fink, Dimitrios Stavrakakis, Dennis Sprokholt, Soham Chakraborty, Jan-Erik Ekberg, Pramod Bhatotia.
    [Paper] [DOI] [Artifact] [Presentation]

    Details & Source Code
    • DOI: 10.1145/3696443.3708920
    • GitHub
    Citation
    @inproceedings{Fink2025Cage,
  author = {Fink, Martin and Stavrakakis, Dimitrios and Sprokholt, Dennis and Chakraborty, Soham and Ekberg, Jan-Erik and Bhatotia, Pramod},
  title = {Cage: Hardware-Accelerated Safe WebAssembly},
  year = {2025},
  isbn = {9798400712753},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3696443.3708920},
  doi = {10.1145/3696443.3708920},
  abstract = {WebAssembly (WASM) is an immensely versatile and increasingly popular compilation target. It executes applications written in several languages (e.g., C/C++) with near-native performance in various domains (e.g., mobile, edge, cloud). Despite WASM's sandboxing feature, which isolates applications from other instances and the host platform, WASM does not inherently provide any memory safety guarantees for applications written in low-level, unsafe languages.
  To this end, we propose Cage, a hardware-accelerated toolchain for WASM that supports unmodified applications compiled to WASM and utilizes diverse Arm hardware features aiming to enrich the memory safety properties of WASM. Precisely, Cage leverages Arm's Memory Tagging Extension (MTE) to (i) provide spatial and temporal memory safety for heap and stack allocations and (ii) improve the performance of WASM's sandboxing mechanism. Cage further employs Arm's Pointer Authentication (PAC) to prevent leaked pointers from being reused by other WASM instances, thus enhancing WASM's security properties.
  We implement our system based on 64-bit WASM. We provide a WASM compiler and runtime with support for Arm's MTE and PAC. On top of that, Cage's LLVM-based compiler toolchain transforms unmodified applications to provide spatial and temporal memory safety for stack and heap allocations and prevent function pointer reuse. Our evaluation on real hardware shows that Cage incurs minimal runtime (<5.8\%) and memory (<3.7\%) overheads and can improve the performance of WASM's sandboxing mechanism, achieving a speedup of over 5.1\%, while offering efficient memory safety guarantees.},
  booktitle = {Proceedings of the 23rd ACM/IEEE International Symposium on Code Generation and Optimization},
  pages = {538--552},
  numpages = {15},
  keywords = {Memory Safety, WebAssembly},
  location = {Las Vegas, NV, USA},
  series = {CGO '25}
}

  • Lasagne: a static binary translator for weak memory model architectures. PLDI'22.
    Rodrigo C. O. Rocha, Dennis Sprokholt, Martin Fink, Redha Gouicem, Tom Spink, Soham Chakraborty, Pramod Bhatotia
    [Paper] [DOI] [Artifact]

    Details & Source Code
    • DOI: 10.1145/3519939.3523719
    • Source code was merged into Microsoft’s static binary translator mctoll.
    Citation
    @inproceedings{Rocha2022Lasagne,
  author = {Rocha, Rodrigo C. O. and Sprokholt, Dennis and Fink, Martin and Gouicem, Redha and Spink, Tom and Chakraborty, Soham and Bhatotia, Pramod},
  title = {Lasagne: a static binary translator for weak memory model architectures},
  year = {2022},
  isbn = {9781450392655},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3519939.3523719},
  doi = {10.1145/3519939.3523719},
  abstract = {The emergence of new architectures create a recurring challenge to ensure that existing programs still work on them. Manually porting legacy code is often impractical. Static binary translation (SBT) is a process where a program’s binary is automatically translated from one architecture to another, while preserving their original semantics. However, these SBT tools have limited support to various advanced architectural features. Importantly, they are currently unable to translate concurrent binaries. The main challenge arises from the mismatches of the memory consistency model specified by the different architectures, especially when porting existing binaries to a weak memory model architecture. In this paper, we propose Lasagne, an end-to-end static binary translator with precise translation rules between x86 and Arm concurrency semantics. First, we propose a concurrency model for Lasagne’s intermediate representation (IR) and formally proved mappings between the IR and the two architectures. The memory ordering is preserved by introducing fences in the translated code. Finally, we propose optimizations focused on raising the level of abstraction of memory address calculations and reducing the number of fences. Our evaluation shows that Lasagne reduces the number of fences by up to about 65\%, with an average reduction of 45.5\%, significantly reducing their runtime overhead.},
  booktitle = {Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
  pages = {888--902},
  numpages = {15},
  keywords = {Memory Model, Compiler, Binary Translation},
  location = {San Diego, CA, USA},
  series = {PLDI 2022}
}

Theses