In this paper, we present a system called Checkbochs, a machine simulator that checks rules about its guest operating system and applications at the hardware level. The properties to be checked can be implemented as plugins' in the Checkbochs simulator. Some of the properties that were checked using Checkbochs include null-pointer checks, format-string vulnerabilities, user kernel pointer checks, and race-conditions. On implementing these checks, we were able to uncover previously-unknown bugs in widely used Linux distributions. We also tested our tools on undergraduate coursework, and found numerous bugs.
Static compile-time analysis with programmer written compiler-extensions was used to catch around 500 bugs in the linux kernel @cite_6 , @cite_3 . Using static data flow analysis and domain specific knowledge, many bugs were found in the heavily audited kernel. Ways have also been suggested to automatically detect anomalies as deviant behavior in the source code @cite_2 . Most of the bugs checked by static analysis are local to a single file, sometimes even local to a single procedure. This is due to the complexity involved in performing global compile time analysis. This limits the power of static analysis tools to surface bugs . Our approach, on the other hand, can track data flow across many different software components possibly written by different vendors and can thus target a different variety of errors. However, static analysis has the huge advantage of being able to check all possible code paths, while our execution-driven approach can only check bugs along the path of execution in the system.
@cite_3 @cite_6 @cite_2
1600965014 2066859698 2043811931
This paper shows how system-specific static analysis can find security errors that violate rules such as "integers from untrusted sources must be sanitized before use" and "do not dereference user-supplied pointers." In our approach, programmers write system-specific extensions that are linked into the compiler and check their code for errors. We demonstrate the approach's effectiveness by using it to find over 100 security errors in Linux and OpenBSD, over 50 of which have led to kernel patches. An unusual feature of our approach is the use of methods to automatically detect when we miss code actions that should be checked. Systems software such as OS kernels, embedded systems, and libraries must obey many rules for both correctness and performance. Common examples include "accesses to variable A must be guarded by lock B," "system calls must check user pointers for validity before using them," and "message handlers should free their buffers as quickly as possible to allow greater parallelism." Unfortunately, adherence to these rules is largely unchecked. This paper attacks this problem by showing how system implementors can use meta-level compilation (MC) to write simple, system-specific compiler extensions that automatically check their code for rule violations. By melding domain-specific knowledge with the automatic machinery of compilers, MC brings the benefits of language-level checking and optimizing to the higher, "meta" level of the systems implemented in these languages. This paper demonstrates the effectiveness of the MC approach by applying it to four complex, real systems: Linux, OpenBSD, the Xok exokernel, and the FLASH machine's embedded software. MC extensions found roughly 500 errors in these systems and led to numerous kernel patches. Most extensions were less than a hundred lines of code and written by implementors who had a limited understanding of the systems checked. A major obstacle to finding program errors in a real system is knowing what correctness rules the system must obey. These rules are often undocumented or specified in an ad hoc manner. This paper demonstrates techniques that automatically extract such checking information from the source code itself, rather than the programmer, thereby avoiding the need for a priori knowledge of system rules.The cornerstone of our approach is inferring programmer "beliefs" that we then cross-check for contradictions. Beliefs are facts implied by code: a dereference of a pointer, p, implies a belief that p is non-null, a call to "unlock(1)" implies that 1 was locked, etc. For beliefs we know the programmer must hold, such as the pointer dereference above, we immediately flag contradictions as errors. For beliefs that the programmer may hold, we can assume these beliefs hold and use a statistical analysis to rank the resulting errors from most to least likely. For example, a call to "spin_lock" followed once by a call to "spin_unlock" implies that the programmer may have paired these calls by coincidence. If the pairing happens 999 out of 1000 times, though, then it is probably a valid belief and the sole deviation a probable error. The key feature of this approach is that it requires no a priori knowledge of truth: if two beliefs contradict, we know that one is an error without knowing what the correct belief is.Conceptually, our checkers extract beliefs by tailoring rule "templates" to a system --- for example, finding all functions that fit the rule template "a must be paired with b." We have developed six checkers that follow this conceptual framework. They find hundreds of bugs in real systems such as Linux and OpenBSD. From our experience, they give a dramatic reduction in the manual effort needed to check a large system. Compared to our previous work [9], these template checkers find ten to one hundred times more rule instances and derive properties we found impractical to specify manually.