{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,25]],"date-time":"2026-03-25T02:19:03Z","timestamp":1774405143240,"version":"3.50.1"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031131844","type":"print"},{"value":"9783031131851","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,7]],"date-time":"2022-08-07T00:00:00Z","timestamp":1659830400000},"content-version":"vor","delay-in-days":218,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Neural networks have achieved state-of-the-art performance in solving many problems, including many applications in safety\/security-critical systems. Researchers also discovered multiple security issues associated with neural networks. One of them is backdoor attacks, i.e., a neural network may be embedded with a backdoor such that a target output is almost always generated in the presence of a trigger. Existing defense approaches mostly focus on detecting whether a neural network is \u2018backdoored\u2019 based on heuristics, e.g., activation patterns. To the best of our knowledge, the only line of work which certifies the absence of backdoor is based on randomized smoothing, which is known to significantly reduce neural network performance. In this work, we propose an approach to verify whether a given neural network is free of backdoor with a certain level of success rate. Our approach integrates statistical sampling as well as abstract interpretation. The experiment results show that our approach effectively verifies the absence of backdoor or generates backdoor triggers.<\/jats:p>","DOI":"10.1007\/978-3-031-13185-1_9","type":"book-chapter","created":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T19:29:09Z","timestamp":1659814149000},"page":"171-192","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Verifying Neural Networks Against Backdoor Attacks"],"prefix":"10.1007","author":[{"given":"Long H.","family":"Pham","sequence":"first","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,7]]},"reference":[{"issue":"1","key":"9_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158668","volume":"28","author":"G Agha","year":"2018","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. (TOMACS) 28(1), 1\u201339 (2018)","journal-title":"ACM Trans. Model. Comput. Simul. (TOMACS)"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Barni, M., Kallas, K., Tondi, B.: A new backdoor attack in CNNs by training set corruption without label poisoning. In: ICIP 2019, pp. 101\u2013105. IEEE (2019)","DOI":"10.1109\/ICIP.2019.8802997"},{"key":"9_CR3","unstructured":"Bojarski, M., et al.: End to end learning for self-driving cars. arXiv preprint arXiv:1604.07316 (2016)"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Carlini, N., Wagner, D.: Towards evaluating the robustness of neural networks. In: S &P 2017, pp. 39\u201357. IEEE (2017)","DOI":"10.1109\/SP.2017.49"},{"key":"9_CR5","unstructured":"Chen, B., et al.: Detecting backdoor attacks on deep neural networks by activation clustering. arXiv preprint arXiv:1811.03728 (2018)"},{"key":"9_CR6","unstructured":"Chen, X., Liu, C., Li, B., Lu, K., Song, D.: Targeted backdoor attacks on deep learning systems using data poisoning. arXiv preprint arXiv:1712.05526 (2017)"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Dong, Y., et al.: Boosting adversarial attacks with momentum. In: CVPR 2018, pp. 9185\u20139193. IEEE (2018)","DOI":"10.1109\/CVPR.2018.00957"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-319-68167-2_19","volume-title":"Automated Technology for Verification and Analysis","author":"R Ehlers","year":"2017","unstructured":"Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 269\u2013286. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_19"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Gao, Y., Xu, C., Wang, D., Chen, S., Ranasinghe, D.C., Nepal, S.: Strip: a defence against trojan attacks on deep neural networks. In: ACSAC 2019, pp. 113\u2013125. ACM (2019)","DOI":"10.1145\/3359789.3359790"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: Ai2: Safety and robustness certification of neural networks with abstract interpretation. In: S &P 2018, pp. 3\u201318. IEEE (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"9_CR11","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. arXiv preprint arXiv:1412.6572 (2014)"},{"key":"9_CR12","unstructured":"Gu, T., Dolan-Gavitt, B., Garg, S.: Badnets: Identifying vulnerabilities in the machine learning model supply chain. arXiv preprint arXiv:1708.06733 (2017)"},{"key":"9_CR13","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2021). https:\/\/www.gurobi.com"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"Computer Aided Verification","author":"X Huang","year":"2017","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety Verification of Deep Neural Networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient smt solver for verifying deep neural networks. In: CAV 2017, pp. 97\u2013117. Springer (2017)","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Li, Q., Cai, W., Wang, X., Zhou, Y., Feng, D.D., Chen, M.: Medical image classification with convolutional neural network. In: ICARCV 2014, pp. 844\u2013848. IEEE (2014)","DOI":"10.1109\/ICARCV.2014.7064414"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-030-00470-5_13","volume-title":"Research in Attacks, Intrusions, and Defenses","author":"K Liu","year":"2018","unstructured":"Liu, K., Dolan-Gavitt, B., Garg, S.: Fine-pruning: defending against backdooring attacks on deep neural networks. In: Bailey, M., Holz, T., Stamatogiannakis, M., Ioannidis, S. (eds.) RAID 2018. LNCS, vol. 11050, pp. 273\u2013294. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-00470-5_13"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Liu, Y., Lee, W.C., Tao, G., Ma, S., Aafer, Y., Zhang, X.: Abs: scanning neural networks for back-doors by artificial brain stimulation. In: CCS 2019, pp. 1265\u20131282. ACM (2019)","DOI":"10.1145\/3319535.3363216"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Liu, Y., Ma, S., Aafer, Y., Lee, W.C., Zhai, J., Wang, W., Zhang, X.: Trojaning attack on neural networks (2017)","DOI":"10.14722\/ndss.2018.23291"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-030-58607-2_11","volume-title":"Computer Vision \u2013 ECCV 2020","author":"Y Liu","year":"2020","unstructured":"Liu, Y., Ma, X., Bailey, J., Lu, F.: Reflection backdoor: a natural backdoor attack on deep neural networks. In: Vedaldi, A., Bischof, H., Brox, T., Frahm, J.-M. (eds.) ECCV 2020. LNCS, vol. 12355, pp. 182\u2013199. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58607-2_11"},{"key":"9_CR21","unstructured":"Lu, J., Kumar, M.P.: Neural network branching for neural network verification. arXiv preprint arXiv:1912.01329 (2019)"},{"key":"9_CR22","unstructured":"Mirman, M., Gehr, T., Vechev, M.: Differentiable abstract interpretation for provably robust neural networks. In: ICML 2018, pp. 3578\u20133586. PMLR (2018)"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Moosavi-Dezfooli, S.M., Fawzi, A., Fawzi, O., Frossard, P.: Universal adversarial perturbations. In: CVPR 2017, pp. 1765\u20131773. IEEE (2017)","DOI":"10.1109\/CVPR.2017.17"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Papernot, N., McDaniel, P., Jha, S., Fredrikson, M., Celik, Z.B., Swami, A.: The limitations of deep learning in adversarial settings. In: EuroS &P 2016, pp. 372\u2013387. IEEE (2016)","DOI":"10.1109\/EuroSP.2016.36"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Parkhi, O.M., Vedaldi, A., Zisserman, A.: Deep face recognition (2015)","DOI":"10.5244\/C.29.41"},{"key":"9_CR26","unstructured":"Pham, L.H., Li, J., Sun, J.: Socrates: Towards a unified platform for neural network verification. arXiv preprint arXiv:2007.11206 (2020)"},{"key":"9_CR27","unstructured":"Pham, L.H., Sun, J.: Source and Benchmark (2022). https:\/\/doi.org\/10.6084\/m9.figshare.19719742"},{"key":"9_CR28","unstructured":"Shafahi, A., Huang, W.R., Najibi, M., Suciu, O., Studer, C., Dumitras, T., Goldstein, T.: Poison frogs! targeted clean-label poisoning attacks on neural networks. arXiv preprint arXiv:1804.00792 (2018)"},{"key":"9_CR29","unstructured":"Singh, G., Ganvir, R., P\u00fcschel, M., Vechev, M.: Beyond the single neuron convex barrier for neural network certification. In: NeurIPS 2019, pp. 15098\u201315109 (2019)"},{"key":"9_CR30","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.: Fast and effective robustness certification. In: NeurIPS 2018, pp. 10802\u201310813 (2018)"},{"key":"9_CR31","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: Boosting robustness certification of neural networks. In: International Conference on Learning Representations (2018)"},{"key":"9_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3290354","volume":"3","author":"G Singh","year":"2019","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages 3, 1\u201330 (2019)","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"9_CR33","unstructured":"Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013)"},{"key":"9_CR34","unstructured":"Tjeng, V., Xiao, K., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356 (2017)"},{"key":"9_CR35","unstructured":"Turner, A., Tsipras, D., Madry, A.: Clean-label backdoor attacks (2018)"},{"key":"9_CR36","doi-asserted-by":"publisher","unstructured":"Virtanen, P., et al.: SciPy 1.0 Contributors: SciPy 1.0: Fundamental Algorithms for Scientific Computing in Python. Nature Methods 17, 261\u2013272 (2020). https:\/\/doi.org\/10.1038\/s41592-019-0686-2","DOI":"10.1038\/s41592-019-0686-2"},{"key":"9_CR37","unstructured":"Wang, B., Cao, X., Gong, N.Z., et al.: On certifying robustness against backdoor attacks via randomized smoothing. arXiv preprint arXiv:2002.11750 (2020)"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Wang, B., Yao, Y., Shan, S., Li, H., Viswanath, B., Zheng, H., Zhao, B.Y.: Neural cleanse: Identifying and mitigating backdoor attacks in neural networks. In: S &P 2019, pp. 707\u2013723. IEEE (2019)","DOI":"10.1109\/SP.2019.00031"},{"key":"9_CR39","doi-asserted-by":"crossref","unstructured":"Wang, J., Dong, G., Sun, J., Wang, X., Zhang, P.: Adversarial sample detection for deep neural network through model mutation testing. In: ICSE 2019, pp. 1245\u20131256. IEEE\/ACM (2019)","DOI":"10.1109\/ICSE.2019.00126"},{"key":"9_CR40","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. In: NeurIPS 2018, pp. 6367\u20136377 (2018)"},{"key":"9_CR41","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: 27th USENIX Security Symposium (USENIX Security 18), pp. 1599\u20131614 (2018)"},{"key":"9_CR42","doi-asserted-by":"crossref","unstructured":"Zhang, P., et al.: White-box fairness testing through adversarial sampling. In: ICSE 2020, pp. 949\u2013960. IEEE\/ACM (2020)","DOI":"10.1145\/3377811.3380331"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13185-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,3]],"date-time":"2022-11-03T17:13:17Z","timestamp":1667495597000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13185-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131844","9783031131851"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13185-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"7 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}