DeepConcolic
Concolic Testing for Deep Neural Networks
Install / Use
/learn @TrustAI/DeepConcolicREADME
DeepConcolic (Testing for Deep Neural Networks)

The tutorial document for this repository is in (tutorial.pdf)
General Introduction
This repository includes a few software packages, all of which are dedicated for the analysis of deep neural netowrks (or tree ensembles) over its safety and/or security properties.
- DeepConcolic, a coverage-guided testing tool for convolutional neural networks. Now, it includes a major upgrade based on Bayesian Network based Abstraction.
- testRNN, a coverage-guided testing tool for Long short-term memory models (LSTMs). LSTMs are a major class of recurrent neural networks.
- EKiML, a tool for backdoor embedding and detection for tree ensembles.
- GUAP: a generalised universal adversarial perturbation. It generates universersal adversarial perburbation that may be applied to many inputs at the same time.
In the following, after the installation and download of example models, we will present them one by one.
Installation
First of all, please set up a conda environment
conda create --name deepconcolic python==3.7
conda activate deepconcolic
This should be followed by installing software dependencies:
conda install opencv nltk matplotlib
conda install -c pytorch torchvision
pip3 install numpy==1.19.5 scipy==1.4.1 tensorflow\>=2.4 pomegranate==0.14 scikit-learn scikit-image pulp keract np_utils adversarial-robustness-toolbox parse tabulate pysmt saxpy keras menpo patool z3-solver pyvis
Download Example Models
We use Fashion-MNIST dataset as the running example. The following are two pre-trained mmodels, one larger and one smaller.
wget -P saved_models https://cgi.csc.liv.ac.uk/~acps/models/small_model_fashion_mnist.h5
wget -P saved_models https://cgi.csc.liv.ac.uk/~acps/models/large_model_fashion_mnist.h5
Tool 1 -- DeepConcolic: Concolic Testing for Convolutional Neural Networks
Concolic testing alternates between CONCrete program execution and symbOLIC analysis to explore the execution paths of a software program and to increase code coverage. In this paper, we develop the first concolic testing approach for Deep Neural Networks (DNNs). More specifically, we utilise quantified linear arithmetic over rationals to express test requirements that have been studied in the literature, and then develop a coherent method to perform concolic testing with the aim of better coverage. Our experimental results show the effectiveness of the concolic testing approach in both achieving high coverage and finding adversarial examples.
The paper is available at https://arxiv.org/abs/1805.00089.
In the following, we first present the original ASE2018 version, and then introduce two new upgrades (fuzzing engine and Bayesian network based abstraction).
ASE2018 Version
Work Flow

Sample Results

Command to Run
usage: python3 -m deepconcolic.main [-h] --dataset
{OpenML:har,cifar10,fashion_mnist,mnist}
--model MODEL --outputs DIR --criterion
{nc,ssc,ssclp,bfc,bfdc} --norm {l0,linf}
[--setup-only] [--init INT]
[--max-iterations INT] [--save-all-tests]
[--rng-seed SEED]
[--extra-tests DIR [DIR ...]]
[--filters {LOF}] [--norm-factor FLOAT]
[--lb-hard FLOAT] [--lb-noise FLOAT]
[--mcdc-cond-ratio FLOAT]
[--top-classes CLS]
[--layers LAYER [LAYER ...]]
[--feature-index INT] [--dbnc-spec SPEC]
[--dbnc-abstr PKL]
Concolic testing for Neural Networks
optional arguments:
-h, --help show this help message and exit
--dataset {OpenML:har,cifar10,fashion_mnist,mnist}
selected dataset
--model MODEL the input neural network model (.h5 file or "vgg16")
--outputs DIR the output test data directory
--criterion {nc,ssc,ssclp,bfc,bfdc}
the test criterion
--norm {l0,linf} the norm metric
--setup-only only setup the coverage critierion and analyzer, and
terminate before engine initialization and startup
--init INT number of test samples to initialize the engine
--max-iterations INT maximum number of engine iterations (use < 0 for
unlimited)
--save-all-tests save all generated tests in output directory; only
adversarial examples are kept by default
--rng-seed SEED Integer seed for initializing the internal random
number generator, and therefore get some(what)
reproducible results
--extra-tests DIR [DIR ...], +i DIR [DIR ...]
additonal directories of test images
--filters {LOF} additional filters used to put aside generated test
inputs that are too far from training data (there is
only one filter to choose from for now; the plural is
used for future-proofing)
--norm-factor FLOAT norm distance upper threshold above which generated
inputs are rejected by the oracle (default is 1/4)
--lb-hard FLOAT hard lower bound for the distance between original and
generated inputs (concolic engine only---default is
1/255 for image datasets, 1/100 otherwise)
--lb-noise FLOAT extra noise on the lower bound for the distance
between original and generated inputs (concolic engine
only---default is 1/10)
--mcdc-cond-ratio FLOAT
the condition feature size parameter (0, 1]
--top-classes CLS check the top-CLS classifications for models that
output estimations for each class (e.g. VGG*)
--layers LAYER [LAYER ...]
test layers given by name or index
--feature-index INT to test a particular feature map
--dbnc-spec SPEC Feature extraction and discretisation specification
--dbnc-abstr PKL, --bn-abstr PKL
input BN abstraction (.pkl)
The neural network model under tested is specified by --model and a set of raw test data should be given
by using --inputs. Some popular datasets like MNIST and CIFAR10 can be directly specified by using the
--dataset option directly. --criterion is used to choose the coverage
criterion and --norm helps select the norm metric to measure the distance between inputs. Some examples
to run DeepConcolic are in the following.
To run an MNIST model
python -m deepconcolic.main --model saved_models/mnist_complicated.h5 --dataset mnist --outputs outs/
To run an CIFAR10 model
python -m deepconcolic.main --model saved_models/cifar10_complicated.h5 --dataset cifar10 --outputs outs/
To test a particular layer
python -m deepconcolic.main --model saved_models/cifar10_complicated.h5 --dataset cifar10 --outputs outs/ --layers 2
To run MC/DC for DNNs on the CIFAR-10 model
python -m deepconcolic.main --model saved_models/cifar10_complicated.h5 --criterion ssc --mcdc-cond-ratio 0.1 --dataset cifar10 --outputs outs
<!-- NB: temporary comment as --inputs argument is about to disapear:
To run MC/DC for DNNs on the VGG16 model (with input images from the ``data`` sub-directory)
```sh
python -m deepconcolic.main --model vgg16 --inputs data/ --outputs outs --mcdc-cond-ratio 0.1 --top-classes 5 --labels labels.txt --criterion ssc
```
-->
To run Concolic Sign-sign-coverage (MC/DC) for DNNs on the MNIST model
python -m deepconcolic.main --model saved_models/mnist_complicated.h5 --dataset mnist --outputs outs --criterion ssclp
Bayesian Network based Abstraction
To run Concolic BN-based Feature coverage (BFCov) for DNNs on the MNIST model
python -m deepconcolic.main --model saved_models/mnist_complicated.h5 --criterion bfc --norm linf --dataset mnist --outputs outs --dbnc-spec dbnc/example.yaml
See the example YAML specification for details on how to configure the BN-based abstraction.
To run Concolic BN-based Feature-dependence coverage (BFdCov) for DNNs on the MNIST model
python -m deepconcolic.main --model saved_models/mnist_complicated.h5 --criterion bfdc --norm linf --dataset mnist --outputs outs --dbnc-spec dbnc/example.yaml
You could adjust the following two parameters in the DBNC specification file defined by --dbnc-spec to dump the generated bayesian network to files bn4trained.yml and bn4tests.yml.
dump_bn_with_trained_dataset_distribution: True,
dump_bn_with_final_dataset_distribution: True,
Fuzzing Engine
DeepConcolic additionally features an experimental fuzzing engine. The following command illustrates how to exercise this engine on a classifier for the CIFAR10 dataset: it will generate at most 1000 images obtained by mutating inputs randomly drawn from the CIFAR10 validation dataset, and save them into the outs/cifar10-fuzzing-basic directory. Aversarial examples can be identified in the latter directory by searching for files named <test-number>-adv-<wrong-label>.png, derived from file <test-number>-original-<true-label>.png. Passed tests are named in a similar way, as <test-number>-ok-<label>.png.
python3 -m deepconcolic.fuzzer --dataset cifar10 -
