elib
DLR-Header
DLR-Logo -> http://www.dlr.de
DLR Portal Home | Imprint | Privacy Policy | Contact | Deutsch
Fontsize: [-] Text [+]

Dynamic Symbolic Execution for Enhanced Intermediate Representation of Data Flow Space Applications

Abdelmaksoud, Hany (2022) Dynamic Symbolic Execution for Enhanced Intermediate Representation of Data Flow Space Applications. Master's, Technische Universität Hamburg.

[img] PDF
2MB

Abstract

Verifying the safety and security requirements of embedded software requires a code analysis. Many software systems are developed based on software development libraries; therefore, code specifications are known at compiling time. Hence, many source-code analyses will be excluded, and low-level intermediate representations (LLIRs) of the analyzed binaries are preferred. Improving the expressiveness of the LLIR and enhancing it with more information from the binaries will improve the tightness of the applied analyses. This work is interested in developing a lifterthat lifts binaries into an enhanced LLIR and can resolve indirect jumps. LLVM is used as the LLIR. Our proposed lifter, which we call DEL (Dynamic symbolic Execution Lifter), combines both static and dynamic symbolic execution and strives to fully recover the analyzed program’s control flow. DEL consists of an API to translate ARMv7-M assembly instructions into static single assignment LLVM instructions, an LLIR to Z3 expressions parser, a memory model, a register model, and a specialized condition flags handler. This work used a case study based on a software development library for onboard data-handling applications developed at the German Aerospace Center (DLR), which is called the Tasking Framework. DEL demonstrated high accuracy of around 93% in resolving indirect jumps in our case study.

Item URL in elib:https://elib.dlr.de/185518/
Document Type:Thesis (Master's)
Title:Dynamic Symbolic Execution for Enhanced Intermediate Representation of Data Flow Space Applications
Authors:
AuthorsInstitution or Email of AuthorsAuthor's ORCID iD
Abdelmaksoud, Hanyhany.abdelmaksoud (at) tuhh.deUNSPECIFIED
Date:25 March 2022
Refereed publication:No
Open Access:Yes
Gold Open Access:No
In SCOPUS:No
In ISI Web of Science:No
Status:Published
Keywords:symbolic execution Binary analysis
Institution:Technische Universität Hamburg
HGF - Research field:Aeronautics, Space and Transport
HGF - Program:Space
HGF - Program Themes:Space System Technology
DLR - Research area:Raumfahrt
DLR - Program:R SY - Space System Technology
DLR - Research theme (Project):R - ScOSA Flight Experiment
Location: Braunschweig
Institutes and Institutions:Institute for Software Technology > Software for Space Systems and Interactive Visualisation
Deposited By: Haj Hammadeh, Zain Alabedin
Deposited On:01 Jun 2022 13:01
Last Modified:01 Jun 2022 13:01

Repository Staff Only: item control page

Browse
Search
Help & Contact
Information
electronic library is running on EPrints 3.3.12
Website and database design: Copyright © German Aerospace Center (DLR). All rights reserved.