Type and Effect Annotations for Safe Memory Access in C

14 years 1 months ago
Type and Effect Annotations for Safe Memory Access in C
In this paper, we present a novel type and effect analysis for detecting memory errors in C source code. We extend the standard C type system with effect, region, and host annotations that hold valuable security information. We define static security checks to detect errors using the annotations. The checks are compliant with the ANSI-C standard, while adding more security restrictions to prevent runtime errors. The flow-sensitivity nature of our analysis enables us to modify type annotations at each program point and to efficiently detect temporal errors. Moreover, we endow our type system with alias information to deal with C aliasing pitfalls and to improve the precision of our analysis. We present an inference algorithm that automatically infers type annotations and applies security checks without programmer’s intervention.
Syrine Tlili, Mourad Debbabi
Added 31 May 2010
Updated 31 May 2010
Type Conference
Year 2008
Authors Syrine Tlili, Mourad Debbabi
Comments (0)