Checkbochs: Use Hardware to Check Software

TL;DR

Checkbochs is a hardware-level machine simulator that verifies OS and application properties through plugins, uncovering new bugs in Linux distributions and educational software.

Contribution

It introduces a hardware-level simulation system with plugin-based property checks, enabling detection of security and correctness bugs not previously identified.

Findings

Discovered unknown bugs in Linux distributions

Uncovered numerous bugs in undergraduate coursework

Validated effectiveness of hardware-level checks

Abstract

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.