{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T16:18:02Z","timestamp":1761581882927,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030317836"},{"type":"electronic","value":"9783030317843"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-31784-3_29","type":"book-chapter","created":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T21:32:04Z","timestamp":1571607124000},"page":"499-514","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Efficient Information-Flow Verification Under Speculative Execution"],"prefix":"10.1007","author":[{"given":"Roderick","family":"Bloem","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Swen","family":"Jacobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yakir","family":"Vizel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,10,21]]},"reference":[{"key":"29_CR1","doi-asserted-by":"publisher","unstructured":"Agat, J.: Transforming out timing leaks. In: POPL, pp. 40\u201353. ACM (2000). https:\/\/doi.org\/10.1145\/325694.325702","DOI":"10.1145\/325694.325702"},{"key":"29_CR2","unstructured":"Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F., Emmi, M.: Verifying constant-time implementations. In: USENIX Security, pp. 53\u201370. USENIX Association (2016). https:\/\/www.usenix.org\/conference\/usenixsecurity16\/technical-sessions\/presentation\/almeida"},{"issue":"7","key":"29_CR3","doi-asserted-by":"publisher","first-page":"796","DOI":"10.1016\/j.scico.2011.10.008","volume":"78","author":"JB Almeida","year":"2013","unstructured":"Almeida, J.B., Barbosa, M., Pinto, J.S., Vieira, B.: Formal verification of side-channel countermeasures using self-composition. Sci. Comput. Program. 78(7), 796\u2013812 (2013). https:\/\/doi.org\/10.1016\/j.scico.2011.10.008","journal-title":"Sci. Comput. Program."},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/3-540-46419-0_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Arons","year":"2000","unstructured":"Arons, T., Pnueli, A.: A comparison of two verification methods for speculative instruction execution. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 487\u2013502. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46419-0_33"},{"key":"29_CR5","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Computer Security Foundations Workshop, (CSFW-17), pp. 100\u2013114 (2004)"},{"issue":"6","key":"29_CR6","doi-asserted-by":"publisher","first-page":"1207","DOI":"10.1017\/S0960129511000193","volume":"21","author":"G Barthe","year":"2011","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. Math. Struct. Comput. Sci. 21(6), 1207\u20131252 (2011). https:\/\/doi.org\/10.1017\/S0960129511000193","journal-title":"Math. Struct. Comput. Sci."},{"key":"29_CR7","unstructured":"Bhattacharyya, A., et al.: Smotherspectre: exploiting speculative execution through port contention. CoRR abs\/1903.01843 (2019). http:\/\/arxiv.org\/abs\/1903.01843"},{"key":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-642-11957-6_10","volume-title":"Programming Languages and Systems","author":"G Boudol","year":"2010","unstructured":"Boudol, G., Petri, G.: A theory of speculative computation. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 165\u2013184. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_10"},{"key":"29_CR9","unstructured":"Canella, C., et al.: A systematic evaluation of transient execution attacks and defenses. CoRR. https:\/\/arxiv.org\/abs\/1811.05441 (2018)"},{"key":"29_CR10","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-54792-8_15","volume-title":"Principles of Security and Trust","author":"MR Clarkson","year":"2014","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265\u2013284. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15"},{"issue":"7","key":"29_CR12","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"DE Denning","year":"1977","unstructured":"Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504\u2013513 (1977)","journal-title":"Commun. ACM"},{"key":"29_CR13","unstructured":"Guarnieri, M., K\u00f6pf, B., Morales, J.F., Reineke, J., S\u00e1nchez, A.: SPECTECTOR: principled detection of speculative information flows. CoRR. http:\/\/arxiv.org\/abs\/1812.08639 (2018)"},{"key":"29_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"issue":"6","key":"29_CR15","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/s10207-009-0086-1","volume":"8","author":"C Hammer","year":"2009","unstructured":"Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. Int. J. Inf. Secur. 8(6), 399\u2013422 (2009)","journal-title":"Int. J. Inf. Secur."},{"key":"29_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/10722167_39","volume-title":"Computer Aided Verification","author":"R Hosabettu","year":"2000","unstructured":"Hosabettu, R., Gopalakrishnan, G., Srivas, M.: Verifying advanced microarchitectures that support speculation and exceptions. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 521\u2013537. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_39"},{"key":"29_CR17","unstructured":"Intel: White paper: intel analysis of speculative execution side channels. Tech. Rep. 336983\u2013001, Revision 1.0. https:\/\/newsroom.intel.com\/wp-content\/uploads\/sites\/11\/2018\/01\/Intel-Analysis-of-Speculative-Execution-Side-Channels.pdf"},{"key":"29_CR18","unstructured":"Intel: Q2 2018 speculative execution side channel update (2018). https:\/\/www.intel.com\/content\/www\/us\/en\/security-center\/advisory\/intel-sa-00115.html . Accessed May 2019"},{"key":"29_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/3-540-44585-4_40","volume-title":"Computer Aided Verification","author":"R Jhala","year":"2001","unstructured":"Jhala, R., McMillan, K.L.: Microarchitecture verification by compositional model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 396\u2013410. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_40"},{"key":"29_CR20","unstructured":"Kiriansky, V., Waldspurger, C.: Speculative buffer overflows: attacks and defenses. CoRR. http:\/\/arxiv.org\/abs\/1807.03757 (2018)"},{"key":"29_CR21","unstructured":"Kocher, P.: Spectre Mitigations in Microsoft\u2019s C\/C++ Compiler. https:\/\/www.paulkocher.com\/doc\/MicrosoftCompilerSpectreMitigation.html"},{"key":"29_CR22","doi-asserted-by":"crossref","unstructured":"Kocher, P., et al.: Spectre attacks: exploiting speculative execution. CoRR. http:\/\/arxiv.org\/abs\/1801.01203 (2018)","DOI":"10.1109\/SP.2019.00002"},{"key":"29_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-540-45069-6_33","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E.: Deductive verification of advanced out-of-order microprocessors. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 341\u2013354. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_33"},{"key":"29_CR24","doi-asserted-by":"publisher","unstructured":"Maisuradze, G., Rossow, C.: ret2spec: speculative execution using return stack buffers. In: CCS, pp. 2109\u20132122. ACM (2018). https:\/\/doi.org\/10.1145\/3243734.3243761","DOI":"10.1145\/3243734.3243761"},{"key":"29_CR25","unstructured":"Pardoe, A.: Spectre mitigations in MSVC (2018). https:\/\/blogs.msdn.microsoft.com\/vcblog\/2018\/01\/15\/spectre-mitigations-in-msvc\/ . Accessed May 2019"},{"key":"29_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/11531142_16","volume-title":"ECOOP 2005 - Object-Oriented Programming","author":"M Pistoia","year":"2005","unstructured":"Pistoia, M., Flynn, R.J., Koved, L., Sreedhar, V.C.: Interprocedural analysis for privileged code placement and tainted variable detection. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 362\u2013386. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11531142_16"},{"key":"29_CR27","doi-asserted-by":"publisher","unstructured":"Rodrigues, B., Pereira, F.M.Q., Aranha, D.F.: Sparse representation of implicit flows with applications to side-channel detection. In: CC, pp. 110\u2013120. ACM (2016). https:\/\/doi.org\/10.1145\/2892208.2892230","DOI":"10.1145\/2892208.2892230"},{"key":"29_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/BFb0028740","volume-title":"Computer Aided Verification","author":"J Sawada","year":"1998","unstructured":"Sawada, J., Hunt, W.A.: Processor verification with precise exceptions and speculative execution. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 135\u2013146. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028740"},{"key":"29_CR29","unstructured":"Stecklina, J., Prescher, T.: Lazyfp: leaking FPU register state using microarchitectural side-channels. CoRR. http:\/\/arxiv.org\/abs\/1806.07480 (2018)"},{"key":"29_CR30","doi-asserted-by":"publisher","unstructured":"Taram, M., Venkat, A., Tullsen, D.M.: Context-sensitive fencing: Securing speculative execution via microcode customization. In: ASPLOS, pp. 395\u2013410. ACM (2019). https:\/\/doi.org\/10.1145\/3297858.3304060","DOI":"10.1145\/3297858.3304060"},{"key":"29_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352\u2013367. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11547662_24"},{"key":"29_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/10722167_24","volume-title":"Computer Aided Verification","author":"MN Velev","year":"2000","unstructured":"Velev, M.N.: Formal verification of VLIW microprocessors with speculative execution. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 296\u2013311. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_24"},{"key":"29_CR33","doi-asserted-by":"crossref","unstructured":"Wang, G., Chattopadhyay, S., Gotovchits, I., Mitra, T., Roychoudhury, A.: oo7: low-overhead defense against spectre attacks via binary analysis. CoRR. http:\/\/arxiv.org\/abs\/1807.05843 (2018)","DOI":"10.1109\/TSE.2019.2953709"},{"key":"29_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-319-96142-2_11","volume-title":"Computer Aided Verification","author":"W Yang","year":"2018","unstructured":"Yang, W., Vizel, Y., Subramanyan, P., Gupta, A., Malik, S.: Lazy self-composition for security verification. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 136\u2013156. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_11"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31784-3_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,9]],"date-time":"2019-12-09T18:09:46Z","timestamp":1575914986000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-31784-3_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030317836","9783030317843"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31784-3_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"21 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taipei","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taiwan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/atva2019.iis.sinica.edu.tw\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Open","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"87","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Between 1 and 2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}