{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T13:37:53Z","timestamp":1771940273330,"version":"3.50.1"},"publisher-location":"Singapore","reference-count":29,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819606160","type":"print"},{"value":"9789819606177","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-981-96-0617-7_13","type":"book-chapter","created":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T15:02:17Z","timestamp":1732806137000},"page":"216-236","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Differential Property Monitoring for\u00a0Backdoor Detection"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-5433-5292","authenticated-orcid":false,"given":"Otto","family":"Brechelmacher","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5468-0396","authenticated-orcid":false,"given":"Dejan","family":"Ni\u010dkovi\u0107","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7712-0006","authenticated-orcid":false,"given":"Tobias","family":"Nie\u00dfen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6828-659X","authenticated-orcid":false,"given":"Sarah","family":"Sallinger","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0143-632X","authenticated-orcid":false,"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,29]]},"reference":[{"key":"13_CR1","unstructured":"Aceto, L., Achilleos, A., Anastasiadi, E., Francalanza, A., Gorla, D., Wagemaker, J.: Centralized vs decentralized monitors for hyperproperties (2024). https:\/\/arxiv.org\/abs\/2405.12882"},{"issue":"12","key":"13_CR2","doi-asserted-by":"publisher","first-page":"1491","DOI":"10.1109\/TSE.1985.231893","volume":"11","author":"A Avizienis","year":"1985","unstructured":"Avizienis, A.: The n-version approach to fault-tolerant software. IEEE Trans. Softw. Eng. 11(12), 1491\u20131501 (1985). https:\/\/doi.org\/10.1109\/TSE.1985.231893","journal-title":"IEEE Trans. Softw. Eng."},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-642-32759-9_9","volume-title":"FM 2012: Formal Methods","author":"H Barringer","year":"2012","unstructured":"Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.: Quantified event automata: towards expressive and efficient runtime monitors. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 68\u201384. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_9"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Basin, D., Klaedtke, F., M\u00fcller, S.: Monitoring security policies with metric first-order temporal logic. In: ACM Symposium on Access Control Models and Technologies (SACMAT). ACM (2010)","DOI":"10.1145\/1809842.1809849"},{"issue":"2","key":"13_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2699444","volume":"62","author":"DA Basin","year":"2015","unstructured":"Basin, D.A., Klaedtke, F., M\u00fcller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 1\u201345 (2015). https:\/\/doi.org\/10.1145\/2699444","journal-title":"J. ACM"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Basin, D.A., Klaedtke, F., Zalinescu, E.: The MonPoly monitoring tool. In: Reger, G., Havelund, K. (eds.) Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES). Kalpa Publications in Computing, vol.\u00a03. EasyChair (2017). https:\/\/doi.org\/10.29007\/89HS","DOI":"10.29007\/89HS"},{"issue":"3","key":"13_CR7","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/J.COSE.2009.09.003","volume":"29","author":"A Bauer","year":"2010","unstructured":"Bauer, A., J\u00fcrjens, J.: Runtime verification of cryptographic protocols. Comput. Secur. 29(3), 315\u2013330 (2010). https:\/\/doi.org\/10.1016\/J.COSE.2009.09.003","journal-title":"Comput. Secur."},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-28891-3_18","volume-title":"NASA Formal Methods","author":"A Bauer","year":"2012","unstructured":"Bauer, A., K\u00fcster, J.-C., Vegliach, G.: Runtime verification meets android security. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 174\u2013180. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_18"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Henzinger, T.A.: Monitoring hyperproperties with prefix transducers. In: Runtime Verification (RV), vol. 14245. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-44267-4_9","DOI":"10.1007\/978-3-031-44267-4_9"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Coppens, B., De\u00a0Sutter, B., Volckaert, S.: Multi-variant execution environments. In: The Continuing Arms Race, vol.\u00a018. ACM\/Morgan & Claypool (2018)","DOI":"10.1145\/3129743.3129752"},{"issue":"26","key":"13_CR11","doi-asserted-by":"publisher","first-page":"251","DOI":"10.3406\/phlou.1952.4394","volume":"50","author":"HB Curry","year":"1952","unstructured":"Curry, H.B.: On the definition of substitution, replacement and allied notions in a abstract formal system. Revue Philosophique De Louvain 50(26), 251\u2013269 (1952). https:\/\/doi.org\/10.3406\/phlou.1952.4394","journal-title":"Revue Philosophique De Louvain"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Evans, R.B., Savoia, A.: Differential testing: a new approach to change detection. In: Foundations of Software Engineering (FSE). ACM (2007)","DOI":"10.1145\/1295014.1295038"},{"issue":"3","key":"13_CR13","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/S10703-019-00334-Z","volume":"54","author":"B Finkbeiner","year":"2019","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties. Formal Methods Syst. Des. (FMSD) 54(3), 336\u2013363 (2019). https:\/\/doi.org\/10.1007\/S10703-019-00334-Z","journal-title":"Formal Methods Syst. Des. (FMSD)"},{"key":"13_CR14","unstructured":"Goodin, D.: 4-year campaign backdoored iphones using possibly the most advanced exploit ever (2023). https:\/\/arstechnica.com\/security\/2023\/12\/exploit-used-in-mass-iphone-infection-campaign-targeted-secret-hardware-feature\/"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Groce, A., Holzmann, G., Joshi, R.: Randomized differential testing as a prelude to formal verification. In: International Conference on Software Engineering (ICSE). IEEE (2007)","DOI":"10.1109\/ICSE.2007.68"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-030-17465-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Hahn","year":"2019","unstructured":"Hahn, C., Stenger, M., Tentrup, L.: Constraint-based monitoring of hyperproperties. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 115\u2013131. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_7"},{"issue":"1","key":"13_CR17","first-page":"1","volume":"56","author":"K Havelund","year":"2020","unstructured":"Havelund, K., Peled, D., Ulus, D.: First-order temporal logic monitoring with BDDs. Formal Methods Syst. Des. (FMSD) 56(1), 1\u201321 (2020)","journal-title":"Formal Methods Syst. Des. (FMSD)"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-319-23820-3_9","volume-title":"Runtime Verification","author":"J-C K\u00fcster","year":"2015","unstructured":"K\u00fcster, J.-C., Bauer, A.: Monitoring real android malware. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 136\u2013152. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_9"},{"key":"13_CR19","unstructured":"Lins, M., Mayrhofer, R., Roland, M., Hofer, D., Schwaighofer, M.: On the critical path to implant backdoors and the effectiveness of potential mitigation techniques: early learnings from $$\\texttt{xz}$$ (2024). https:\/\/arxiv.org\/abs\/2404.08987"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-030-88494-9_12","volume-title":"Runtime Verification","author":"F Muehlboeck","year":"2021","unstructured":"Muehlboeck, F., Henzinger, T.A.: Differential monitoring. In: Feng, L., Fisman, D. (eds.) RV 2021. LNCS, vol. 12974, pp. 231\u2013243. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88494-9_12"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Petersen, H.E., Turn, R.: System implications of information privacy. In: Joint Computer Conference of the American Federation of Information Processing Societies (AFIPS). AFIPS Conference Proceedings, vol.\u00a030. ACM (1967). https:\/\/doi.org\/10.1145\/1465482.1465526","DOI":"10.1145\/1465482.1465526"},{"key":"13_CR22","unstructured":"Roose, K.: Spotting a bug that may have been meant to cripple the internet. The New York Times p. 1 of section A of the New York edition (2024). https:\/\/www.nytimes.com\/2024\/04\/03\/technology\/prevent-cyberattack-linux.html"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Sabt, M., Achemlal, M., Bouabdallah, A.: Trusted execution environment: what it is, and what it is not. In: TrustCom\/BigDataSE\/ISPA. IEEE (2015). https:\/\/doi.org\/10.1109\/TRUSTCOM.2015.357","DOI":"10.1109\/TRUSTCOM.2015.357"},{"key":"13_CR24","unstructured":"Schneier, B.: Cisco can\u2019t stop using hard-coded passwords (2023). https:\/\/www.schneier.com\/blog\/archives\/2023\/10\/cisco-cant-stop-using-hard-coded-passwords.html. Accessed 29 Apr 2024"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Schuster, F., Holz, T.: Towards reducing the attack surface of software backdoors. In: Computer and Communications Security (CCS). ACM (2013)","DOI":"10.1145\/2508859.2516716"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Shoshitaishvili, Y., Wang, R., Hauser, C., Kruegel, C., Vigna, G.: Firmalice - automatic detection of authentication bypass vulnerabilities in binary firmware. In: Network and Distributed System Security Symposium (NDSS). Internet Society (2015)","DOI":"10.14722\/ndss.2015.23294"},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Signoles, J., Kosmatov, N., Vorobyov, K.: E-ACSL, a runtime verification tool for safety and security of C programs (tool paper). In: Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES). Kalpa Publications in Computing, vol.\u00a03. EasyChair (2017). https:\/\/doi.org\/10.29007\/FPDH","DOI":"10.29007\/FPDH"},{"key":"13_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-030-30942-8_25","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"S Stucki","year":"2019","unstructured":"Stucki, S., S\u00e1nchez, C., Schneider, G., Bonakdarpour, B.: Gray-Box monitoring of hyperproperties. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 406\u2013424. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_25"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-030-00470-5_5","volume-title":"Research in Attacks, Intrusions, and Defenses","author":"SL Thomas","year":"2018","unstructured":"Thomas, S.L., Francillon, A.: Backdoors: definition, deniability and detection. In: Bailey, M., Holz, T., Stamatogiannakis, M., Ioannidis, S. (eds.) RAID 2018. LNCS, vol. 11050, pp. 92\u2013113. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-00470-5_5"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-96-0617-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T15:09:11Z","timestamp":1732806551000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-96-0617-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9789819606160","9789819606177"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-981-96-0617-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hiroshima","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.icfem2024.info\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}