Compiling C programs into a strongly typed assembly language

Abstract

C is one of the most popular languages in system programming, though its unsafe nature often causes security vulnerabilities. In the face of this situation, many tools are developed to ensure safety properties of C programs. However, most of them work at the source code level, and conventional compilers lose safety guarantee as they translate source code into assembly code. In this paper, we present CTAL0, a strongly typed assembly language that is aimed at certifying the memory safety of assembly code compiled from C programs. CTAL0 is expressive enough to implement potentially unsafe ANSI C features including pointer arithmetics and casts. We have also implemented a type-checker and an experimental C compiler that produces safe CTAL0 assembly code by performing several transformations on given programs to avoid dangerous operations. © Springer-Verlag Berlin Heidelberg 2007.