On Designing an ACL2-Based C Integer Type Safety Checking Tool

摘要

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.