POPL 2018 (series) / PriSC 2018 (series) / Principles of Secure Compilation /
Short talk: Compiler Optimizations with Retrofitting Transformations: Is there a Semantic Mismatch?
A retrofitting transformation modifies an input program by adding instrumentation to monitor security properties at runtime. These tools often transform the input program in complex ways. Compiler optimizations can erroneously remove the instrumentation added by a retrofitting transformation in the presence of semantic mismatches between the assumptions of retrofitting transformations and compiler optimizations. This talk will highlight a strategy to ascertain that every event of interest that is checked in the retrofitted program is also checked after optimizations. Our initial experiments have identified bugs both in previously proposed retrofitting transformations and our implementations of retrofitting transformations.
Santosh-Nagarakatte-Prisc2018-talk (santosh-nagarakatte-prisc2018.pdf) | 5.15MiB |
Sat 13 Jan Times are displayed in time zone: Tijuana, Baja California change
Sat 13 Jan
Times are displayed in time zone: Tijuana, Baja California change
11:30 - 11:35 Talk | Short talk: The Meaning of Memory Safety PriSC Arthur Azevedo de AmorimCarnegie Mellon University, USA, Cătălin HriţcuInria Paris, Benjamin C. PierceUniversity of Pennsylvania Pre-print File Attached | ||
11:35 - 11:40 Talk | Short talk: Dependently Typed Assembly for Secure Linking PriSC William J. BowmanNortheastern University, USA Link to publication File Attached | ||
11:40 - 11:45 Talk | Short talk: Compiler Optimizations with Retrofitting Transformations: Is there a Semantic Mismatch? PriSC Santosh NagarakatteRutgers University, USA Pre-print File Attached | ||
11:45 - 11:50 Talk | Short Talk: Secure compilation from F* to WebAssembly PriSC Jonathan ProtzenkoMicrosoft Research, n.n. File Attached |