{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T14:24:26Z","timestamp":1771856666572,"version":"3.50.1"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2021,6,8]],"date-time":"2021-06-08T00:00:00Z","timestamp":1623110400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,6,8]],"date-time":"2021-06-08T00:00:00Z","timestamp":1623110400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP160102457"],"award-info":[{"award-number":["DP160102457"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100008812","name":"Defence Science and Technology Group","doi-asserted-by":"publisher","award":["NA"],"award-info":[{"award-number":["NA"]}],"id":[{"id":"10.13039\/501100008812","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,10]]},"DOI":"10.1007\/s10703-021-00376-2","type":"journal-article","created":{"date-parts":[[2021,6,8]],"date-time":"2021-06-08T10:08:40Z","timestamp":1623146920000},"page":"251-293","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Information-flow control on ARM and POWER multicore processors"],"prefix":"10.1007","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1019-4761","authenticated-orcid":false,"given":"Graeme","family":"Smith","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicholas","family":"Coughlin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toby","family":"Murray","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,6,8]]},"reference":[{"issue":"2","key":"376_CR1","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/2627752","volume":"36","author":"J Alglave","year":"2014","unstructured":"Alglave J, Maranget L, Tautschnig M (2014) Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans Program Lang Syst 36(2):7:1-7:74. https:\/\/doi.org\/10.1145\/2627752","journal-title":"ACM Trans Program Lang Syst"},{"key":"376_CR2","unstructured":"Almeida JB, Barbosa M, Barthe G, Dupressoir F, Emmi M (2016) Verifying constant-time implementations. In: Holz T, Savage S (eds) 25th USENIX Security Symposium, USENIX Security 16, pp 53\u201370. USENIX Association. https:\/\/www.usenix.org\/conference\/usenixsecurity16\/technical-sessions\/presentation\/almeida"},{"issue":"POPL","key":"376_CR3","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/3371075","volume":"4","author":"G Barthe","year":"2020","unstructured":"Barthe G, Blazy S, Gr\u00e9goire B, Hutin R, Laporte V, Pichardie D, Trieu A (2020) Formal verification of a constant-time preserving C compiler. Proc ACM Program Lang (PACMPL) 4(POPL):7:1-7:30. https:\/\/doi.org\/10.1145\/3371075","journal-title":"Proc ACM Program Lang (PACMPL)"},{"key":"376_CR4","doi-asserted-by":"publisher","unstructured":"Boehm H (2012) Can seqlocks get along with programming language memory models? In: Zhang L, Mutlu O (eds.) Proceedings of the 2012 ACM SIGPLAN workshop on Memory Systems Performance and Correctness: held in conjunction with PLDI \u201912, pp 12\u201320. ACM. doi: https:\/\/doi.org\/10.1145\/2247684.2247688","DOI":"10.1145\/2247684.2247688"},{"key":"376_CR5","doi-asserted-by":"publisher","unstructured":"Casinghino C, Paasch JT, Roux C, Altidor J, Dixon M, Jamner D (2019) Using binary analysis frameworks: The case for BAP and angr. In: Badger JM, Rozier KY (eds) NASA Formal Methods\u201411th International Symposium, NFM 2019, Lecture Notes in Computer Science, vol. 11460, pp 123\u2013129. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-030-20652-9_8","DOI":"10.1007\/978-3-030-20652-9_8"},{"issue":"4","key":"376_CR6","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1145\/358598.358613","volume":"24","author":"KM Chandy","year":"1981","unstructured":"Chandy KM, Misra J (1981) Asynchronous distributed simulation via a sequence of parallel computations. Commun ACM 24(4):198\u2013206. https:\/\/doi.org\/10.1145\/358598.358613","journal-title":"Commun ACM"},{"key":"376_CR7","doi-asserted-by":"publisher","unstructured":"Chase D, Lev Y (2005) Dynamic circular work-stealing deque. In: ACM symposium on parallelism in algorithms and architectures (SPAA\u201905), pp 21\u201328. ACM Press, New York. https:\/\/doi.org\/10.1145\/1073970.1073974","DOI":"10.1145\/1073970.1073974"},{"key":"376_CR8","unstructured":"Colvin RJ, Smith G (2018) A high-level operational semantics for hardware weak memory models. CoRR abs\/1812.00996"},{"key":"376_CR9","doi-asserted-by":"publisher","unstructured":"Colvin RJ, Smith G (2018) A wide-spectrum language for verification of programs on weak memory models. In: Havelund K, Peleska J, Roscoe B, de\u00a0Vink EP (eds.) Formal Methods\u201422nd International Symposium, FM 2018, Lecture Notes in Computer Science, vol. 10951, pp 240\u2013257. Springer. https:\/\/doi.org\/10.1007\/978-3-319-95582-7_14","DOI":"10.1007\/978-3-319-95582-7_14"},{"key":"376_CR10","doi-asserted-by":"publisher","unstructured":"Coughlin N, Smith G (2020) Rely\/guarantee reasoning for noninterference in non-blocking algorithms. In: 33rd IEEE Computer Security Foundations Symposium, CSF 2020, pp 380\u2013394. IEEE. doi: https:\/\/doi.org\/10.1109\/CSF49147.2020.00034","DOI":"10.1109\/CSF49147.2020.00034"},{"key":"376_CR11","doi-asserted-by":"publisher","unstructured":"D\u2019Silva V, Payer M, Song DX, (2015) The correctness-security gap in compiler optimization. In (2015) IEEE Symposium on Security and Privacy Workshops, SPW 2015, pp 73\u201387. IEEE Computer Society. https:\/\/doi.org\/10.1109\/SPW.2015.33","DOI":"10.1109\/SPW.2015.33"},{"key":"376_CR12","doi-asserted-by":"publisher","unstructured":"Ernst G, Murray T (2019) SecCSL: Security concurrent separation logic. In: Dillig I, Tasiran S (eds) Computer Aided Verification\u201431st International Conference, CAV 2019, Proceedings, Part II, Lecture Notes in Computer Science, vol. 11562, pp 208\u2013230. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-030-25543-5_13","DOI":"10.1007\/978-3-030-25543-5_13"},{"issue":"5","key":"376_CR13","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1145\/1941487.1941501","volume":"54","author":"J Fitzpatrick","year":"2011","unstructured":"Fitzpatrick J (2011) An interview with Steve Furber. Commun ACM 54(5):34\u201339. https:\/\/doi.org\/10.1145\/1941487.1941501","journal-title":"Commun ACM"},{"key":"376_CR14","doi-asserted-by":"publisher","unstructured":"Flur S, Gray KE, Pulte C, Sarkar S, Sezgin A, Maranget L, Deacon W, Sewell P (2016) Modelling the ARMv8 architecture, operationally: Concurrency and ISA. In: Bod\u00edk R, Majumdar R (eds) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp 608\u2013621. ACM. https:\/\/doi.org\/10.1145\/2837614.2837615","DOI":"10.1145\/2837614.2837615"},{"issue":"10","key":"376_CR15","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576\u2013580. https:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun ACM"},{"key":"376_CR16","unstructured":"Jones CB (1983) Specification and design of (parallel) programs. In: Proceedings of IFIP\u201983, pp 321\u2013332. North-Holland"},{"key":"376_CR17","doi-asserted-by":"crossref","unstructured":"Kang J, Hur C, Lahav O, Vafeiadis V, Dreyer D (2017) A promising semantics for relaxed-memory concurrency. In: Castagna G, Gordon AD (eds) Proceedings of the 44th ACM SIGPLAN symposium on principles of programming languages, POPL 2017, pp 175\u2013189. ACM. http:\/\/dl.acm.org\/citation.cfm?id=3009850","DOI":"10.1145\/3009837.3009850"},{"key":"376_CR18","doi-asserted-by":"crossref","unstructured":"Kocher P, Genkin D, Gruss D, Haas W, Hamburg M, Lipp M, Mangard S, Prescher T, Schwarz M, Yarom Y (2018) Spectre attacks: Exploiting speculative execution. CoRR abs\/1801.01203. http:\/\/arxiv.org\/abs\/1801.01203","DOI":"10.1109\/SP.2019.00002"},{"key":"376_CR19","doi-asserted-by":"publisher","unstructured":"L\u00ea N, Pop A, Cohen A, Zappa\u00a0Nardelli F (2013) Correct and efficient work-stealing for weak memory models. In: Principles and Practice of Parallel Programming (PPoPP\u201913), pp 69\u201380. ACM. doi: https:\/\/doi.org\/10.1145\/2442516.2442524","DOI":"10.1145\/2442516.2442524"},{"key":"376_CR20","unstructured":"Leroy X, Blazy S, K\u00e4stner D, Schommer B, Pister M, Ferdinand C (2016) CompCert\u2014a formally verified optimizing compiler. In: ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress. SEE. https:\/\/hal.inria.fr\/hal-01238879"},{"key":"376_CR21","doi-asserted-by":"publisher","unstructured":"Louren\u00e7o L, Caires L (2015) Dependent information flow types. In: Rajamani SK, Walker D (eds.) Proceedings of the 42nd annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2015, pp 317\u2013328. ACM. https:\/\/doi.org\/10.1145\/2676726.2676994","DOI":"10.1145\/2676726.2676994"},{"key":"376_CR22","doi-asserted-by":"publisher","unstructured":"Mantel H, Perner M, Sauer J (2014) Noninterference under weak memory models. In: IEEE 27th computer security foundations symposium, CSF 2014, pp 80\u201394. IEEE Computer Society. https:\/\/doi.org\/10.1109\/CSF.2014.14","DOI":"10.1109\/CSF.2014.14"},{"key":"376_CR23","doi-asserted-by":"publisher","unstructured":"Mantel H, Sands D, Sudbrock H (2011) Assumptions and guarantees for compositional noninterference. In: Proceedings of the 24th IEEE computer security foundations symposium, CSF 2011, pp 218\u2013232. IEEE Computer Society. https:\/\/doi.org\/10.1109\/CSF.2011.22","DOI":"10.1109\/CSF.2011.22"},{"key":"376_CR24","doi-asserted-by":"publisher","unstructured":"Moir M, Shavit N (2004) Concurrent data structures. In: Mehta DP, Sahni S (eds) Handbook of data structures and applications. Chapman and Hall\/CRC, Boca Raton. https:\/\/doi.org\/10.1201\/9781420035179.ch47","DOI":"10.1201\/9781420035179.ch47"},{"key":"376_CR25","doi-asserted-by":"publisher","unstructured":"Molnar D, Piotrowski M, Schultz D, Wagner DA (2005) The program counter security model: automatic detection and removal of control-flow side channel attacks. In: Won D, Kim S (eds.) Information security and cryptology - ICISC 2005, 8th international conference, lecture notes in computer science, vol. 3935, pp 156\u2013168. Springer, Berlin. https:\/\/doi.org\/10.1007\/11734727_14","DOI":"10.1007\/11734727_14"},{"key":"376_CR26","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura LM, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Ramakrishnan CR, Rehof J (eds.) Tools and algorithms for the construction and analysis of systems, 14th International conference, TACAS 2008, Held as part of the joint european conferences on theory and practice of software, ETAPS 2008. Proceedings, Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"376_CR27","doi-asserted-by":"publisher","unstructured":"Murray TC (2015) Short paper: On high-assurance information-flow-secure programming languages. In: Clarkson M, Jia L (eds.) Proceedings of the 10th ACM workshop on programming languages and analysis for security, PLAS@ECOOP 2015, pp 43\u201348. ACM. https:\/\/doi.org\/10.1145\/2786558.2786561","DOI":"10.1145\/2786558.2786561"},{"key":"376_CR28","doi-asserted-by":"publisher","unstructured":"Murray TC, Sison R, Engelhardt K, (2018) C overn: A logic for compositional verification of information flow control. In: 2018 IEEE European Symposium on Security and Privacy, EuroS&P 2018, pp 16\u201330. IEEE. https:\/\/doi.org\/10.1109\/EuroSP.2018.00010","DOI":"10.1109\/EuroSP.2018.00010"},{"key":"376_CR29","doi-asserted-by":"publisher","unstructured":"Murray TC, Sison R, Pierzchalski E, Rizkallah C (2016) Compositional verification and refinement of concurrent value-dependent noninterference. In: IEEE 29th computer security foundations symposium, CSF, pp 417\u2013431. IEEE Computer Society (2016). https:\/\/doi.org\/10.1109\/CSF.2016.36","DOI":"10.1109\/CSF.2016.36"},{"key":"376_CR30","doi-asserted-by":"publisher","unstructured":"Nipkow T, Paulson LC, Wenzel M (2002) Isabelle\/HOL\u2014A proof assistant for higher-order logic. lecture notes in computer science, vol. 2283. Springer, Berlin. https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"376_CR31","doi-asserted-by":"publisher","unstructured":"Pulte C, Flur S, Deacon W, French J, Sarkar S, Sewell P (2018) Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. Proceedings of the ACM on programming languages (PACMPL) 2(POPL):19:1-19:29. https:\/\/doi.org\/10.1145\/3158107","DOI":"10.1145\/3158107"},{"issue":"1","key":"376_CR32","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2003","unstructured":"Sabelfeld A, Myers AC (2003) Language-based information-flow security. IEEE J Sel Areas Commun 21(1):5\u201319. https:\/\/doi.org\/10.1109\/JSAC.2002.806121","journal-title":"IEEE J Sel Areas Commun"},{"key":"376_CR33","doi-asserted-by":"publisher","unstructured":"Sarkar S, Sewell P, Alglave J, Maranget L, Williams D (2011) Understanding POWER multiprocessors. In: Hall MW, Padua DA (eds.) Proceedings of the 32nd ACM SIGPLAN conference on programming language design and implementation, PLDI 2011, pp 175\u2013186. ACM. https:\/\/doi.org\/10.1145\/1993498.1993520","DOI":"10.1145\/1993498.1993520"},{"key":"376_CR34","doi-asserted-by":"crossref","unstructured":"Schoepe D, Murray T, Sabelfeld A (2020) Veronica: Expressive and precise concurrent information flow security. In: IEEE Computer Security Foundations Symposium (CSF), pp 79\u201394","DOI":"10.1109\/CSF49147.2020.00014"},{"issue":"7","key":"376_CR35","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P Sewell","year":"2010","unstructured":"Sewell P, Sarkar S, Owens S, Nardelli FZ, Myreen MO (2010) x86-TSO: a rigorous and usable programmers model for x86 multiprocessors. Commun ACM 53(7):89\u201397. https:\/\/doi.org\/10.1145\/1785414.1785443","journal-title":"Commun ACM"},{"key":"376_CR36","unstructured":"Sison R, Murray T (2019) Verifying that a compiler preserves concurrent value-dependent information-flow security. In: Harrison J, O\u2019Leary J, Tolmach A (eds.) International conference on interactive theorem proving (ITP 2019), Leibniz international proceedings in informatics, vol. 141, pp 27:1\u201327:19. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik"},{"key":"376_CR37","doi-asserted-by":"publisher","unstructured":"Smith G, Coughlin N, Murray T (2019) Value-dependent information-flow security on weak memory models. In: ter Beek MH, McIver A, Oliveira JN (eds) Formal Methods\u2014The Next 30 Years\u2014Third World Congress, FM 2019, Lecture Notes in Computer Science, vol 11800, pp 539\u2013555. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-030-30942-8_32","DOI":"10.1007\/978-3-030-30942-8_32"},{"key":"376_CR38","doi-asserted-by":"publisher","first-page":"e2","DOI":"10.1017\/S0956796818000229","volume":"29","author":"YK Tan","year":"2019","unstructured":"Tan YK, Myreen MO, Kumar R, Fox ACJ, Owens S, Norrish M (2019) The verified CakeML compiler backend. J. Funct. Program. 29:e2. https:\/\/doi.org\/10.1017\/S0956796818000229","journal-title":"J. Funct. Program."},{"key":"376_CR39","doi-asserted-by":"publisher","unstructured":"Vaughan JA, Millstein TD (2012) Secure information flow for concurrent programs under Total Store Order. In: Chong S (ed.) 25th IEEE Computer Security Foundations Symposium, CSF 2012, pp 19\u201329. IEEE Computer Society. doi: https:\/\/doi.org\/10.1109\/CSF.2012.20","DOI":"10.1109\/CSF.2012.20"},{"issue":"2\u20133","key":"376_CR40","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/s10207-007-0019-9","volume":"6","author":"L Zheng","year":"2007","unstructured":"Zheng L, Myers AC (2007) Dynamic security labels and static information flow control. Int. J. Inf. Sec. 6(2\u20133):67\u201384. https:\/\/doi.org\/10.1007\/s10207-007-0019-9","journal-title":"Int. J. Inf. Sec."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00376-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00376-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00376-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,26]],"date-time":"2022-08-26T15:51:34Z","timestamp":1661529094000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00376-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,8]]},"references-count":40,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["376"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00376-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,8]]},"assertion":[{"value":"28 February 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 May 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 June 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}