Blogs >>
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Fri 4 Nov 2016 10:55 - 11:20 at Matterhorn 1 - Typing, in Practice Chair(s): Sebastian Erdweg

Existing approaches for detecting type errors in unsafe languages are limited. Static analysis methods are imprecise, and often require source-level changes, while most dynamic methods check only memory properties (bounds, liveness, etc.), owing to a lack of run-time type information. This paper describes libcrunch, a system for binary-compatible run-time type checking of unmodified unsafe code, currently focusing on C. Practical experience shows that our prototype implementation is easily applicable to many real codebases without source-level modification, correctly flags programmer errors with a very low rate of false positives, offers a very low run-time overhead, and covers classes of error caught by no previously existing tool.

I did my Bachelor’s and PhD degrees at the University of Cambridge. My initial research background was in operating systems, hypervisors and the like, with a little networking and distributed systems thrown in. Moving some way up the stack, my PhD work centred on the programmer-facing problem of building software by composition of ill-matched components, for which I developed the Cake language. From January 2011 until March 2012 I was a James Martin Fellow in the Department of Computer Science at the University of Oxford, mostly focused on program analysis and the problem of combining state-space methods (e.g. symbolic execution) with syntactic methods (e.g. type checking). From May 2012 to May 2013, I was a postdoctoral researcher at USI’s Faculty of Informatics in Lugano, Switzerland, working on programmer-facing dynamic analysis infrastructure for Java-like virtual machines. From May until October 2013 I was temporarily a Research Assistant at Oracle Labs, on the Alphabet Soup project, working on native object code and debugging support in the Truffle/SubstrateVM stack. Since 2013 I have been a Research Associate back at the University of Cambridge Computer Laboratory, working on various topics with robustness in low-level programming as a recurring theme. I have also worked (some time ago) for Opal Telecom and ARM, and (more recently) and as a consultant for Ellexus.