{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T20:13:41Z","timestamp":1729628021557,"version":"3.28.0"},"reference-count":19,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,5]]},"DOI":"10.1109\/hst.2016.7495566","type":"proceedings-article","created":{"date-parts":[[2016,6,25]],"date-time":"2016-06-25T11:39:11Z","timestamp":1466854751000},"page":"109-113","source":"Crossref","is-referenced-by-count":1,"title":["Model checking to find vulnerabilities in an instruction set architecture"],"prefix":"10.1109","author":[{"given":"Chris","family":"Bradfield","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cynthia","family":"Sturton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","article-title":"Formal Verification of the ARM6 Micro-Architecture","author":"fox","year":"2002","journal-title":"Technical Report UCAM-CL-TR-548"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_2"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_23"},{"key":"ref13","first-page":"441","article-title":"Patrice Godefroid and Ankur Taly. Automated synthesis of symbolic instruction encodings from I\/O samples","volume":"47","year":"2012","journal-title":"Programming Language Design and Implementation"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2150976.2151012"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831730"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572303"},{"key":"ref17","first-page":"271","article-title":"Cardinal Pill Testing of System Virtual Machines","author":"shi","year":"2014","journal-title":"23rd USENIX Security Symposium (USENIX Security 14)"},{"key":"ref18","article-title":"Towards a Formal Model of the x86 ISA","author":"hunt","year":"2012","journal-title":"Technical report University of Texas at Austin"},{"key":"ref19","article-title":"A Stitch In Time Saves Nine: A Case Of Multiple OS Vulnerability","author":"wojtczuk","year":"2012","journal-title":"Black Hat"},{"journal-title":"Opensparc t2 source code Sun","year":"0","key":"ref4"},{"journal-title":"Intel The IA-32 Intel Architecture Software Developer's Manual","year":"0","key":"ref3"},{"journal-title":"Vulnerability Notes Database 2012","article-title":"SYSRET 64-bit operating system privilege escalation vulnerability on Intel CPU hardware","year":"0","key":"ref6"},{"journal-title":"Xen Security Advisory 7 (CVE-2012–0217) - PV privilege escalation Xen-announce","year":"0","key":"ref5"},{"journal-title":"Updated Specifications","article-title":"Intel Core i7–600, i5-500, i5-400 and i3-300 Mobile Processor Series","year":"2014","key":"ref8"},{"journal-title":"Product Revision","article-title":"Revision Guide for AMD Family 16h Models 00h-0Fh Processors","year":"2013","key":"ref7"},{"journal-title":"DynAlloy An efficient extension of Alloy with procedural actions","year":"0","key":"ref2"},{"journal-title":"General-Purpose and System Instructions","article-title":"AMD64 Architecture Programmers Manual Volume 3","year":"0","key":"ref1"},{"key":"ref9","article-title":"Advanced exploitation of Windows kernel Intel 64-bit mode SYSRET vulnerability (ms12–042)","author":"bonetti","year":"2012","journal-title":"VUPEN Vulnerability Research Team (VRT) Blog"}],"event":{"name":"2016 IEEE International Symposium on Hardware Oriented Security and Trust (HOST)","start":{"date-parts":[[2016,5,3]]},"location":"McLean, VA, USA","end":{"date-parts":[[2016,5,5]]}},"container-title":["2016 IEEE International Symposium on Hardware Oriented Security and Trust (HOST)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7489989\/7495545\/07495566.pdf?arnumber=7495566","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2016,9,29]],"date-time":"2016-09-29T13:03:18Z","timestamp":1475154198000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7495566\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5]]},"references-count":19,"URL":"https:\/\/doi.org\/10.1109\/hst.2016.7495566","relation":{},"subject":[],"published":{"date-parts":[[2016,5]]}}}