Current Maintainer: llylly (linyi2@illinois.edu, linyil.com) @ Secure Learning Lab, UIUC

This is a unified toolbox for representative robustness verification approaches for DNNs. The leaderboard for different approaches can be found here: https://github.com/AI-secure/Provable-Training-and-Verification-Approaches-Towards-Robust-Neural-Networks.

Related paper: SoK: Certified Robustness for Deep Neural Networks.

@inproceedings{li2023sok,
    title={SoK: Certified Robustness for Deep Neural Networks},
    author={Linyi Li and Tao Xie and Bo Li},
    booktitle={44th {IEEE} Symposium on Security and Privacy, {SP} 2023, San Francisco, CA, USA, 22-26 May 2023},
    publisher={IEEE},
    year={2023}
}

• What is robustness verification for DNNs?

  DNNs are vulnerable to adversarial examples. Given a model and an input x0, the robustness verification approaches can certify that there are no adversarial samples around x0 within radius r. The complete verification of DNNs is NP-complete [1,2]. Therefore, current verification approaches usually leverage relaxations, which results in outputting smaller r than the real one.

• What neural networks are supported?

  Currently, existing approaches mainly support image classification tasks for MNIST, CIFAR-10, and ImageNet, and our toolbox supports all of them though networks for ImageNet are usually too large for standard non-probabilistic verification approaches. Though a significant amount of verification approaches support skip connections, max-pooling layers, etc, typical verification approaches mainly work on feed-forward neural networks with ReLU activations, containing only fully-connected layers and convolutional layers.

Main Features:

1. A unified lightweight platform for running about 20 verification approaches in a simple PyTorch-based interface.
2. Easily extensible to your own customized neural networks.
3. Easily extensible to your own verification approaches.
4. High-efficiency benefited from the lightweight structure.

[1] Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. https://arxiv.org/abs/1702.01135.

[2] Towards Fast Computation of Certified Robustness for ReLU Networks. http://proceedings.mlr.press/v80/weng18a.html.

1. Find a server with GPU support and Linux / MacOS system. (The toolbox has been tested on Linux and MacOS. It should be possible to run on Windows, but we can't guarantee so.)

2. Prepare necessary datasets:

   1. If you only want to benchmark on MNIST and CIFAR-10, don't need to do anything, since PyTorch will automatically download them later.

   2. If you want to benchmark on ImageNet, in datasets.py, please set the Line 12 to the path of ImageNet dataset on your local environment. The dataset should be organized according to the instruction above Line 12.

3. Install necessary packages according to requirements.txt.

4. Download model weights at: https://drive.google.com/drive/folders/1vh7dwvn1P544r5rzOfJFPzShV4-UsTAv?usp=sharing, then store the whole folder as models_weights/exp_models/. Or if you like, you can also train and load your own models.

5. Set your global Keras settings in ~/.keras/keras.json as below.

{
    "floatx": "float32",
    "epsilon": 1e-07,
    "backend": "tensorflow",
    "image_data_format": "channels_first"
}

6. Install ELINA, and DeepG according to the instructions in eran/install.sh. Then specify their path in constants.py (Line 5 and Line 6).

7. Create an empty folder named tmp/ under the tool root path.

Then you are all set!

The experiments/run.sh and experiments/run_cifar.sh contain concrete commands for the users to replicate our results.

In the arguments of these commands, --method specifies the verification approaches to run, --dataset specifies the dataset to run, --model specifies the model to run, --weight specifies the model weight to run, and --mode specifies the type of evaluation to run. All of them supports multiple arguments, and multiple settings will be ran sequentially.

• --method: From experiments/data_analyzer, the dictionary approach_mapper defines the name mapping between paper's verification approach names to argument names.
• --dataset: It should be names in contants.py's DATASETS list.
• --model: ranging from A to G, where A = FCNNa, B = FCNNb, C = CNNa, D = CNNb, E = CNNc, F = CNNd, and G = FCNNc.
• --weight: same names as trained weight settings in the paper.
• --mode: should be either "verify" - compute the robust accuracy, or "radius" - compute the average certified robustness radius.

The main script main.py shows how to run the toolkit on your customized tasks.

To enable the support for new verification approaches, you could copy the implementation folder to the project root folder, then write your own adaptor following the adaptor.adaptor.Adaptor template, and strore it in adaptor/ folder.

To enable the support for your own model, you could write your model loading function in models/ (the function should load both structure and weights, and should be PyTorch model), and register the new model in model.py.

• If the model works on normalized input, you should treat the input normalization as the additional first layer of your model, and this first layer could be implemented by datasets.NormalizeLayer.
• If the model contains flatten layer, it should be replaced by our flatten layer implementation in models.zoo.Flatten.

To enable the support for new datasets, you could extend datasets.py, and register the dataset name in constants.py.

Our toolbox is based on following tools, which are stored in respective folders:

• cnn_cert/: from https://github.com/IBM/CNN-Cert
• convex_adversarial/: from https://github.com/locuslab/convex_adversarial
• crown_ibp/: from https://github.com/huanzhang12/CROWN-IBP
• eran/: from https://github.com/eth-sri/eran
• recurjac/: from https://github.com/huanzhang12/RecurJac-and-CROWN

To provide a uniform interface for them, we utilize the "adaptor design pattern", where we write a class to provide uniform methods for each approach in these tools. All classes are in folder adaptor/, and inherited from adaptor.adaptor.Adaptor class.

The adaptor.adaptor.Adaptor class should be initialized by dataset and model, and provides two main methods: verify(self, input, label, norm_type, radius) and calc_radius(self, input, label, norm_type, upper=0.5, eps=1e-2).

The verify() method receives the input, true label, Lp norm type, and radius. It returns true or false.

The calc_radius() method receives the input, true label, Lp norm type, the maximum possible radius, and the precision. It by default implements a binary-search based procedure which calls verify() multiples times to compute robustness radius.

The basic/ folder includes our own reimplementation of a few verification approaches.

The experiments/ folder contains our raw experiment data.

The models/ folder contains the full definitions of the model structure used in the experiments. You can extend it to more models.

constants.py defines important global constants.

• If you want to improve the toolbox for more norm types, datasets, or verification approaches, remember to update them here.

datasets.py contains the dataset preparation scripts.

model.py indexes the models defined in models/, it contains a large dictionary, which maps the string indexes to concrete methods in models/ which loads the models.

main.py: the toggle entrance for runing all the verification approaches.

A significant amount of code in this project is embeded and adapted from existing open-sourced repositories. For those code, we keep all the source labels and author tags without modifications. We tried to list all the sources thoroughly above, but may still miss some. If you feel this tool violates your copyright, we apologize in advance and please contact us immediately.

For all other original parts, we allow free distribution of the code under the MIT license.

We plan to provide an uniform interface for C++-based verification approaches, including Reluplex, Neurify, ReluVal, etc.

For recently popular randomized smoothing series approaches, we may provide a separate tool in the future.