{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T03:19:51Z","timestamp":1783567191399,"version":"3.55.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2023,1,31]],"date-time":"2023-01-31T00:00:00Z","timestamp":1675123200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"IHUB NTIHAC Foundation\u2013IIT Kanpur and Robert Bosch Engineering and Business Solutions Private Limited"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2023,1,31]]},"abstract":"<jats:p>Modern vehicles contain a multitude of electronic control units that implement software features controlling most of the operational, entertainment, connectivity, and safety aspects of the vehicle. However, with security requirements often being an afterthought in automotive software development, incorporation of such software features with intra- and inter-vehicular connectivity requirements often opens up new attack surfaces. Demonstrations of such security vulnerabilities in past reports and literature bring in the necessity to formally analyze how secure automotive control systems really are against adversarial attacks. Modern vehicles often incorporate onboard monitoring systems that test the sanctity of data samples communicated among controllers and detect possible attack\/noise insertion scenarios. The performance of such monitors against security threats also needs to be verified.<\/jats:p>\n          <jats:p>\n            In this work, we outline a rigorous methodology for estimating the vulnerability of automotive CPSs. We provide a computer-aided design framework that considers the model-based representation of safety-critical automotive controllers and monitoring systems working in a closed loop with vehicle dynamics and verifies their safety and robustness w.r.t.\n            <jats:italic>false data injection<\/jats:italic>\n            attacks. Symbolically exploring all possible combinations of attack points of the input automotive CPS, the proposed framework tries to find out which sensor and\/or actuation signal is vulnerable by generating\n            <jats:italic>stealthy and successful<\/jats:italic>\n            attacks using a formal method-based counter-example guided abstract refinement process. We also validate the efficacy of the proposed framework using a case study performed in an industry-scale simulator.\n          <\/jats:p>","DOI":"10.1145\/3571287","type":"journal-article","created":{"date-parts":[[2022,11,18]],"date-time":"2022-11-18T12:04:38Z","timestamp":1668773078000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["CAD Support for Security and Robustness Analysis of Safety-critical Automotive Software"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9033-3295","authenticated-orcid":false,"given":"Ipsita","family":"Koley","sequence":"first","affiliation":[{"name":"Indian Institute of Technology Kharagpur,, Kharagpur, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9329-6389","authenticated-orcid":false,"given":"Soumyajit","family":"Dey","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Kharagpur,, Kharagpur, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6499-8346","authenticated-orcid":false,"given":"Debdeep","family":"Mukhopadhyay","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Kharagpur,, Kharagpur, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3947-0443","authenticated-orcid":false,"given":"Sachin","family":"Singh","sequence":"additional","affiliation":[{"name":"Robert Bosch Engineering and Business Solutions Private Limited, Bangalore, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4714-9537","authenticated-orcid":false,"given":"Lavanya","family":"Lokesh","sequence":"additional","affiliation":[{"name":"Robert Bosch Engineering and Business Solutions Private Limited, Bangalore, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9088-5583","authenticated-orcid":false,"given":"Shantaram Vishwanath","family":"Ghotgalkar","sequence":"additional","affiliation":[{"name":"Robert Bosch Engineering and Business Solutions Private Limited, Bangalore, India"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,2,20]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1145\/3411498.3419966","volume-title":"Proceedings of the Joint Workshop on CPS&IoT Security and Privacy","author":"Adhikary Sunandan","year":"2020","unstructured":"Sunandan Adhikary, Ipsita Koley, Saurav Kumar Ghosh, Sumana Ghosh, Soumyajit Dey, and Debdeep Mukhopadhyay. 2020. Skip to secure: Securing cyber-physical control loops with intentionally skipped executions. In Proceedings of the Joint Workshop on CPS&IoT Security and Privacy. 81\u201386."},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/TVT.2004.838829"},{"key":"e_1_3_3_4_2","doi-asserted-by":"crossref","unstructured":"M. K. Aripin Yahaya Md Sam Kumeresan A. Danapalasingam Kemao Peng N. Hamzah and M. F. Ismail. 2014. A review of active yaw control system for vehicle handling and stability enhancement. International Journal of Vehicular Technology 2014 (2014) 1\u201315.","DOI":"10.1155\/2014\/437515"},{"key":"e_1_3_3_5_2","volume-title":"Computer-controlled Systems: Theory and Design","author":"\u00c5str\u00f6m Karl J.","year":"2013","unstructured":"Karl J. \u00c5str\u00f6m et\u00a0al. 2013. Computer-controlled Systems: Theory and Design. Courier Corporation."},{"key":"e_1_3_3_6_2","first-page":"173","volume-title":"Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control","author":"Bak Stanley","year":"2017","unstructured":"Stanley Bak and Parasara Sridhar Duggirala. 2017. Hylaa: A tool for computing simulation-equivalent reachability for linear systems. In Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control. 173\u2013178."},{"key":"e_1_3_3_7_2","first-page":"148","volume-title":"International Summer School on Engineering Trustworthy Software Systems","author":"Bj\u00f8rner Nikolaj","year":"2018","unstructured":"Nikolaj Bj\u00f8rner, Leonardo de Moura, Lev Nachmanson, and Christoph M. Wintersteiger. 2018. Programming Z3. In International Summer School on Engineering Trustworthy Software Systems. Springer, 148\u2013201."},{"key":"e_1_3_3_8_2","first-page":"447","volume-title":"Proceedings of the USENIX Security Symposium","volume":"4","author":"Checkoway Stephen","year":"2011","unstructured":"Stephen Checkoway, Damon McCoy, Brian Kantor, Danny Anderson, Hovav Shacham, Stefan Savage, Karl Koscher, Alexei Czeskis, Franziska Roesner, Tadayoshi Kohno, et\u00a0al. 2011. Comprehensive experimental analyses of automotive attack surfaces. In Proceedings of the USENIX Security Symposium, Vol. 4. 447\u2013462."},{"key":"e_1_3_3_9_2","first-page":"1044","volume-title":"Proceedings of the ACM SIGSAC Conference on Computer and Communications Security","author":"Cho Kyong-Tak","year":"2016","unstructured":"Kyong-Tak Cho and Kang G. Shin. 2016. Error handling of in-vehicle networks makes them vulnerable. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security. 1044\u20131055."},{"key":"e_1_3_3_10_2","first-page":"52","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Cimatti Alessandro","year":"2015","unstructured":"Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. 2015. HyComp: An SMT-based model checker for hybrid systems. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 52\u201367."},{"key":"e_1_3_3_11_2","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Proceedings of the International Conference on Computer Aided Verification","author":"Clarke Edmund","year":"2000","unstructured":"Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-guided abstraction refinement. In Proceedings of the International Conference on Computer Aided Verification. Springer, 154\u2013169."},{"key":"e_1_3_3_12_2","first-page":"1","volume-title":"Proceedings of the IEEE Vehicular Networking Conference (VNC\u201916)","author":"Santos Eduardo dos","year":"2016","unstructured":"Eduardo dos Santos, Dominik Schoop, and Andrew Simpson. 2016. Formal models for automotive systems and vehicular networks: Benefits and challenges. In Proceedings of the IEEE Vehicular Networking Conference (VNC\u201916). IEEE, 1\u20138."},{"key":"e_1_3_3_13_2","unstructured":"Gregory Ewing. 2010. Reverse-Engineering a CRC Algorithm. Retrieved from https:\/\/www.cosc.canterbury.ac.nz\/greg.ewing\/essays\/CRC-Reverse-Engineering.html."},{"key":"e_1_3_3_14_2","first-page":"347","volume-title":"Proceedings of the International Conference on Computer Aided Verification","author":"Fan Chuchu","year":"2018","unstructured":"Chuchu Fan, Umang Mathur, Sayan Mitra, and Mahesh Viswanathan. 2018. Controller synthesis made real: Reach-avoid specifications and linear dynamics. In Proceedings of the International Conference on Computer Aided Verification. Springer, 347\u2013366."},{"key":"e_1_3_3_15_2","volume-title":"Proceedings of the Network and Distributed System Security Symposium (NDSS\u201911)","author":"Francillon Aur\u00e9lien","year":"2011","unstructured":"Aur\u00e9lien Francillon, Boris Danev, and Srdjan Capkun. 2011. Relay attacks on passive keyless entry and start systems in modern cars. In Proceedings of the Network and Distributed System Security Symposium (NDSS\u201911)."},{"key":"e_1_3_3_16_2","first-page":"90","volume-title":"Proceedings of the 49th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W\u201919)","author":"Heneghan John","year":"2019","unstructured":"John Heneghan, Siraj Ahmed Shaikh, Jeremy Bryans, Madeline Cheah, and Paul Wooderson. 2019. Enabling security checking of automotive ECUs with formal CSP models. In Proceedings of the 49th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W\u201919). IEEE, 90\u201397."},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.5555\/827267.828918"},{"key":"e_1_3_3_18_2","unstructured":"Steve Corrigan. 2002. Introduction to the controller area network (CAN). Appl. Rep. SLOA101 (2002) 1\u201317."},{"key":"e_1_3_3_19_2","volume-title":"Model-based Security Testing in Automotive Industry","author":"Kastebo Martin","year":"2017","unstructured":"Martin Kastebo and Victor Nordh. 2017. Model-based Security Testing in Automotive Industry. Master\u2019s thesis."},{"key":"e_1_3_3_20_2","first-page":"47","volume-title":"Proceedings of the International Workshop on Formal Methods for Industrial Critical Systems","author":"Kim Jin Hyun","year":"2015","unstructured":"Jin Hyun Kim, Kim G. Larsen, Brian Nielsen, Marius Miku\u010dionis, and Petur Olsen. 2015. Formal analysis and testing of real-time automotive systems using UPPAAL tools. In Proceedings of the International Workshop on Formal Methods for Industrial Critical Systems. Springer, 47\u201361."},{"key":"e_1_3_3_21_2","first-page":"314","volume-title":"Proceedings of the Design, Automation & Test in Europe Conference & Exhibition (DATE\u201920)","author":"Koley Ipsita","year":"2020","unstructured":"Ipsita Koley, Saurav Kumar Ghosh, Soumyajit Dey, Debdeep Mukhopadhyay, Amogh Kashyap K. N., Sachin Kumar Singh, Lavanya Lokesh, Jithin Nalu Purakkal, and Nishant Sinha. 2020. Formal synthesis of monitoring and detection systems for secure CPS implementations. In Proceedings of the Design, Automation & Test in Europe Conference & Exhibition (DATE\u201920). IEEE, 314\u2013317."},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.34"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3126518"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3380866"},{"key":"e_1_3_3_26_2","first-page":"207","volume-title":"Proceedings of the IEEE International Workshop on Factory Communication Systems","author":"Makowitz Rainer","year":"2006","unstructured":"Rainer Makowitz and Christopher Temple. 2006. FlexRay-a communication network for automotive control systems. In Proceedings of the IEEE International Workshop on Factory Communication Systems. IEEE, 207\u2013212."},{"key":"e_1_3_3_27_2","volume-title":"Proceedings of the 10th USENIX Workshop on Offensive Technologies (WOOT\u201916)","author":"Mazloom Sahar","year":"2016","unstructured":"Sahar Mazloom, Mohammad Rezaeirad, Aaron Hunter, and Damon McCoy. 2016. A security analysis of an in-vehicle infotainment and app platform. In Proceedings of the 10th USENIX Workshop on Offensive Technologies (WOOT\u201916)."},{"key":"e_1_3_3_28_2","first-page":"94","article-title":"A survey of remote automotive attack surfaces","author":"Miller Charlie","year":"2014","unstructured":"Charlie Miller and Chris Valasek. 2014. A survey of remote automotive attack surfaces. Black Hat USA (2014), 94.","journal-title":"Black Hat USA"},{"key":"e_1_3_3_29_2","first-page":"91","article-title":"Remote exploitation of an unaltered passenger vehicle","author":"Miller Charlie","year":"2015","unstructured":"Charlie Miller and Chris Valasek. 2015. Remote exploitation of an unaltered passenger vehicle. Black Hat USA (2015), 91.","journal-title":"Black Hat USA"},{"key":"e_1_3_3_30_2","first-page":"1","volume-title":"Preprints of the 1st Workshop on Secure Control Systems","author":"Mo Yilin","year":"2010","unstructured":"Yilin Mo and Bruno Sinopoli. 2010. False data injection attacks in control systems. In Preprints of the 1st Workshop on Secure Control Systems. 1\u20136."},{"key":"e_1_3_3_31_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-73512-2","volume-title":"Guide to Automotive Connectivity and Cybersecurity","author":"M\u00f6ller Dietmar P. F.","year":"2019","unstructured":"Dietmar P. F. M\u00f6ller and Roland E. Haas. 2019. Guide to Automotive Connectivity and Cybersecurity. Springer."},{"key":"e_1_3_3_32_2","doi-asserted-by":"crossref","unstructured":"Arslan Munir and Farinaz Koushanfar. 2018. Design and analysis of secure and dependable automotive cps: A steer-by-wire case study. IEEE Trans. Depend. Secure Comput. 17 4 (2018) 813\u2013827.","DOI":"10.1109\/TDSC.2018.2846741"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3098954.3103174"},{"issue":"29","key":"e_1_3_3_34_2","first-page":"1","article-title":"Correlation of objective and subjective evaluation of vehicle handling by neural networks","volume":"8","author":"Pelikan Jan","year":"2011","unstructured":"Jan Pelikan, Pavel Steinbauer, Michael Valasek, and Jaroslav Ulehla. 2011. Correlation of objective and subjective evaluation of vehicle handling by neural networks. Bull. Appl. Mech. 8, 29 (2011), 1\u20134.","journal-title":"Bull. Appl. Mech."},{"key":"e_1_3_3_35_2","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Proceedings of the International Joint Conference on Automated Reasoning","author":"Platzer Andr\u00e9","year":"2008","unstructured":"Andr\u00e9 Platzer and Jan-David Quesel. 2008. KeYmaera: A hybrid theorem prover for hybrid systems (system description). In Proceedings of the International Joint Conference on Automated Reasoning. Springer, 171\u2013178."},{"key":"e_1_3_3_36_2","volume-title":"Vehicle Dynamics and Control","author":"Rajamani Rajesh","year":"2011","unstructured":"Rajesh Rajamani. 2011. Vehicle Dynamics and Control. Springer Science & Business Media."},{"key":"e_1_3_3_37_2","volume-title":"Automotive Mechatronics","author":"Reif Konrad","year":"2014","unstructured":"Konrad Reif. 2014. Automotive Mechatronics. Springer."},{"key":"e_1_3_3_38_2","volume-title":"Proceedings of the USENIX Security Symposium","volume":"10","author":"Rouf Ishtiaq","year":"2010","unstructured":"Ishtiaq Rouf, Robert D. Miller, Hossen A. Mustafa, Travis Taylor, Sangho Oh, Wenyuan Xu, Marco Gruteser, Wade Trappe, and Ivan Seskar. 2010. Security and privacy vulnerabilities of in-car wireless networks: A tire pressure monitoring system case study. In Proceedings of the USENIX Security Symposium, Vol. 10."},{"key":"e_1_3_3_39_2","first-page":"3382","volume-title":"Proceedings of the IEEE 58th Vehicular Technology Conference (VTC\u201903)","volume":"5","author":"Ruff Matthew","year":"2003","unstructured":"Matthew Ruff. 2003. Evolution of local interconnect network (LIN) solutions. In Proceedings of the IEEE 58th Vehicular Technology Conference (VTC\u201903), Vol. 5. IEEE, 3382\u20133389."},{"key":"e_1_3_3_40_2","first-page":"458","volume-title":"Proceedings of the Design, Automation & Test in Europe Conference & Exhibition (DATE\u201913)","author":"Sagstetter Florian","year":"2013","unstructured":"Florian Sagstetter, Martin Lukasiewycz, Sebastian Steinhorst, Marko Wolf, Alexandre Bouard, William R. Harris, Somesh Jha, Thomas Peyrin, Axel Poschmann, and Samarjit Chakraborty. 2013. Security challenges in automotive hardware\/software architecture design. In Proceedings of the Design, Automation & Test in Europe Conference & Exhibition (DATE\u201913). IEEE, 458\u2013463."},{"issue":"4","key":"e_1_3_3_41_2","doi-asserted-by":"crossref","first-page":"954","DOI":"10.1109\/TIFS.2018.2868245","article-title":"Automatic characterization of exploitable faults: A machine learning approach","volume":"14","author":"Saha Sayandeep","year":"2018","unstructured":"Sayandeep Saha, Dirmanto Jap, Sikhar Patranabis, Debdeep Mukhopadhyay, Shivam Bhasin, and Pallab Dasgupta. 2018. Automatic characterization of exploitable faults: A machine learning approach. IEEE Trans. Inf. Forens. Secur. 14, 4 (2018), 954\u2013968.","journal-title":"IEEE Trans. Inf. Forens. Secur."},{"key":"e_1_3_3_42_2","article-title":"A formal model to facilitate security testing in modern automotive systems","author":"Santos Eduardo dos","year":"2018","unstructured":"Eduardo dos Santos, Andrew Simpson, and Dominik Schoop. 2018. A formal model to facilitate security testing in modern automotive systems. arXiv:1805.05520. Retrieved from https:\/\/arxiv.org\/abs\/1805.05520.","journal-title":"arXiv:1805.05520"},{"issue":"1","key":"e_1_3_3_43_2","article-title":"New elements in vehicle communication \u201cmedia oriented systems transport\u201d protocol","volume":"12","author":"Sumorek Andrzej","year":"2012","unstructured":"Andrzej Sumorek and Marcin Buczaj. 2012. New elements in vehicle communication \u201cmedia oriented systems transport\u201d protocol. Teka Komisji Motoryz. Energ. Rolnict. 12, 1 (2012).","journal-title":"Teka Komisji Motoryz. Energ. Rolnict."},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59897-6_2"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.conengprac.2005.10.005"}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571287","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571287","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:22Z","timestamp":1750183702000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571287"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,31]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,1,31]]}},"alternative-id":["10.1145\/3571287"],"URL":"https:\/\/doi.org\/10.1145\/3571287","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"value":"2378-962X","type":"print"},{"value":"2378-9638","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,31]]},"assertion":[{"value":"2021-02-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-09-15","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-02-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}