Accurate binary-level symbolic execution of embedded firmware
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
Accurate_Binary-Level_Symbolic_Execution_of_Embedded_Firmware.pdf | 6.31 MB | Adobe PDF | Anzeigen |
Autor/Autorin: | Tempel, Sören ![]() |
BetreuerIn: | Drechsler, Rolf ![]() |
1. GutachterIn: | Drechsler, Rolf ![]() |
Weitere Gutachter:innen: | Baccelli, Emmanuel ![]() |
Zusammenfassung: | Symbolic execution is an automated software testing technique that has enabled the discovery of numerous bugs in conventional, non-embedded software. Unfortunately, its application to embedded firmware is presently limited due to unique challenges associated with this domain. Central to many of these challenges is the tight integration of hardware and software components. Due to this tight integration, firmware interacts on a low abstraction level with both the processor and the peripherals provided by a hardware platform. In order to support these interactions, a symbolic execution engine needs to implement the reference manuals specifying processor and peripheral behavior. These specifications have an enormous complexity; hence, prior work approximates peripheral behavior and abstracts processor instruction execution. Unfortunately, these approximations may induce inaccuracies, which can result in bugs being missed in the tested firmware. This dissertation accomplishes a more accurate analysis by contributing a binary-level symbolic execution approach that is faithful to both the specification of peripheral behavior and processor instruction execution. This is achieved by facilitating machine-readable formal descriptions of instruction semantics and an established modeling standard for the description of peripheral behavior. Conducted experiments have resulted in the discovery of 16 previously unknown bugs in a popular embedded operating system, thereby illustrating the effectiveness of the proposed approach. |
Schlagwort: | symbolic execution; embedded systems; SystemC | Veröffentlichungsdatum: | 14-Jun-2024 | Dokumenttyp: | Dissertation | DOI: | 10.26092/elib/3090 | URN: | urn:nbn:de:gbv:46-elib80569 | Forschungsdatenlink: | https://doi.org/10.5281/zenodo.7515748 https://doi.org/10.5281/zenodo.6802198 https://doi.org/10.5281/zenodo.5091709 https://doi.org/10.5281/zenodo.10925791 https://doi.org/10.5281/zenodo.7817414 https://doi.org/10.24433/CO.7255660.v1 |
Institution: | Universität Bremen | Fachbereich: | Fachbereich 03: Mathematik/Informatik (FB 03) |
Enthalten in den Sammlungen: | Dissertationen |
Seitenansichten
430
checked on 31.08.2024
Download(s)
137
checked on 31.08.2024
Google ScholarTM
Prüfe
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.