Closed JoranHonig closed 5 years ago
For the abstraction layer, how is about pysmt (https://github.com/pysmt/pysmt)? It uses SMT-Lib format to interact with SMT/SAT solvers and has supported many popular solvers, including Z3 and CVC4.
@hzzhang , Thats quite interesting, will look into that
@hzzhang That still leaves taint analysis unimplemented
we can implement an interface between pysmt and mythril where we can implement stuff like taint .
@JoranHonig @norhh Agree, another interface would be needed.
@JoranHonig If no one has already been working on this, I'd like to take it.
@hzzhang Go ahead and pick this up :+1:
I'm going to take this over because @hzzang doesn't have time to work on this right now.
I've looked into the following three options:
Roll our own abstraction layer Possible, and it would allow us to build a solution that exactly fits our needs. But would take more time than the other two options
Extend pySMT This is the approach that hzzang took. In the pr we see that a symbol manager can be used to store properties for each symbol. However, this doesn't allow us to taint or annotate expressions, therefore it doesn't fully fit our needs yet.
Use claripy
Description
Currently we are directly using z3 objects in laser, and are often directly using the z3 api. This has a few downsides.
Details
Abstraction layer
To solve this problem we should build abstraction around SMT solving logic, which would provide an interface along the lines of https://github.com/angr/claripy.
Taint analysis
For the dynamic taint analysis we'd need to be able to taint a bitvector multiple times, and to distinguish the different taints. This is required because different analysis modules will run at the same time, and the integer overflow detection should not look for tainted variables from another module.