The C integer types are prone to errors due to unchecked casting that can leave programs vulnerable to a host of security exploits. These errors manifest themselves when there is a semantic disconnect between the programmer's view of the language and the actual implementation of the programming language. To help detect these errors, we are developing a C integer type safety checking tool written in ACL2. This paper presents the justification and fundamental logic behind the tool, the basic operations of the tool, and discussion of future plans.
展开▼
