{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T11:37:45Z","timestamp":1759837065341,"version":"3.40.5"},"reference-count":43,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"3","license":[{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["U21B2019","U2003206"],"award-info":[{"award-number":["U21B2019","U2003206"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Dependable and Secure Comput."],"published-print":{"date-parts":[[2025,5]]},"DOI":"10.1109\/tdsc.2024.3481433","type":"journal-article","created":{"date-parts":[[2024,10,16]],"date-time":"2024-10-16T18:10:07Z","timestamp":1729102207000},"page":"2211-2226","source":"Crossref","is-referenced-by-count":4,"title":["Binary-Level Formal Verification Based Automatic Security Ensurement for PLC in Industrial IoT"],"prefix":"10.1109","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-2041-4013","authenticated-orcid":false,"given":"Xuankai","family":"Zhang","sequence":"first","affiliation":[{"name":"School of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6831-3973","authenticated-orcid":false,"given":"Jianhua","family":"Li","sequence":"additional","affiliation":[{"name":"School of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2483-6980","authenticated-orcid":false,"given":"Jun","family":"Wu","sequence":"additional","affiliation":[{"name":"School of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8107-5909","authenticated-orcid":false,"given":"Guoxing","family":"Chen","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, Shanghai Jiao Tong University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5445-0347","authenticated-orcid":false,"given":"Yan","family":"Meng","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, Shanghai Jiao Tong University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5079-4556","authenticated-orcid":false,"given":"Haojin","family":"Zhu","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, Shanghai Jiao Tong University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9886-1412","authenticated-orcid":false,"given":"Xiaosong","family":"Zhang","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, University of Electronic Science and Technology of China, Chengdu, China"}]}],"member":"263","reference":[{"article-title":"W32. Stuxnet dossier","year":"2011","author":"Falliere","key":"ref1"},{"author":"Hentunen","key":"ref2","article-title":"Havex hunts for ICS\/SCADA systems"},{"key":"ref3","first-page":"1","article-title":"Triton: The first ICS cyber attack on safety instrument systems","volume":"2018","author":"Di Pinto","year":"2018","journal-title":"Black Hat USA"},{"article-title":"Codesys device directory","year":"2023","author":"Group","key":"ref4"},{"year":"2023","key":"ref5","article-title":"Global PLC market share as of 2017, by manufacturer, 2017"},{"key":"ref6","first-page":"1","article-title":"Confirmation of a coordinated attack on the ukrainian power grid","volume":"207","author":"Assante","year":"2016","journal-title":"SANS Ind. Control Syst. Secur. Blog"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2018.06.336"},{"issue":"62","key":"ref8","first-page":"1","article-title":"German steel mill cyber attack","volume":"30","author":"Lee","year":"2014","journal-title":"Ind. Control Syst."},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2015.2489184"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.3311\/ppee.9743"},{"key":"ref11","first-page":"78","article-title":"Towards verified model transformations","volume-title":"Proc. 3rd Int. Workshop Model Develop. Validation Verification","author":"Giese"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9415-7"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00018-9_22"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2014.23043"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.5724"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2014.113"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.17"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/COMAPP.2018.8460287"},{"article-title":"PLC code vulnerabilities through SCADA systems","year":"2013","author":"Valentine","key":"ref19"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/SmartGridComm.2014.7007754"},{"article-title":"On dynamic malware payloads aimed at programmable logic controllers","volume-title":"Proc. 6th USENIX Conf. Hot Topics Secur.","author":"McLaughlin","key":"ref21"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14261-1_11"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23271"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43613-4_18"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_32"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2010.10"},{"author":"K\u00fchner","key":"ref27","article-title":"Dotnetsiemensplctoolboxlibrary"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382244"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-450010-5.50015-3"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/b105236"},{"article-title":"Report on the NSF workshop on formal methods for security","year":"2016","author":"Chong","key":"ref31"},{"key":"ref32","first-page":"21","article-title":"PLCverif re-engineered: An open platform for the formal analysis of PLC programs","volume-title":"Proc. 17th Int. Conf. Accel. Large Exp. Phys. Control Syst.","author":"Blanco Vi\u00f1uela"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/TPWRS.2016.2631891"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC.2013.85"},{"key":"ref35","first-page":"1","article-title":"PLC-blaster: A worm living solely in the PLC","author":"Spenneberg","year":"2016","journal-title":"Black Hat Asia"},{"key":"ref36","first-page":"22","article-title":"Internet-facing PLCs\u2013A new back orifice","author":"Klick","year":"2015","journal-title":"Blackhat USA"},{"issue":"2","key":"ref37","first-page":"723","article-title":"Exploiting siemens simatic S7 PLCs","volume":"16","author":"Beresford","year":"2011","journal-title":"Black Hat USA"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/PRDC.2017.34"},{"key":"ref39","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-08867-9","volume-title":"26th International Conference Computer Aided Verification","author":"Biere","year":"2014"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2015.23294"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2023.23131"},{"article-title":"ICSPatch: Automated vulnerability localization and non-intrusive hotpatching in industrial control systems using data dependence graphs","volume-title":"Proc. 32nd USENIX Secur. Symp.","author":"Rajput","key":"ref42"},{"key":"ref43","first-page":"2847","article-title":"ICSFuzz: Manipulating I\/Os and repurposing binary code to enable instrumented fuzzing in ICS control applications","volume-title":"Proc. 30th USENIX Secur. Symp.","author":"Tychalas"}],"container-title":["IEEE Transactions on Dependable and Secure Computing"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/8858\/10992672\/10720350.pdf?arnumber=10720350","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,15]],"date-time":"2025-05-15T19:37:17Z","timestamp":1747337837000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10720350\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5]]},"references-count":43,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.1109\/tdsc.2024.3481433","relation":{},"ISSN":["1545-5971","1941-0018","2160-9209"],"issn-type":[{"type":"print","value":"1545-5971"},{"type":"electronic","value":"1941-0018"},{"type":"electronic","value":"2160-9209"}],"subject":[],"published":{"date-parts":[[2025,5]]}}}