Binary lifting and formal verification of control algorithms in embedded firmware
Chen, Anthea
This item's files can only be accessed by the Administrator group.
Permalink
https://hdl.handle.net/2142/124686
Description
Title
Binary lifting and formal verification of control algorithms in embedded firmware
Author(s)
Chen, Anthea
Issue Date
2024-04-30
Director of Research (if dissertation) or Advisor (if thesis)
Levchenko, Kirill
Department of Study
Electrical & Computer Eng
Discipline
Electrical & Computer Engr
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
M.S.
Degree Level
Thesis
Keyword(s)
Security
Emulation
Industrial Control
Fuzzing
Lifting
Language
eng
Abstract
In this thesis, I present two novel contributions: ANANKE, a framework for abstracting control algorithms in firmware by dynamically rewriting and reducing symbolic expressions during symbolic execution, and an emulation-based fuzzing framework for GPU firmware security testing. ANANKE extends the symbolic execution system angr to skip program regions and replace them with abstractions while maintaining the integrity of the symbolic state’s semantics. The framework allows users to nest abstractions, creating an extensible lifting framework. ANANKE’s effectiveness is demonstrated by lifting continuous equations from quad-copter and PLC firmware, uncovering bugs and reproducing attacks. The GPU fuzzing framework combines the Unicorn emulation engine, AFL fuzzer, and custom GPU models to uncover vulnerabilities in GPU firmware and drivers. The framework targets the device manager communication protocol and modules written in Ada/SPARK, demonstrating the effectiveness of emulation-based fuzzing for GPU security testing. The thesis contributions include: (1) ANANKE a tool for lifting control algorithms from firmware binaries; (2) a specification language for symbolic expression rewriting and program region abstraction; (3) a demonstration of ANANKE on real-world firmware; (4) an emulation-based fuzzing framework for GPU firmware security testing; and (5) an exploration of fuzzing techniques on NVIDIA Hopper/Blackwell GPU firmware, complementing Ada/SPARK’s formal verification.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
