2009-12-29

translating to safe c

11.9: proj.adda/translating to safe c:

. found in log/2006.9.11:
CIL (C to C translator) http://manju.cs.berkeley.edu/cil/
--. that link is dead,
but there is an active derivative:
CCured 1.3.5 (based on CIL 1.3.5) (2007)

CCured is a source-to-source translator for C.
It analyzes the C program to determine the
smallest number of run-time checks
that must be inserted in the program
to prevent all memory safety violations.
The resulting program is memory safe,
meaning that it will stop rather than
overrun a buffer or scribble over memory that it shouldn't touch.
Many programs can be made memory-safe this way
while losing only 10...60% run-time performance
Using CCured we have found bugs that Purify misses
with an order of magnitude smaller run-time cost.
. source is at:

. a tool to ensure both temporal and spatial memory safety in C programs
through a source-to-source transformation.
. implemented in Objective Caml and uses CIL(the dead link again)
as the front end to manipulate C constructs.
. for more details of the transformation
see our ACM SIGSOFT FSE 2004 paper:
"An efficient and backwards-compatible transformation
to ensure memory safety of C programs" (pdf)

. an optimizing C-to-C compiler,
it implements the extended pointer and array access semantics needed for
efficient, reliable and immediate detection of
memory access errors in unbridled C codes.

Fail-Safe ANSI-C Compiler: An Approach to
Making C Programs Secure Progress Report (pdf)
ISBN 978-3-540-00708-1
. many approaches to safe implementations of the C language
- such as Safe C and CCured --
have been proposed and implemented. To our knowledge, however,
none of them support all the features of the ANSI C standard
and prevent all unsafe operations.
(By unsafe operations, we mean any operation that leads to
undefined behavior,
such as array boundary overrun
and dereference of a pointer in a wrong type.)
This paper describes a memory-safe implementation of the full ANSI C language.
Our implementation detects and disallows
all unsafe operations,
yet conforming to the full ANSI C standard
(including casts and unions)
and even supporting many dirty tricks
common in programs beyond ANSI C.
This is achieved using sophisticated representations
of pointers (and integers)
that contain dynamic type and size information.
We also devise several techniques
-- both compile-time and run-time --
to reduce the overhead of runtime checks.