{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,26]],"date-time":"2026-03-26T15:43:32Z","timestamp":1774539812168,"version":"3.50.1"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319231648","type":"print"},{"value":"9783319231655","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23165-5_19","type":"book-chapter","created":{"date-parts":[[2015,8,26]],"date-time":"2015-08-26T03:57:43Z","timestamp":1440561463000},"page":"404-426","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Network-on-Chip Firewall: Countering Defective and Malicious System-on-Chip Hardware"],"prefix":"10.1007","author":[{"given":"Michael","family":"LeMay","sequence":"first","affiliation":[]},{"given":"Carl A.","family":"Gunter","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,27]]},"reference":[{"key":"19_CR1","unstructured":"Bluespec SystemVerilog overview. Technical report, Bluespec, Inc. (2006). http:\/\/www.bluespec.com\/products\/documents\/BluespecSystemVerilogOverview.pdf"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Arbaugh, W.A., Farber, D.J., Smith, J.M.: A secure and reliable bootstrap architecture. In: 18th IEEE Symposium on Security and Privacy, Oakland, CA, USA, pp. 65\u201371, May 1997","DOI":"10.1109\/SECPRI.1997.601317"},{"key":"19_CR3","unstructured":"Arditi, L.: Formal verification: so many applications. In: Design Automation Conference on Electronic Chips & Systems Design Initiative 2010 Presentation, Anaheim, CA, USA, June 2010"},{"key":"19_CR4","unstructured":"Beaumont, M., Hopkins, B., Newby, T.: Hardware trojans - prevention, detection, countermeasures (A literature review). Technical report DSTO-TN-1012, DSTO Defence Science and Technology Organisation, Edinburgh, South Australia, July 2011. http:\/\/www.eetimes.com\/author.asp?section_id=36&doc_id=1266011"},{"key":"19_CR5","unstructured":"Butler, S.: Managing IP quality in the SoC era. Electronic Engineering Times Europe p. 5, October 2011. http:\/\/www.wsj.com\/articles\/SB10001424052748704641604576255223445021138"},{"key":"19_CR6","unstructured":"Cheng, R.: So you want to use your iPhone for work? Uh-oh. Wall Street J., April 2011"},{"key":"19_CR7","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Maude manual (version 2.6). Technical report, January 2011"},{"key":"19_CR8","volume-title":"Formal Verification of a Processor with Memory Management Units","author":"I Dalinger","year":"2006","unstructured":"Dalinger, I.: Formal Verification of a Processor with Memory Management Units. Saarland University, Saarbr\u00fccken (2006)"},{"key":"19_CR9","unstructured":"Goering, R.: Panelists discuss solutions to SoC IP integration challenges. Industry Insights - Cadence Community, May 2011"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Gotze, K.: A survey of frequently identified vulnerabilities in commercial computing semiconductors. In: 4th IEEE International Symposium on Hardware-Oriented Security and Trust, pp. 122\u2013126. HOST, San Diego (2011)","DOI":"10.1109\/HST.2011.5955008"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Huffmire, T., Brotherton, B., Wang, G., Sherwood, T., Kastner, R., Levin, T., Nguyen, T., Irvine, C.: Moats and drawbridges: an isolation primitive for reconfigurable hardware based systems. In: 28th IEEE Symposium on Security and Privacy, Oakland, CA, USA, pp. 281\u2013295, May 2007","DOI":"10.1109\/SP.2007.28"},{"key":"19_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-90-481-9157-4","volume-title":"Handbook of FPGA Design Security","author":"T Huffmire","year":"2010","unstructured":"Huffmire, T., Irvine, C., Nguyen, T.D., Levin, T., Kastner, R., Sherwood, T.: Handbook of FPGA Design Security. Springer, The Netherlands (2010)"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: 22nd ACM Symposium on Operating Systems Principles, SOSP, Big Sky, MT, USA, pp. 207\u2013220, October 2009","DOI":"10.1145\/1629575.1629596"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"LeMay, M., Gunter, C.A.: Network-on-chip firewall: countering defective and malicious system-on-chip hardware, April 2014. http:\/\/arxiv.org\/abs\/1404.3465","DOI":"10.1007\/978-3-319-23165-5_19"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Li, X., Tiwari, M., Oberg, J.K., Kashyap, V., Chong, F.T., Sherwood, T., Hardekopf, B.: Caisson: a hardware description language for secure information flow. In: 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, San Jose, CA, USA, pp. 109\u2013120, June 2011","DOI":"10.1145\/1993498.1993512"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J., Verdejo, A.: A rewriting semantics for Maude strategies. In: 7th International Workshop on Rewriting Logic and its Applications, WRLA, pp. 227\u2013247. Elsevier, Budapest (2008)","DOI":"10.1016\/j.entcs.2009.05.022"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Meredith, P., Katelman, M., Meseguer, J., Rosu, G.: A formal executable semantics of Verilog. In: 8th ACM\/IEEE International Conference on Formal Methods and Models for Codesign, MemoCODE, Grenoble, France, pp. 179\u2013188, July 2010","DOI":"10.1109\/MEMCOD.2010.5558634"},{"key":"19_CR18","unstructured":"Katelman, M.K.: A Meta-Language for Functional Verification. Ph.D. Dissertation, University of Illinois at Urbana-Champaign, Urbana, Illinois (2011)"},{"key":"19_CR19","unstructured":"Mukherjee, S.S., Emer, J., Reinhardt, S.K.: The soft error problem: an architectural perspective. In: 11th International Symposium on High-Performance Computer Architecture, HPCA, pp. 243\u2013247. IEEE, San Francisco (2005)"},{"key":"19_CR20","unstructured":"Nachenberg, C.: A window into mobile device security: examining the security approaches employed in Apple\u2019s iOS and Google\u2019s Android. Technical report, Symantec Security Response, June 2011"},{"issue":"2","key":"19_CR21","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s11334-011-0149-0","volume":"7","author":"D Richards","year":"2011","unstructured":"Richards, D., Lester, D.: A monadic approach to automated reasoning for Bluespec SystemVerilog. Innovations Syst. Softw. Eng. 7(2), 85\u201395 (2011). Springer","journal-title":"Innovations Syst. Softw. Eng."},{"key":"19_CR22","unstructured":"Schubert, E.T., Levitt, K., Cohen, G.C.: Formal verification of a set of memory management units. Contractor Report 189566, National Aeronautics and Space Administration, Hampton, VA, USA, March 1992"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Seshadri, A., Luk, M., Qu, N., Perrig, A.: SecVisor: a tiny hypervisor to provide lifetime kernel code integrity for commodity OSes. In: 21st ACM Symposium on Operating Systems Principles, SOSP, Stevenson, WA, USA, pp. 335\u2013350, October 2007","DOI":"10.1145\/1323293.1294294"},{"key":"19_CR24","unstructured":"Shimpi, A.L.: NVIDIA to acquire Icera, adds software baseband to its portfolio, May 2011. AnandTech.com"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Szefer, J., Keller, E., Lee, R.B., Rexford, J.: Eliminating the hypervisor attack surface for a more secure cloud. In: 18th ACM Conference on Computer and Communications Security, CCS, Chicago, IL, USA, October 2011","DOI":"10.1145\/2046707.2046754"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Tiwari, M., Oberg, J.K., Li, X., Valamehr, J., Levin, T., Hardekopf, B., Kastner, R., Chong, F.T., Sherwood, T.: Crafting a usable microkernel, processor, and I\/O system with strict and provable information flow security. In: 38th International Symposium on Computer Architecture, ISCA, pp. 189\u2013200. ACM, San Jose (2011)","DOI":"10.1145\/2000064.2000087"},{"key":"19_CR27","unstructured":"Villasenor, J.: Ensuring hardware cybersecurity. The Brookings Institution, May 2011"},{"key":"19_CR28","unstructured":"Volpano, D.: Towards provable security for multilevel reconfigurable hardware. Technical report, Naval Postgraduate School (2008)"},{"key":"19_CR29","doi-asserted-by":"crossref","unstructured":"Wassel, H.M.G., Gao, Y., Oberg, J.K., Huffmire, T., Kastner, R., Chong, F.T., Sherwood, T.: SurfNoC: a low latency and provably non-interfering approach to secure networks-on-chip. In: 40th International Symposium on Computer Architecture, ISCA, pp. 583\u2013594. ACM, Tel-Aviv (2013)","DOI":"10.1145\/2485922.2485972"}],"container-title":["Lecture Notes in Computer Science","Logic, Rewriting, and Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23165-5_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T04:40:04Z","timestamp":1748580004000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23165-5_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319231648","9783319231655"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23165-5_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"27 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}