Static Checking Technique For Embedded Software In C Language

Embedded system is a kind of special computer system that combines the software and hardware tightly as a whole. As it is used more and more widely in some highly secure areas such as national defense, space, industrial control, the security of embedded system itself has become more important that ever. C is the most commonly used computer language in embedded software development, so the correctness checking for C program has become a key point in guarantee the security for embedded software.There are two main types in C program checking: dynamic checking and static checking. Dynamic checking, known as run-time checking, is a kind of checking that do the verification when the program is actually running. It choose proper test case, run the program against these case and monitor the running process of the program to see if there is something abnormal happened. If error happened, the monitor can trace the track of the problem to detect the bug in original code. The static checking, on the other way, does not run the program on the computer. Instead, it try to analyze the source code, simulate the run time behavior of the program in order to detect the potential bug and flaw in the source code with the help of some static check tool. Due to the special develop process of embedded software, compare to dynamic checking, static checking is simpler and ask for fewer resources. So, static checking is more suitable for embedded software development. In this thesis, we try to summarize the main security challenges for C program based on the related research works in this area and analyze the reason for these security problems. Base on all of these works, we introduce two main methods for static checking of C language. The first one is an annotation based method used to detect the memory and pointer error and the second one is a stack overflow detection method base on function calling analyzing. The second one is the main contribution of this thesis.Memory and pointer error are the most common and hardest detecting errors in C program. In this thesis, we present a static checking model using annotation in source code to solve these two problems. The model marks all of the objects in program with different annotations, by checking the consistency among states and annotations, memory and pointer errors can be detected. Because of the limited resource in embedded system, detecting for stack overflow has became an important aspect in static checking. In this thesis, we introduce the memory model and function calling process in C program. Explain the cause of stack overflow. Beyond that, we propose a static checking method for the stack overflow problem. Describe the key technologies in detail. Also, we design and implemented the whole stack overflow checker, testing its correctness and usability to prove that it's works in the real system.