Emulation-based security measurement with applications in avionics, redaction, and industrial control

The safety of critical systems and data is of paramount importance to society. Attacks on these systems can have catastrophic consequences, and the security of these systems is often difficult to measure. Existing methods often involve access to an operating version of the system, such as a physical device or executable specification, to provide ground-truth. However, access to a complete representation of the system is not always possible or practical. In this dissertation, we explore the use of emulation to measure the security of systems in the absence of this ground-truth information. Complex system emulation often requires sophisticated approaches to digital forensics and tactics for navigating undecidability resulting from uncertainty of the system's state. To address these challenges, we present intelligent guess-and-check strategies for deducing hidden information in executable code in the absence of original source code or other auxiliary information. Our core technical contributions are (1) the first symbolic execution based firmware rehosting system, used to generate emulations of embedded systems. (2) A novel system for the analysis and recovery of glyph positioning information in PDF documents. This system was used to recover redacted text information where the characters were removed in hundreds of sensitive documents. (3) A logic-based intermediate representation and framework for the extraction of lifted function summaries from binary firmware. This framework makes existing verification and synthesis techniques applicable to real-world systems by translating implemented code to mathematical models. Where appropriate, we justify our strategies through discussions of correctness, precision, and generalizability. Our results are never theoretical: we apply them to pre-existing, empirically validatable domain rather than models: among others, we study the Communication Management Unit used in Boeing 737 Aircraft, historically important redacted documents, and a programmable logic controller operating a Tennessee Eastman chemical plant reactor pressure valve.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2023

Author dc:creator

• Bland, Maxwell

Contributors dc:contributor

• Levchenko, Kirill
• Bates, Adam
• Schulman, Aaron
• Wang, Gang

• Emulation
• Industrial Control
• Rehosting
• Information Leaks
• Lifting
• Security
• Privacy
• Redactions
• Avionics

Statement dc:rights

• Copyright 2023 Maxwell Bland

Language dc:language

en, eng

Handle dc:identifier

https://hdl.handle.net/2142/121481

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F121481