SE4PY: a Symbolic Execution Tool for Python
Linhan Li
Author
08/03/2021
Added
83
Plays
Description
SE4PY: a Symbolic Execution Tool for Python. Supervised by Dr. ThanhVu Nguyen.
Searchable Transcript
Toggle between list and paragraph view.
- [00:00:00.000]Hi,
- [00:00:04.730]dear audience.
- [00:00:06.140]My name is Lehan Li and my project is [inaudible]
- [00:00:11.110]P Y a symbolic execution tool for Python script.
- [00:00:16.040]This project is under the guidance of Dr.
- [00:00:21.020]ThanhVu Nguyen from the computer science and engineering
- [00:00:25.700]department at the university of Nebraska at Lincoln.
- [00:00:34.400]So first of all, I'm going to briefly talk about symbolic execution.
- [00:00:40.100]So symbolic execution is a technique using software testing and
- [00:00:44.660]verification
- [00:00:47.510]in which we analyzed the program statically and by
- [00:00:52.430]statically, we mean we analyze it without actually
- [00:00:57.920]running the program.
- [00:01:00.800]So no input it's and
- [00:01:05.620]it's good for test case generation and obtaining cold
- [00:01:10.100]coverages.
- [00:01:14.030]The motivation for our project is because our other
- [00:01:18.830]project or in need of a symbolic execution tool
- [00:01:23.780]for Python, and there's no such tool exist.
- [00:01:28.070]So we've decided to implement well by our own.
- [00:01:36.290]And here are our objectives.
- [00:01:39.590]So we want to learn the program's behavior and
- [00:01:43.730]generalized their input and output.
- [00:01:49.280]And
- [00:01:52.670]also like to determine the reachability of code and January test
- [00:01:57.470]cases that can optimize the coverages
- [00:02:04.400]and by coverages. Well, here, we mean,
- [00:02:08.870]we would like to
- [00:02:11.690]cover as much lines of code as possible with a
- [00:02:16.370]small amount of test cases.
- [00:02:20.390]So to achieve these, we first applied symbolic execution,
- [00:02:26.240]Python script,
- [00:02:27.230]and along the symbolic execution,
- [00:02:32.660]we collect the program programs, behavior as constraints.
- [00:02:38.240]And those collective constraints later can be used to analyze
- [00:02:43.070]the program or solved by an
- [00:02:48.860]SMT solver to solve for the
- [00:02:53.780]concrete input that care leads to those lines of code.
- [00:03:00.370]And here are some diamonds and they are simplified for the purpose
- [00:03:05.140]of demonstration.
- [00:03:08.260]So what happens here is that symbolic
- [00:03:12.880]execution allows the execution to advance without knowing
- [00:03:17.890]the actual input.
- [00:03:21.610]And as you can see over here, we have an IF statement,
- [00:03:26.800]whatever the symbolic execution reaches,
- [00:03:30.490]a branch in the coat,
- [00:03:32.740]it will split up into two separate branches and continue
- [00:03:37.510]on each one of the branch separately.
- [00:03:41.770]This is different from concrete execution in which
- [00:03:46.810]only one branch can be chose to end executed at a
- [00:03:51.520]single time. And whenever,
- [00:03:56.140]the symbolic execution hit vtrace function,
- [00:03:59.530]which was a function.
- [00:04:01.240]We sat up for tracing the
- [00:04:05.620]execution. Well,
- [00:04:08.800]I'll put the path and generate the proper input.
- [00:04:13.270]That can be two point if, if such input exist.
- [00:04:18.970]as you can see,
- [00:04:23.350]we have ax equals 400 and the F conditional for the
- [00:04:27.820]FFC statement is X smaller than C roles.
- [00:04:32.410]So the bead phase can never be reached in,
- [00:04:37.540]I mean, during, uh, how quick execution.
- [00:04:42.070]So as you can see,
- [00:04:43.660]we have those classic collected constraints.
- [00:04:48.040]However, we were not able to generate a solution for the
- [00:04:54.250]path,
- [00:04:59.880]And for test b
- [00:05:02.100]here the program split up into two
- [00:05:06.600]branches and we were able to generate input for each of them.
- [00:05:17.580]So in conclusion,
- [00:05:20.550]the creation of this tool it's successful and it provides means for
- [00:05:25.740]software developers to analyze and test their
- [00:05:30.270]code. And in the future,
- [00:05:33.210]we plan to support more the data types and
- [00:05:38.010]this will be integrated into a visual studio
- [00:05:42.600]code extension,
- [00:05:44.700]and it will be made available to the developers.
- [00:05:53.880]And here are some works referenced or used in this
- [00:05:58.820]project, the fuzzing book as a book by
- [00:06:04.130]the authors of here and
- [00:06:08.060]sort of like a reference manual for this
- [00:06:12.920]project and the Z3 SMT,
- [00:06:16.400]solver is another tool by Microsoft.
- [00:06:20.270]It provides functionality for primarily in this project.
- [00:06:25.130]That's just solving constraints.
- [00:06:28.630][inaudible].
- [00:06:32.470]And.
- [00:06:34.810]At the end, I would like to give special, thanks to Dr.
- [00:06:38.320]Nguyen, who inspired me to develop this tool and
- [00:06:43.060]introduced me to you on the undergraduate research.
- [00:06:46.360]And I will like to thank UCARE
- [00:06:51.280]as well, this project was made possible by their founding.
- [00:06:56.500]And that's all. Thank you for your time.
The screen size you are trying to search captions on is too small!
You can always jump over to MediaHub and check it out there.
Log in to post comments
Embed
Copy the following code into your page
HTML
<div style="padding-top: 56.25%; overflow: hidden; position:relative; -webkit-box-flex: 1; flex-grow: 1;">
<iframe
style="bottom: 0; left: 0; position: absolute; right: 0; top: 0; border: 0; height: 100%; width: 100%;"
src="https://mediahub.unl.edu/media/17606?format=iframe&autoplay=0"
title="Video Player: SE4PY: a Symbolic Execution Tool for Python"
allowfullscreen
></iframe>
</div>
Comments
0 Comments