2008 Third International Conference on Availability, Reliability and Security
Type and Effect Annotations for Safe Memory Access in C
March 04-March 07
ISBN: 978-0-7695-3102-1
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.
Index Terms:
Type and Effect Analysis, Type Annotations, Memory Safety, C Programming
Citation:
Syrine Tlili, Mourad Debbabi, "Type and Effect Annotations for Safe Memory Access in C," ares, pp.302-309, 2008 Third International Conference on Availability, Reliability and Security, 2008