POPL 2018 (series) / PriSC 2018 (series) / Principles of Secure Compilation /
Short Talk: Secure compilation from F* to WebAssembly
Last year, we presented at this very workshop a new toolchain that compiles Low*, a low-level subset of F*, to C programs, while preserving side-channel resistance. In this brief talk, I will give an update on KreMLin, the Low*-to-C compiler, and its new WebAssembly target. In particular, I will discuss the pros and cons of using a custom compiler, and will outline future work and possible connections with the new constant-time semantics for WebAssembly, slated to be presented later that day.
| (pres.pdf) | 185KiB |
Sat 13 JanDisplayed time zone: Tijuana, Baja California change
Sat 13 Jan
Displayed time zone: Tijuana, Baja California change
11:30 - 12:00 | |||
11:30 5mTalk | Short talk: The Meaning of Memory Safety PriSC Arthur Azevedo de Amorim Carnegie Mellon University, USA, Cătălin Hriţcu Inria Paris, Benjamin C. Pierce University of Pennsylvania Pre-print File Attached | ||
11:35 5mTalk | Short talk: Dependently Typed Assembly for Secure Linking PriSC William J. Bowman Northeastern University, USA Link to publication File Attached | ||
11:40 5mTalk | Short talk: Compiler Optimizations with Retrofitting Transformations: Is there a Semantic Mismatch? PriSC Santosh Nagarakatte Rutgers University, USA Pre-print File Attached | ||
11:45 5mTalk | Short Talk: Secure compilation from F* to WebAssembly PriSC Jonathan Protzenko Microsoft Research, n.n. File Attached | ||
