Writing device drivers is notoriously hard, and driver bugs are a major cause of system failures and vulnerabilities. The problem is particularly acute in bus-based protocols like I2C, where driver correctness is only half the story: correct functioning of the complete subsystem depends on all components on the bus interoperating correctly. Unfortunately, developers cannot control all aspects of a platform, and must interact with existing devices (peripherals and/or hardware bus controllers) which may misbehave. Failures in a protocol like I2C, often used in critical low-level system management, can result in permanent damage to the hardware, whether a server or a satellite.

We developed a set of tools designed to provide rapid feedback to students as they learn to write programs in assembly language (LC-3, a RISC-like educational instruction set architecture). At the heart of the system is an extended version of KLEE, KLC3, that enables us to both identify issues and perform equivalence checking between student code and a gold (correct) version of each assignment. Feedback begins when students edit their code using a VSCode extension that leverages static analysis to perform a variety of correctness and style checks, encouraging students to improve their code quality. Each time a student commits code to their Git repository, our system triggers. Using KLC3 (KLEE), the student code is executed along with the gold version, and issues and behavioral differences are delivered back to the student through their Git repository as a human-readable report, test cases, and scripts. A queueing system allows students to monitor progress, but responses are generally available within minutes. We also extended the LC-3 simulation tools to support reverse debugging, making the process of finding complex bugs much more tractable for students, and used Emscripten to develop a browser-based interface for use in testing and debugging. Finally, our system maintains an individual regression test suite for each student and requires a submission to pass all previous tests before re-evaluation in KLC3, thus avoiding encouraging programming-by-guesswork. We deployed the system to provide feedback for the assembly programming assignments in a class of over 100 students in Fall 2020. Students wrote a median of around 700 lines of assembly for these assignments, making heavy use of our tools to understand and eliminate their bugs. Anonymous student feedback on the tools was uniformly positive. Since that semester, we have continued to refine and expand our tools’ analysis capabilities and performance, and plan to deploy the system again in the near future (the class is offered every Fall).