Fuzbolic Project: Path Constraint Classifier
This repository provides the implementation of Path Constraint Classifier (PCC), which is a novel symbolic execution module to support solver selection functionality. Given a set of path constraint, PCC will predict a fatest solver according the characteristics of the input path constraint.
Usage & Simple Example
Please take a look of the tutorial scripts in the
It will tell you how to perform PCC to:
- Extract path constraint features
- Evaluate solver performance
- Generate machine learning data for training / testing
- Train and test the performance of a model
To reproduce the experiment results in the thesis, please take a look at the script in
- Feature Extractor (
- Constraint Feature Cache (
- Machine Learning Module (Implement in each model in
- Solver Selection Interface/Module (
- Classifier: Not explicitly implemented, but one can use
model.test()to perform similar operation. E.g.
- FeatureProcessor (
feature.FeatureProcessor): Normalize the numeric value of features to avoid training failure.
- SolverEvaluator (
- AnswerEvaluator (
- PredictionEvaluator (
- DataPartitioner (
- DataCombiner (
To be continue.
To be continue.
- Data and Solvers
- Collect more symbolic data (more binaries)
- Import more SMT solvers
- Machine Learning
- Feature engineering / minimization (Dominating features)
- Model design and training a. More DNN Layer? b. Better loss function?
- Integrate to an exisiting symbolic execution engine
- Angr or KLEE?
- Solving Procedure Design
- Backup Solver: More backup solver to use?
- Logic Selection
- Other Optimization