{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:59:29Z","timestamp":1740142769901,"version":"3.37.3"},"reference-count":60,"publisher":"Oxford University Press (OUP)","issue":"11","license":[{"start":{"date-parts":[[2022,10,1]],"date-time":"2022-10-01T00:00:00Z","timestamp":1664582400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"name":"National Key Research and Development","award":["2019YFA0706404"],"award-info":[{"award-number":["2019YFA0706404"]}]},{"DOI":"10.13039\/501100001809","name":"National Nature Science Foundation of China","doi-asserted-by":"publisher","award":["3420\/21","62161146001"],"award-info":[{"award-number":["3420\/21","62161146001"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Fundamental Research Funds for Central Universities"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,11,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>In the Internet of Things, smart devices are expected to correctly capture and process data from environments, regardless of perturbation and adversarial attacks. Therefore, it is important to guarantee the robustness of their intelligent components, e.g. neural networks, to protect the system from environment perturbation and adversarial attacks. In this paper, we propose a formal verification technique for rigorously proving the robustness of neural networks. Our approach leverages a tight liner approximation technique and constraint substitution, by which we transform the robustness verification problem into an efficiently solvable linear programming problem. Unlike existing approaches, our approach can automatically generate adversarial examples when a neural network fails to verify. Besides, it is general and applicable to more complex neural network architectures such as CNN, LeNet and ResNet. We implement the approach in a prototype tool called WiNR and evaluate it on extensive benchmarks, including Fashion MNIST, CIFAR10 and GTSRB. Experimental results show that WiNR can verify neural networks that contain over 10 000 neurons on one input image in a minute with a 6.28% probability of false positive on average.<\/jats:p>","DOI":"10.1093\/comjnl\/bxac094","type":"journal-article","created":{"date-parts":[[2022,10,3]],"date-time":"2022-10-03T11:25:39Z","timestamp":1664796339000},"page":"2894-2908","source":"Crossref","is-referenced-by-count":2,"title":["Efficient Robustness Verification of the Deep Neural Networks for Smart IoT Devices"],"prefix":"10.1093","volume":"65","author":[{"given":"Zhaodi","family":"Zhang","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing , East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jing","family":"Liu","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing , East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Min","family":"Zhang","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing , East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Haiying","family":"Sun","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing , East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2022,10,1]]},"reference":[{"key":"2022111713012741000_ref1","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1109\/JIOT.2015.2417684","article-title":"An IoT-aware architecture for smart healthcare systems","volume":"2","author":"Catarinucci","year":"2015","journal-title":"IEEE Internet Things J."},{"key":"2022111713012741000_ref2","doi-asserted-by":"crossref","first-page":"17:1","DOI":"10.1145\/3311956","article-title":"Music, search, and IoT: how people (really) use voice assistants","volume":"26","author":"Ammari","year":"2019","journal-title":"ACM Trans. Comput. Hum Interact."},{"key":"2022111713012741000_ref3","doi-asserted-by":"crossref","first-page":"10350","DOI":"10.3390\/s150510350","article-title":"WSN- and IOT-based smart homes and their extension to smart buildings","volume":"15","author":"Ghayvat","year":"2015","journal-title":"Sensors"},{"key":"2022111713012741000_ref4","doi-asserted-by":"crossref","DOI":"10.1016\/j.comnet.2022.108771","article-title":"State-of-the-art survey of artificial intelligent techniques for IoT security","volume":"206","author":"Ahanger","year":"2022","journal-title":"Comput. Netw."},{"key":"2022111713012741000_ref5","article-title":"TSMAE: a novel anomaly detection approach for Internet of Things time series data using memory-augmented autoencoder","volume":"10.1109","author":"Gao","year":"2022","journal-title":"IEEE Trans. Networ. Sci. Eng."},{"key":"2022111713012741000_ref6","first-page":"1106","volume-title":"Proceedings of Conference on Neural Information Processing Systems","author":"Krizhevsky","year":"2012"},{"key":"2022111713012741000_ref7","first-page":"273","volume-title":"Proceedings of Workshop on Automatic Speech Recognition and Understanding, Olomouc","author":"Graves","year":"2013"},{"key":"2022111713012741000_ref8","first-page":"6645","volume-title":"Proceedings of International Conference on Acoustics, Speech and Signal Processing","author":"Graves","year":"2013"},{"key":"2022111713012741000_ref9","first-page":"2261","volume-title":"Proceedings of Conference on Computer Vision and Pattern Recognition","author":"Huang","year":"2017"},{"key":"2022111713012741000_ref10","first-page":"4171","volume-title":"Proceedings of Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies","author":"Devlin","year":"2019"},{"key":"2022111713012741000_ref11","doi-asserted-by":"crossref","first-page":"2923","DOI":"10.1109\/COMST.2018.2844341","article-title":"Deep learning for IoT big data and streaming analytics: a survey","volume":"20","author":"Mohammadi","year":"2018","journal-title":"IEEE Commun. Surv. Tutor."},{"key":"2022111713012741000_ref12","doi-asserted-by":"crossref","first-page":"10:1","DOI":"10.1145\/3436751","article-title":"Malware classification based on multilayer perception and Word2Vec for IoT security","volume":"22","author":"Qiao","year":"2022","journal-title":"ACM Trans. Internet Technol."},{"key":"2022111713012741000_ref13","doi-asserted-by":"crossref","first-page":"122:1","DOI":"10.1145\/3417987","article-title":"Security and privacy in IoT using machine learning and blockchain: threats and countermeasures","volume":"53","author":"Waheed","year":"2021","journal-title":"ACM Comput Surv."},{"key":"2022111713012741000_ref14","article-title":"Deep neural network based anomaly detection in internet of things network traffic tracking for the applications of future smart cities","volume":"32","author":"Reddy","year":"2021","journal-title":"Trans. Emerg. Telecommun. Technol."},{"key":"2022111713012741000_ref15","doi-asserted-by":"crossref","DOI":"10.1016\/j.compeleceng.2021.107039","article-title":"Stacked recurrent neural network for botnet detection in smart homes","volume":"92","author":"Popoola","year":"2021","journal-title":"Comput. Electr. Eng."},{"key":"2022111713012741000_ref16","first-page":"427","volume-title":"Proceedings of Conference on Design Automation","author":"Clarke","year":"1995"},{"key":"2022111713012741000_ref17","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"Proceedings of International Conference on Computer Aided Verification","author":"Huang","year":"2017"},{"key":"2022111713012741000_ref18","first-page":"241","volume-title":"Proceedings of Conference on Computer Vision and Pattern Recognition","author":"Mohapatra","year":"2020"},{"key":"2022111713012741000_ref19","first-page":"10825","volume-title":"Proceedings of Conference on Neural Information Processing Systems","author":"Singh","year":"2018"},{"key":"2022111713012741000_ref20","first-page":"5037","volume-title":"Proceedings of Conference on Artificial Intelligence","author":"Lyu","year":"2020"},{"key":"2022111713012741000_ref21","doi-asserted-by":"crossref","DOI":"10.1016\/j.cosrev.2020.100270","article-title":"A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability","volume":"37","author":"Huang","year":"2020","journal-title":"Comput. Sci. Rev."},{"key":"2022111713012741000_ref22","article-title":"Explaining and harnessing adversarial examples","volume":"abs\/1412.6572","author":"Goodfellow","year":"2015","journal-title":"CoRR"},{"key":"2022111713012741000_ref23","article-title":"On evaluating adversarial robustness","author":"Carlini","year":"2019","journal-title":"CoRR"},{"key":"2022111713012741000_ref24","first-page":"125","volume-title":"Proceedings of Conference on Neural Information Processing Systems","author":"Ilyas","year":"2019"},{"key":"2022111713012741000_ref25","first-page":"1122","volume-title":"Proceedings of International Conference on Machine Learning","author":"Chen","year":"2019"},{"key":"2022111713012741000_ref26","first-page":"1829","volume-title":"Proceedings of Conference on Neural Information Processing Systems","author":"Zhang","year":"2019"},{"key":"2022111713012741000_ref27","first-page":"14521","volume-title":"Proceedings of Conference on Computer Vision and Pattern Recognition","author":"Zhang","year":"2020"},{"key":"2022111713012741000_ref28","article-title":"Using learning dynamics to explore the role of implicit regularization in adversarial examples","volume":"abs\/2006.11440","author":"Caro","year":"2020","journal-title":"CoRR"},{"key":"2022111713012741000_ref29","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/978-3-642-14295-6_24","volume-title":"Proceedings of International Conference on Computer Aided Verification","author":"Pulina","year":"2010"},{"key":"2022111713012741000_ref30","first-page":"11418","volume-title":"Proceedings of Conference on Computer Vision and Pattern Recognition","author":"Lin","year":"2019"},{"key":"2022111713012741000_ref31","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/978-3-319-77935-5_9","volume-title":"Proceedings of International Symposium on NASA Formal Methods","author":"Dutta","year":"2018"},{"key":"2022111713012741000_ref32","first-page":"6369","volume-title":"Proceedings of Conference on Neural Information Processing Systems","author":"Wang","year":"2018"},{"key":"2022111713012741000_ref33","first-page":"1599","volume-title":"Proceedings of USENIX Security Symposium","author":"Wang","year":"2018"},{"key":"2022111713012741000_ref34","doi-asserted-by":"crossref","first-page":"5777","DOI":"10.1109\/TNNLS.2018.2808470","article-title":"Output reachable set estimation and verification for multilayer neural networks","volume":"29","author":"Xiang","year":"2018","journal-title":"IEEE Trans. Neural Netw.Learn. Syst."},{"key":"2022111713012741000_ref35","first-page":"5276","volume-title":"Proceedings of International Conference on Machine Learning","author":"Weng","year":"2018"},{"key":"2022111713012741000_ref36","first-page":"4944","volume-title":"Proceedings of Conference on Neural Information Processing Systems","author":"Zhang","year":"2018"},{"key":"2022111713012741000_ref37","first-page":"5757","volume-title":"Proceedings of Conference on Artificial Intelligence","author":"Zhang","year":"2019"},{"key":"2022111713012741000_ref38","first-page":"3240","volume-title":"Proceedings of Conference on Artificial Intelligence","author":"Boopathy","year":"2019"},{"key":"2022111713012741000_ref39","first-page":"3","volume-title":"Proceedings of IEEE Symposium on Security and Privacy","author":"Gehr","year":"2018"},{"key":"2022111713012741000_ref40","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3290354","article-title":"An abstract domain for certifying neural networks","volume":"3","author":"Singh","year":"2019","journal-title":"Proc. ACM Program. Lang."},{"key":"2022111713012741000_ref41","article-title":"An approach to reachability analysis for feed-forward ReLU neural networks","author":"Lomuscio","year":"2017","journal-title":"CoRR"},{"key":"2022111713012741000_ref42","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/978-3-319-68167-2_18","volume-title":"Proceedings of International Symposium on Automated Technology for Verification and Analysis","author":"Cheng","year":"2017"},{"key":"2022111713012741000_ref43","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Proceedings of International Conference on Computer Aided Verification","author":"Katz","year":"2017"},{"key":"2022111713012741000_ref44","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","volume-title":"Proceedings of International Conference on Computer Aided Verification","author":"Katz","year":"2019"},{"key":"2022111713012741000_ref45","first-page":"11674","volume-title":"Proceedings of Conference on Artificial Intelligence","author":"Wu","year":"2021"},{"key":"2022111713012741000_ref46","doi-asserted-by":"crossref","first-page":"2278","DOI":"10.1109\/5.726791","article-title":"Gradient-based learning applied to document recognition","volume":"86","author":"LeCun","year":"1998","journal-title":"Proc. IEEE"},{"key":"2022111713012741000_ref47","first-page":"770","volume-title":"Proceedings of Conference on Computer Vision and Pattern Recognition","author":"He","year":"2016"},{"key":"2022111713012741000_ref48","article-title":"Fashion-MNIST: a novel image dataset for benchmarking machine learning algorithms","author":"Xiao","year":"2017","journal-title":"CoRR"},{"key":"2022111713012741000_ref49","article-title":"Learning multiple layers of features from tiny images","volume-title":"Master\u2019s thesis, Department of Computer Science, University of Toronto","author":"","year":"2009"},{"key":"2022111713012741000_ref50","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/j.neunet.2012.02.016","article-title":"Man vs. computer: benchmarking machine learning algorithms for traffic sign recognition","volume":"32","author":"Stallkamp","year":"2012","journal-title":"Neural Netw."},{"key":"2022111713012741000_ref51","article-title":"Evaluating robustness of neural networks with mixed integer programming","author":"Tjeng","year":"2017","journal-title":"CoRR"},{"key":"2022111713012741000_ref52","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1038\/d41586-019-03013-5","article-title":"Why deep-learning AIs are so easy to fool","volume":"574","author":"Heaven","year":"2019","journal-title":"Nature"},{"key":"2022111713012741000_ref53","first-page":"2574","volume-title":"Proceedings of Conference on Computer Vision and Pattern Recognition","author":"Moosavi-Dezfooli","year":"2016"},{"key":"2022111713012741000_ref54","first-page":"427","volume-title":"Proceedings of Conference on Computer Vision and Pattern Recognition","author":"Nguyen","year":"2015"},{"key":"2022111713012741000_ref55","first-page":"3291","volume-title":"Proceedings of Conference on Artificial Intelligence","author":"Botoeva","year":"2020"},{"author":"Gurobi Optimization, LLC","key":"2022111713012741000_ref56","article-title":"Gurobi Optimizer Reference Manual"},{"key":"2022111713012741000_ref57","first-page":"550","volume-title":"Proceedings of Conference on Uncertainty in Artificial Intelligence","author":"Dvijotham","year":"2018"},{"key":"2022111713012741000_ref58","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/7.4.308","article-title":"A simplex method for function minimization","volume":"7","author":"Nelder","year":"1965","journal-title":"Comput J."},{"key":"2022111713012741000_ref59","article-title":"A mutually supervised graph attention network for few-shot segmentation: the perspective of fully utilizing limited samples","volume":"10.1109","author":"Gao","year":"2022","journal-title":"IEEE Trans. Neural Netw. Learn. Syst."},{"key":"2022111713012741000_ref60","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1109\/TCSS.2021.3102591","article-title":"The deep features and attention mechanism-based method to dish healthcare under social IOT systems: an empirical study with a hand-deep local-global net","volume":"9","author":"Gao","year":"2022","journal-title":"IEEE Trans.Comput. Soc. Syst."}],"container-title":["The Computer Journal"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/comjnl\/article-pdf\/65\/11\/2894\/47089015\/bxac094.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/comjnl\/article-pdf\/65\/11\/2894\/47089015\/bxac094.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,17]],"date-time":"2022-11-17T13:02:41Z","timestamp":1668690161000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/comjnl\/article\/65\/11\/2894\/6741092"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,1]]},"references-count":60,"journal-issue":{"issue":"11","published-online":{"date-parts":[[2022,10,1]]},"published-print":{"date-parts":[[2022,11,11]]}},"URL":"https:\/\/doi.org\/10.1093\/comjnl\/bxac094","relation":{},"ISSN":["0010-4620","1460-2067"],"issn-type":[{"type":"print","value":"0010-4620"},{"type":"electronic","value":"1460-2067"}],"subject":[],"published-other":{"date-parts":[[2022,11]]},"published":{"date-parts":[[2022,10,1]]}}}