Static Symbolic Execution in SVF

Zhang, Guanqin

Static Symbolic Execution in SVF

Zhang, Guanqin

Permalink

Publication Type:: Thesis
Issue Date:: 2022

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download contents and abstractAdobe PDF (195.36 kB)

Adobe PDF

Download thesisAdobe PDF (517.1 kB)

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Zhang, Guanqin
dc.date.accessioned	2022-10-04T01:36:07Z
dc.date.available	2022-10-04T01:36:07Z
dc.date.issued	2022
dc.identifier.uri	http://hdl.handle.net/10453/162275
dc.description	University of Technology Sydney. Faculty of Engineering and Information Technology.	en_US.UTF-8
dc.description.abstract	This thesis presents the implementation of a static symbolic execution (SSE) tool on top of SVF framework. SSE is a well-studied technique for program testing and verification, which is based on collecting the program execution paths and exploring the program behaviours in the form of the constraints. SSE replies on SVF-IR language to translate the program into logical formulas of a particular rules-based form which supplies useful program properties for use in the program analysis. SSE maintains all elements of program running data and its manipulations. More precisely, SSE traverses on program control flow graph and modulates program behaviours, e.g., buffer-over-flow is an anomaly in program, which can be identified that the data overruns the buffer’s boundary and overwrites adjacent memory locations. Experiments conducting our implementation of SSE indicates many benefits by using symbolic execution, e.g., depth-first searching on particular paths to mimic real program execution process, or finding certain program anomalies based on translating rules.	en_US.UTF-8
dc.format	Thesis (MAnalytics)
dc.language.iso	en_US	en_US.UTF-8
dc.relation	https://opus.lib.uts.edu.au/bitstream/10453/162275/2/02whole.pdf
dc.rights	The author owns the copyright in this thesis including all reproduction and reuse rights for the work. The work may not be altered without the permission of the copyright owner. Attribution is essential when quoting or paraphrasing from this thesis.
dc.rights	au.edu.uts.lib/ppc
dc.rights	info:eu-repo/semantics/openAccess
dc.title	Static Symbolic Execution in SVF	en_US.UTF-8
dc.type	Thesis
utslib.copyright.status	open_access	*

Abstract:

This thesis presents the implementation of a static symbolic execution (SSE) tool on top of SVF framework. SSE is a well-studied technique for program testing and verification, which is based on collecting the program execution paths and exploring the program behaviours in the form of the constraints. SSE replies on SVF-IR language to translate the program into logical formulas of a particular rules-based form which supplies useful program properties for use in the program analysis. SSE maintains all elements of program running data and its manipulations. More precisely, SSE traverses on program control flow graph and modulates program behaviours, e.g., buffer-over-flow is an anomaly in program, which can be identified that the data overruns the buffer’s boundary and overwrites adjacent memory locations. Experiments conducting our implementation of SSE indicates many benefits by using symbolic execution, e.g., depth-first searching on particular paths to mimic real program execution process, or finding certain program anomalies based on translating rules.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/162275