An Overview of an ACL2 Prototype C Integer Type Safety Verification Tool

Abstract

The preeminent status that the C programming language continues to enjoy comes at the cost of a lack of memory bounds checking. For example, it is widely known that C is not type safe because its integer types are highly susceptible to entering an error condition. A single integer error might cause a system to exhibit unexpected behaviors. Moreover, the error can leave an entire system vulnerable to failure or even to a hostile takeover. If such an error manifests in a critical system, the consequences could be devastating. Such errors occur both in mobile systems as well as control systems. Analysis of the code in these systems is an essential building block for ensuring the correctness of security solutions.

Several solutions, such as safe coding guidelines, libraries of safe integer operations, and type safe subsets of C, have been proposed to ameliorate the likelihood integer errors. Except for the better coding practices, the solutions may not be practical for every situation. Libraries of safe opera- tions require added operational overhead that could exceed the limits low powered or other real time systems; and are therefore ignored in control system and mobile systems. Likewise, type safe subsets ties the hands of programmers by forcing them to use cumbersome procedures when the use of mixed data types are required.

Because the onus of writing type safe C programs remains squarely with the programmers, their code should be rigorously tested throughout the development process. Several tests have been devel- oped to achieve this end. Some are designed to verify type safety. However, no two of these test are the same in their methods, logic, and reporting. As a result, wide gaps in both accuracy and coverage remain in the realm of type safety verification. We are developing a prototype C integer type safety verification tool with a goal of closing that gap.

This poster presents an overview of the steps we took to develop our tool. That includes the identification of the problem space and a formalization of the static typing semantics of C expressions and statements based on the typing constraints on each program construct. From those two steps, the operational semantics of our tool were developed. The algorithms are supported by annotated lookup tables that gives our ability to track state wise changes. For example, entities in the data object table contain unique identification, typing, value, and/or any error-warning message information. Finally, there is the customizable output of our tool that can be proven to be correct.

Speaker Bio