MSc Thesis Presentation - Sepehr Noorafshan

Name: Sepehr Noorafshan

Date: Friday, Sept. 26th

Time: 10 am

Location: X836

Supervisor: Margo Seltzer

Zoom: https://ubc.zoom.us/j/517560312?pwd=Und6RjFXK2N0TkRKVUxjcTd0Y0w4UT09

Meeting ID: 517 560 312

Passcode: 424183

Title: Synthesizing Device Emulators

Abstract:
Emulators, such as the Quick Emulator (QEMU), support peripheral device emulation, enabling early software development and platform prototyping on architectures such as ARM and x86. How- ever, peripheral emulators often contain two classes of bugs: behavioural bugs, which arise when emulated behaviour diverges from the hardware specification—either unintentionally or due to simplifying assumptions —and implementation bugs, caused by programming errors or undefined behaviour in the implementation language.

This work presents a systematic approach for emulator developers to construct models and generate device emulators with correctness guarantees, using a combination of formal specifications and program synthesis. The first step is to model device behaviour and internal state in Temporal Logic of Actions (TLA+), yielding a specification that can be independently model-checked for consistency across different operations. Next, a custom transpiler converts the TLA+ specification into a program in Rosette, a solver-aided language that supports symbolic execution and program synthesis. The transpiler encodes the device behaviour as pre- and post-conditions on specific de- vice functionality, such as register accesses, over a symbolic device state and execution context. To reduce synthesis time and complexity, I introduce a domain-specific language (DSL) in Rosette, equipped with an interpreter and a C transpiler, to abstract away the complexity of C as the target implementation language. Given a grammar over DSL constructs, Rosette uses symbolic execution to encode the space of candidate DSL programs, along with the constraints in the specification, as a Satisfiability Modulo Theories (SMT) query and sends it to an SMT solver, such as Z3. The solver then either finds a given assignment to the SMT formula that corresponds to a concrete DSL program that satisfies the specified constraints or returns unsatisfiable when it cannot find such an assignment. The C-transpiler then emits the corresponding C function to the DSL program. As two case studies, I apply this methodology to the PL011 UART, a serial device, and the PL061 GPIO controller, both commonly used in ARM platforms and emulated in QEMU. Upon evaluation, this approach identified an assertion violation, revealing a bug in the Linux PL011 serial driver.