Short talk: Dependently Typed Assembly for Secure Linking
Type-preserving compilation is used to statically enforce safety and security properties through type checking. The idea is to design strongly typed compiler target languages, preserve type information through the compiler, then use the types in the target language to enforce invariants when linking with untrusted code. Unfortunately, this technique is limited by the expressiveness of the target type system, and existing simple and polymorphic typed assembly languages cannot express all security invariants we wish to enforce. Dependent types could be used to express safety, security, and full functional correctness invariants. In this talk, I briefly describe work-in-progress on developing a dependently typed assembly, and how it could be used to statically enforce security guarantees when linking.
Slides for "Dependently Typed Assembly and Secure Linking" (prisc2018-dtal.pdf) | 369KiB |
William J. Bowman is a 6th Ph.D. candidate in the College of Computer and Information Science (specializing in programming languages) at Northeastern University. Broadly speaking, he is interested in making it easier for programmers to communicate their intent to machines, and preserving that intent through the stages of compilation. More specifically, his research interests include secure and verified compilation, dependently typed programming, verification, and meta-programming. His recent work examines type-preserving compilation of dependently typed programming language like Coq, a technique that can enable preserving security and correctness invariants of verified software through compilation and statically enforcing those invariants in the low-level (assembly-like) code generated by compilers.
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 |