{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/124686"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/124686","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Binary lifting and formal verification of control algorithms in embedded firmware","abstract":"Submission published under a 24 month embargo labeled 'Closed Access', the embargo will last until 2026-05-01","abstract_html":"Submission published under a 24 month embargo labeled 'Closed Access', the embargo will last until 2026-05-01","abstract_has_math":false,"creators":["Chen, Anthea"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Electrical & Computer Engr","degree_department":null,"school":null,"contributors":["Levchenko, Kirill"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2024,"date_issued":"2024-05","date_published":"2024-05","updated_at":"2026-07-22T22:25:02Z","subjects":["Security","Emulation","Industrial Control","Fuzzing","Lifting"],"languages":["en","eng"],"rights":["Copyright 2024 Anthea Chen"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/124686","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Levchenko, Kirill"]},{"key":"dc:creator","label":"Author","values":["Chen, Anthea"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2024-05","2024-04-30"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical & Computer Engr"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Security","Emulation","Industrial Control","Fuzzing","Lifting"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en","eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2024 Anthea Chen"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/124686"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Submission published under a 24 month embargo labeled 'Closed Access', the embargo will last until 2026-05-01","The student, Anthea Chen, accepted the attached license on 2024-04-22 at 20:01.","The student, Anthea Chen, submitted this Thesis for approval on 2024-04-22 at 20:02.","This Thesis was approved for publication on 2024-04-30 at 14:52.","DSpace SAF Submission Ingestion Package generated from Vireo submission #20561 on 2024-09-16 at 00:50:05","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."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Binary lifting and formal verification of control algorithms in embedded firmware"]}]}],"canonical_facts":{"dc:contributor":["Levchenko, Kirill"],"dc:creator":["Chen, Anthea"],"dc:date":["2024-05","2024-04-30"],"dc:description":["Submission published under a 24 month embargo labeled 'Closed Access', the embargo will last until 2026-05-01","The student, Anthea Chen, accepted the attached license on 2024-04-22 at 20:01.","The student, Anthea Chen, submitted this Thesis for approval on 2024-04-22 at 20:02.","This Thesis was approved for publication on 2024-04-30 at 14:52.","DSpace SAF Submission Ingestion Package generated from Vireo submission #20561 on 2024-09-16 at 00:50:05","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."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/124686"],"dc:language":["en","eng"],"dc:rights":["Copyright 2024 Anthea Chen"],"dc:subject":["Security","Emulation","Industrial Control","Fuzzing","Lifting"],"dc:title":["Binary lifting and formal verification of control algorithms in embedded firmware"],"dc:type":["text"],"thesis:degree_discipline":["Electrical & Computer Engr"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:02Z"}