David Tarditi
Talk: An Overview of the Checked C Project
- Date and Time
- October 26, 2016 at 3:30pm
- Location
Abstract
C is widely used for system programming. It is prone to low-level programming errors that can lead to security and reliability issues. The Checked C project is a new research effort that is extending C with checking to detect or prevent low-level programming errors. The project has focused initially on designing and implementing a backwards-compatible extension to C that adds bounds checking. This talk will cover the motivation for Checked C, give an overview of the language extension design, discuss work implementing the extension in the clang compiler front-end, and discuss next steps.
The language extension puts bounds checking under the control of the programmer, in line with the design of C. It adds new pointer and array types that have bounds checking. It also adds simple pointer types that only point to data and that do not allow pointer arithmetic. Memory accesses through simple pointers types do not need bounds checking. Programmers describe how bounds information is represented at runtime by adding bounds declarations to variables and data structure members. Static checking ensures that the bounds declarations are consistent. The validity of bounds declarations must follow from calls to memory allocators, declarations of variables, existing bounds declarations, and other program facts. Bounds are checked at runtime at memory accesses using bounds information, unless it can be proved at compile time that the checks are unnecessary. Programmers describe the behavior and expectations of existing code with respect to bounds by extending existing declarations with bounds declarations, creating bounds-safe interfaces to unchecked code. This allows existing code to be converted to checked code in a modular fashion.
We are validating and refining the language design by implementing it in the clang compiler front-end. Some aspects of the language design, such as incorporating static checking of bounds declarations into a compiler, are novel and experimental. We plan to evaluate the design and implementation of those aspects by modifying real-word C code to use the Checked C extension.
Checked C is an open-source research project. The language design is available at https://github.com/Microsoft/checkedc/releases. The clang implementation is on Github as well at http://github.com/Microsoft/checkedc-clang.
Bio
I am a Principal Researcher at Microsoft Research, where I am a member of the Operating System Technologies group. My research interests span compilers, programming languages, operating systems, and performance. My current focus is on better programming languages and tools for systems programming. I lead the Checked C project.
Checked C is investigating extending C with static and dynamic checking to detect or prevent common programming errors in C such as buffer overruns, out-of-bounds memory accesses, and incorrect pointer casts. This will improve system reliability, security, and programmer productivity for widely-used C and C++ code bases.
I rejoined Microsoft Research in 2015. From 2014 to 2015, I led the System C# project, an effort to create a version of C# and an implementation suitable for systems programming on Windows. The effort was shelved largely because of incompatibilities between the programming models of C#, C++ and C. The differences were too large to overcome to make this practical at this time. C# is type-safe and uses automatic memory management, while C++ and C do not enforce strong type-safety and use explicit memory management. C++ or C code could corrupt the memory used by C# code, leading to hard-to-debug crashes in the garbage collector or C# code.
From 2007 to 2014, I led the tools team for the Midori project. I was the development lead and then the development manager for the tools team. The team built the technology that enabled the Midori OS to be written almost entirely in C#, including an ahead-of-time compiler, a lightweight runtime system, and the implementation of core OS features such as shared libraries for C#. We built on the work that we did for Singularity. The shared libraries included support for sharing generic code across libraries, something not provided by typical C++ template implementations. This reduced code size for Midori by over 35%. We also focused on reducing code size, improving optimizations for managed code, and reducing costs of managed code such as bounds checking, and ode.
Our work on highly-optimizing ahead-of-time compilation for C# directly inspired the .Net Native product, which shipped in 2014.
From 2001 to 2007, I led the Advanced Compiler Technology group at Microsoft Research. The group was one of the research groups that worked on the Singularity Project. We designed and built the Bartok compiler and lightweight runtime system used in Singularity.