Synthesis and Verification of CHERI Memory Managers

Jeremy Singer, University of Glasgow

How do you write a memory allocator or garbage collector for your favourite language runtime? Borrow an existing allocator library … how do you know it’s secure? Roll your own allocator … how long does that take? And can you guarantee performance and security anyway? In this lecture, we briefly review the CHERI concept of memory safety via hardware capabilities, then sketch out some techniques for automated synthesis and verification of `malloc` routines, seeking to ensure both security and performance. This will be a pragmatic talk with live follow-along coding examples.        

To benefit the most from this lecture, student will need some knowledge of C programming and remote source code editing via vim/emacs

Jeremy Singer is a Reader in Programming Language Implementation at the School of Computing Science with a particular research focus is on systems software, including virtual machines, system security and programming language runtimes. He is also a senior member of the ACM and a fellow of the BCS.