{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,29]],"date-time":"2025-03-29T16:49:04Z","timestamp":1743266944239,"version":"3.37.3"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,11,11]],"date-time":"2022-11-11T00:00:00Z","timestamp":1668124800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,11,11]],"date-time":"2022-11-11T00:00:00Z","timestamp":1668124800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"name":"NSF","award":["NS-1816637 and 1718586"],"award-info":[{"award-number":["NS-1816637 and 1718586"]}]},{"name":"Intel"},{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Cryptogr Eng"],"published-print":{"date-parts":[[2023,11]]},"DOI":"10.1007\/s13389-022-00306-w","type":"journal-article","created":{"date-parts":[[2022,11,11]],"date-time":"2022-11-11T13:03:02Z","timestamp":1668171782000},"page":"391-407","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Isadora: automated information-flow property generation for hardware security verification"],"prefix":"10.1007","volume":"13","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1354-7200","authenticated-orcid":false,"given":"Calvin","family":"Deutschbein","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andres","family":"Meza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco","family":"Restuccia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ryan","family":"Kastner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cynthia","family":"Sturton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,11,11]]},"reference":[{"key":"306_CR1","doi-asserted-by":"publisher","unstructured":"Ammons, G., Bod\u00edk, R., and Larus, J.R.: Mining specifications. In 29th Symposium on Principles of Programming Languages (POPL). ACM, 4\u201316. (2002) https:\/\/doi.org\/10.1145\/503272.503275","DOI":"10.1145\/503272.503275"},{"key":"306_CR2","doi-asserted-by":"crossref","unstructured":"Ardeshiricham, A., Hu, W., Marxen, J., Kastner, R.: Register transfer level information flow tracking for provably secure hardware design. In Design. Automation Test in Europe Conference Exhibition (DATE) 2017, 1691\u20131696 (2017)","DOI":"10.23919\/DATE.2017.7927266"},{"key":"306_CR3","doi-asserted-by":"crossref","unstructured":"Bilzor, M., Huffmire, T., Irvine, C., Levin, T.: Security checkers: Detecting processor malicious inclusions at runtime. In International Symposium on Hardware-Oriented Security and Trust (HOST). IEEE, 34\u201339 (2011)","DOI":"10.1109\/HST.2011.5954992"},{"key":"306_CR4","unstructured":"Brown, M.: Cross-validation processor specifications. Master\u2019s thesis, University of North Carolina at Chapel Hill (2017)"},{"key":"306_CR5","doi-asserted-by":"crossref","unstructured":"Chang, P.-H., Wang, L.C.: Automatic assertion extraction via sequential data mining of simulation traces. In 15th Asia and South Pacific Design Automation Conference (ASP-DAC). IEEE, 607\u2013612 (2010)","DOI":"10.1109\/ASPDAC.2010.5419813"},{"key":"306_CR6","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur.\u00a0186, 1157\u20131210. (2010). http:\/\/dl.acm.org\/citation.cfm?id=1891823.1891830","DOI":"10.3233\/JCS-2009-0393"},{"key":"306_CR7","doi-asserted-by":"crossref","unstructured":"Danese, A., Ghasempouri, T., Pravadelli, G.: Automatic extraction of assertions from execution traces of behavioural models. In Design, Automation Test in Europe Conference Exhibition (DATE), 67\u201372 (2015)","DOI":"10.7873\/DATE.2015.0110"},{"key":"306_CR8","doi-asserted-by":"crossref","unstructured":"Danese, A., Pravadelli, G., Zandon\u00e0, I.: Automatic generation of power state machines through dynamic mining of temporal assertions. In Design, Automation Test in Europe Conference Exhibition (DATE), 606\u2013611 (2016)","DOI":"10.3850\/9783981537079_0278"},{"key":"306_CR9","doi-asserted-by":"crossref","unstructured":"Danese, A., Riva, N.D., Pravadelli, G.: A-TEAM: Automatic template-based assertion miner. In 54th Design Automation Conference (DAC). ACM\/EDAC\/IEEE, 1\u20136 (2017)","DOI":"10.1145\/3061639.3062206"},{"key":"306_CR10","unstructured":"Dessouky, G., Gens, D., Haney, P., Persyn, G., Kanuparthi, A., Khattri, H., Fung, J.M., Sadeghi, A.-R., Rajendran, J.: Hardfails: Insights into software-exploitable hardware bugs. In 28th USENIX Security Symposium. USENIX Association, 213\u2013230 (2019)"},{"key":"306_CR11","doi-asserted-by":"crossref","unstructured":"Deutschbein, C., Sturton, C.: Mining security critical linear temporal logic specifications for processors. In International Workshop on Microprocessor and SoC Test, Security, and Verification (MTV). IEEE (2018)","DOI":"10.1109\/MTV.2018.00013"},{"key":"306_CR12","doi-asserted-by":"crossref","unstructured":"Deutschbein, C., Sturton, C.: Evaluating security specification mining for a cisc architecture. In 2020 IEEE International Symposium on Hardware Oriented Security and Trust (HOST), 164\u2013175 (2020)","DOI":"10.1109\/HOST45689.2020.9300291"},{"key":"306_CR13","doi-asserted-by":"crossref","unstructured":"Deutschbein, C., Sturton, C.: Evaluating security specification mining for a CISC architecture. In Symposium on Hardware Oriented Security and Trust (HOST). IEEE (2020)","DOI":"10.1109\/HOST45689.2020.9300291"},{"issue":"1\u20133","key":"306_CR14","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007). https:\/\/doi.org\/10.1016\/j.scico.2007.01.015","journal-title":"Sci. Comput. Program."},{"key":"306_CR15","doi-asserted-by":"crossref","unstructured":"Farzana, N., Rahman, F., Tehranipoor, M., Farahmandi, F.: Soc security verification using property checking. In 2019 IEEE International Test Conference (ITC), 1\u201310 (2019)","DOI":"10.1109\/ITC44170.2019.9000170"},{"key":"306_CR16","doi-asserted-by":"publisher","unstructured":"Gabel, M., Su, Z.: Javert: Fully automatic mining of general temporal properties from dynamic traces. In 16th International Symposium on Foundations of Software Engineering (FSE). ACM, 339\u2013349. (2008a). https:\/\/doi.org\/10.1145\/1453101.1453150","DOI":"10.1145\/1453101.1453150"},{"key":"306_CR17","doi-asserted-by":"publisher","unstructured":"Gabel, M., Su, Z.: Symbolic mining of temporal specifications. In 30th International Conference on Software Engineering (ICSE). ACM, 51\u201360. (2008b). https:\/\/doi.org\/10.1145\/1368088.1368096","DOI":"10.1145\/1368088.1368096"},{"key":"306_CR18","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In 1982 IEEE Symposium on Security and Privacy, 11\u201311 (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"306_CR19","doi-asserted-by":"crossref","unstructured":"Hangal, S., Chandra, N., Narayanan, S., Chakravorty, S.: IODINE: a tool to automatically infer dynamic invariants for hardware designs. In 42nd annual Design Automation Conference. ACM, 775\u2013778 (2005a)","DOI":"10.1145\/1065579.1065786"},{"key":"306_CR20","doi-asserted-by":"crossref","unstructured":"Hangal, S., Narayanan, S., Chandra, N., Chakravorty, S.: IODINE: A tool to automatically infer dynamic invariants for hardware designs. In 42nd Design Automation Conference (DAC). IEEE (2005b)","DOI":"10.1145\/1065579.1065786"},{"issue":"6","key":"306_CR21","doi-asserted-by":"publisher","first-page":"952","DOI":"10.1109\/TCAD.2013.2241176","volume":"32","author":"S Hertz","year":"2013","unstructured":"Hertz, S., Sheridan, D., Vasudevan, S.: Mining hardware assertions with guidance from static analysis. Trans Comput-Aided Design Integr Circuits Syst 32(6), 952\u2013965 (2013)","journal-title":"Trans Comput-Aided Design Integr Circuits Syst"},{"key":"306_CR22","doi-asserted-by":"publisher","unstructured":"Hicks, M., Sturton, C., King, S.T., Smith, J.M.: SPECS: A lightweight runtime mechanism for protecting software from security-critical processor bugs. In Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). ACM, 517\u2013529 (2015) https:\/\/doi.org\/10.1145\/2694344.2694366","DOI":"10.1145\/2694344.2694366"},{"key":"306_CR23","doi-asserted-by":"crossref","unstructured":"Hu, W., Althoff, A., Ardeshiricham, A., Kastner, R.: Towards property driven hardware security. In 2016 17th International Workshop on Microprocessor and SOC Test and Verification (MTV). IEEE, 51\u201356 (2016)","DOI":"10.1109\/MTV.2016.12"},{"key":"306_CR24","first-page":"4","volume":"54","author":"W Hu","year":"2021","unstructured":"Hu, W., Ardeshiricham, A., Kastner, R.: Hardware information flow tracking. ACM Comput. Surv. 54, 4 (2021)","journal-title":"ACM Comput. Surv."},{"key":"306_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2676548","volume":"20","author":"W Hu","year":"2014","unstructured":"Hu, W., Mu, D., Oberg, J., Mao, B., Tiwari, M., Sherwood, T., Kastner, R.: Gate-level information flow tracking for security lattices. ACM Trans. Des. Autom. Electron. Syst. 20, 1 (2014). https:\/\/doi.org\/10.1145\/2676548","journal-title":"ACM Trans. Des. Autom. Electron. Syst."},{"key":"306_CR26","doi-asserted-by":"publisher","unstructured":"Li, W., Forin, A., Seshia, S.A.: Scalable specification mining for verification and diagnosis. In 47th Design Automation Conference (DAC). ACM, 755\u2013760 (2010). https:\/\/doi.org\/10.1145\/1837274.1837466","DOI":"10.1145\/1837274.1837466"},{"key":"306_CR27","doi-asserted-by":"crossref","unstructured":"Liu, L., Lin, C., Vasudevan, S.: Word level feature discovery to enhance quality of assertion mining. In International Conference on Computer-Aided Design (ICCAD). IEEE\/ACM, 210\u2013217 (2012)","DOI":"10.1145\/2429384.2429424"},{"key":"306_CR28","unstructured":"Logic, T.: Radix Coverage for Hardware Common Weakness Enumeration (CWE) Guide"},{"key":"306_CR29","doi-asserted-by":"crossref","unstructured":"Meng, X., Kundu, S., Kanuparthi, A.K., Basu, K.: Rtl-contest: Concolic testing on rtl for detecting security vulnerabilities. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1 (2021)","DOI":"10.1109\/TCAD.2021.3066560"},{"key":"306_CR30","doi-asserted-by":"publisher","unstructured":"Min, C., Kashyap, S., Lee, B., Song, C., Kim, T.: Cross-checking semantic correctness: The case of finding file system bugs. In 25th Symposium on Operating Systems Principles (SOSP). ACM, 361\u2013377. (2015). https:\/\/doi.org\/10.1145\/2815400.2815422","DOI":"10.1145\/2815400.2815422"},{"key":"306_CR31","unstructured":"MITRE. The Common Weakness Enumeration Official Webpage"},{"key":"306_CR32","doi-asserted-by":"publisher","unstructured":"Perkins, J.H., Kim, S., Larsen, S., Amarasinghe, S., Bachrach, J., Carbin, M., Pacheco, C., Sherwood, F., Sidiroglou, S., Sullivan, G., Wong, W.-F., Zibin, Y., Ernst, M.D., Rinard, M.: Automatically patching errors in deployed software. In 22nd Symposium on Operating Systems Principles (SOSP). ACM, 87\u2013102 (2009). https:\/\/doi.org\/10.1145\/1629575.1629585","DOI":"10.1145\/1629575.1629585"},{"issue":"5","key":"306_CR33","doi-asserted-by":"publisher","first-page":"798","DOI":"10.1109\/TCAD.2018.2834421","volume":"38","author":"C Pilato","year":"2019","unstructured":"Pilato, C., Wu, K., Garg, S., Karri, R., Regazzoni, F.: Tainthls: High-level synthesis for dynamic information flow tracking. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 38(5), 798\u2013808 (2019)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"306_CR34","doi-asserted-by":"crossref","unstructured":"Rawat, M., Muduli, S.K., Subramanyan, P.: Mining hyperproperties from behavioral traces. In 2020 IFIP\/IEEE 28th International Conference on Very Large Scale Integration (VLSI-SOC), 88\u201393 (2020)","DOI":"10.1109\/VLSI-SOC46417.2020.9344106"},{"key":"306_CR35","doi-asserted-by":"crossref","unstructured":"Reger, G., Barringer, H., Rydeheard, D.: A pattern-based approach to parametric specification mining. In 28th International Conference on Automated Software Engineering (ASE). IEEE\/ACM, 658\u2013663 (2013)","DOI":"10.1109\/ASE.2013.6693129"},{"key":"306_CR36","doi-asserted-by":"crossref","unstructured":"Restuccia, F., Meza, A., Kastner, R.: KER: A design and verification framework for safe and secure soc access control. CoRR arxiv:2106.13263 (2021)","DOI":"10.1109\/ICCAD51958.2021.9643538"},{"key":"306_CR37","unstructured":"Tan, L., Zhang, X., Ma, X., Xiong, W., Zhou, Y.: AutoISES: Automatically inferring security specifications and detecting violations. In 17th USENIX Security Symposium. USENIX Association, 379\u2013394 (2008). http:\/\/dl.acm.org\/citation.cfm?id=1496711.1496737"},{"key":"306_CR38","doi-asserted-by":"crossref","unstructured":"Tiwari, M., Wassel, H.M., Mazloom, B., Mysore, S., Chong, F.T., and Sherwood, T.: Complete information flow tracking from the gates up. In Proceedings of the 14th international conference on Architectural support for programming languages and operating systems, 109\u2013120 (2009)","DOI":"10.1145\/1508244.1508258"},{"key":"306_CR39","doi-asserted-by":"publisher","unstructured":"Weimer, W., Necula, G.C.: Mining temporal specifications for error detection. In 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer-Verlag, 461\u2013476 (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_30","DOI":"10.1007\/978-3-540-31980-1_30"},{"key":"306_CR40","unstructured":"Yamaguchi, F., Lindner, F., Rieck, K.: Vulnerability extrapolation: Assisted discovery of vulnerabilities using machine learning. In 5th USENIX Conference on Offensive Technologies (WOOT). USENIX Association, 13 (2011). http:\/\/dl.acm.org\/citation.cfm?id=2028052.2028065"},{"key":"306_CR41","doi-asserted-by":"publisher","unstructured":"Yang, J., Evans, D., Bhardwaj, D., Bhat, T., Das, M.: Perracotta: mining temporal API rules from imperfect traces. In 28th International Conference on Software Engineering (ICSE). ACM, 282\u2013291 (2006). https:\/\/doi.org\/10.1145\/1134285.1134325","DOI":"10.1145\/1134285.1134325"},{"issue":"4","key":"306_CR42","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1145\/2775054.2694372","volume":"50","author":"D Zhang","year":"2015","unstructured":"Zhang, D., Wang, Y., Suh, G.E., Myers, A.C.: A hardware design language for timing-sensitive information-flow security. Acm Sigplan Notices 50(4), 503\u2013516 (2015)","journal-title":"Acm Sigplan Notices"},{"key":"306_CR43","doi-asserted-by":"crossref","unstructured":"Zhang, R., Stanley, N., Griggs, C., Chi, A., Sturton, C.: Identifying security critical properties for the dynamic verification of a processor. In Architectural Support for Prog. Lang. and Operating Sys. (ASPLOS). ACM (2017)","DOI":"10.1145\/3037697.3037734"}],"container-title":["Journal of Cryptographic Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13389-022-00306-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s13389-022-00306-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13389-022-00306-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,23]],"date-time":"2023-11-23T12:19:12Z","timestamp":1700741952000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s13389-022-00306-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,11]]},"references-count":43,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,11]]}},"alternative-id":["306"],"URL":"https:\/\/doi.org\/10.1007\/s13389-022-00306-w","relation":{},"ISSN":["2190-8508","2190-8516"],"issn-type":[{"type":"print","value":"2190-8508"},{"type":"electronic","value":"2190-8516"}],"subject":[],"published":{"date-parts":[[2022,11,11]]},"assertion":[{"value":"19 June 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 October 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 November 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}