Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Formal Methods

FM 2019: Formal Methods – The Next 30 Years pp 539–555Cite as

Value-Dependent Information-Flow Security on Weak Memory Models

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11800))

Abstract

Weak memory models implemented on modern multicore processors are known to affect the correctness of concurrent code. They can also affect whether or not it is secure. This is particularly the case in programs where the security levels of variables are value-dependent, i.e., depend on the values of other variables. In this paper, we illustrate how instruction reordering allowed by contemporary multicore processors leads to vulnerabilities in such programs, and present a compositional, timing-sensitive information-flow logic which can be used to detect such vulnerabilities. The logic allows step-local reasoning (one instruction at a time) about a thread’s security by tracking information about dependencies between instructions which guarantee their order of occurrence. Program security can then be established from individual thread security using rely/guarantee reasoning.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    The recently discovered Meltdown [12], Spectre [11] and Foreshadow [4] vulnerabilities show that this is not strictly the case.

  2. 2.

    We will refer to this as simply ARMv8 in the remainder of this paper.

References

  1. Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F., Emmi, M.: Verifying constant-time implementations. In: Holz, T., Savage, S. (eds.) 25th USENIX Security Symposium, USENIX Security 16, pp. 53–70. USENIX Association (2016)

    Google Scholar 

  2. Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: Hermenegildo, M.V., Palsberg, J. (eds.) Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 7–18. ACM (2010)

    Google Scholar 

  3. Boehm, H.: 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 2012, pp. 12–20. ACM (2012)

    Google Scholar 

  4. Bulck, J.V., et al.: Foreshadow: extracting the keys to the Intel SGX kingdom with transient out-of-order execution. In: Enck, W., Felt, A.P. (eds.) 27th USENIX Security Symposium, USENIX Security 2018, pp. 991–1008. USENIX Association (2018)

    Google Scholar 

  5. Chandy, K.M., Misra, J.: Asynchronous distributed simulation via a sequence of parallel computations. Commun. ACM 24(4), 198–206 (1981)

    Article  MathSciNet  Google Scholar 

  6. Colvin, R.J., Smith, G.: A high-level operational semantics for hardware weak memory models. CoRR, abs/1812.00996 (2018)

    Google Scholar 

  7. Colvin, R.J., Smith, G.: A wide-spectrum language for verification of programs on weak memory models. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 240–257. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-95582-7_14

    Chapter  Google Scholar 

  8. Fitzpatrick, J.: An interview with Steve Furber. Commun. ACM 54(5), 34–39 (2011)

    Article  Google Scholar 

  9. Flur, S., et al.: Modelling the ARMv8 architecture, operationally: concurrency and ISA. In: Bodík, R., Majumdar, R. (eds.), Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 608–621. ACM (2016)

    Google Scholar 

  10. Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)

    Google Scholar 

  11. Kocher, P., et al.: Spectre attacks: exploiting speculative execution. CoRR, abs/1801.01203 (2018)

    Google Scholar 

  12. Lipp, M., et al.: Meltdown: reading kernel memory from user space. In: Enck, W., Felt, A.P. (eds.) 27th USENIX Security Symposium, USENIX Security 2018, pp. 973–990. USENIX Association (2018)

    Google Scholar 

  13. Lourenço, L., Caires, L.: Dependent information flow types. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, pp. 317–328. ACM (2015)

    Google Scholar 

  14. Mantel, H., Perner, M., Sauer, J.: Noninterference under weak memory models. In: IEEE 27th Computer Security Foundations Symposium, CSF 2014, pp. 80–94. IEEE Computer Society (2014)

    Google Scholar 

  15. Mantel, H., Sands, D., Sudbrock, H.: Assumptions and guarantees for compositional noninterference. In: Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, pp. 218–232. IEEE Computer Society (2011)

    Google Scholar 

  16. Moir, M., Shavit, N.: Concurrent data structures. In: Mehta, D.P., Sahni, S. (eds.), Handbook of Data Structures and Applications. Chapman and Hall/CRC (2004)

    Google Scholar 

  17. Molnar, D., Piotrowski, M., Schultz, D., Wagner, D.: The program counter security model: automatic detection and removal of control-flow side channel attacks. In: Won, D.H., Kim, S. (eds.) ICISC 2005. LNCS, vol. 3935, pp. 156–168. Springer, Heidelberg (2006). https://doi.org/10.1007/11734727_14

    Chapter  MATH  Google Scholar 

  18. Murray, T.C.: 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–48. ACM (2015)

    Google Scholar 

  19. Murray, T.C., Sison, R., Engelhardt, K.: COVERN: a logic for compositional verification of information flow control. In: 2018 IEEE European Symposium on Security and Privacy, EuroS&P 2018, pp. 16–30. IEEE (2018)

    Google Scholar 

  20. Murray, T.C., Sison, R., Pierzchalski, E., Rizkallah, C.: Compositional verification and refinement of concurrent value-dependent noninterference. In: IEEE 29th Computer Security Foundations Symposium, CSF 2016, pp. 417–431. IEEE Computer Society (2016)

    Google Scholar 

  21. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

    Book  MATH  Google Scholar 

  22. Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S., Sewell, P.: Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. PACMPL 2(POPL), 19:1–19:29 (2018)

    Google Scholar 

  23. Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Hall, M.W., Padua, D.A. (eds.), Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 175–186. ACM (2011)

    Google Scholar 

  24. Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM 53(7), 89–97 (2010)

    Article  Google Scholar 

  25. Sorin, D.J., Hill, M.D., Wood, D.A.: A Primer on Memory Consistency and Cache Coherence. Synthesis Lectures on Computer Architecture. Morgan & Claypool Publishers, San Rafael (2011)

    Book  Google Scholar 

  26. Vaughan, J.A., Millstein, T.D.: Secure information flow for concurrent programs under Total Store Order. In: Chong, S. (ed), 25th IEEE Computer Security Foundations Symposium, CSF 2012, pp. 19–29. IEEE Computer Society (2012)

    Google Scholar 

  27. Zheng, L., Myers, A.C.: Dynamic security labels and static information flow control. Int. J. Inf. Sec. 6(2–3), 67–84 (2007)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Defence Science and Technology Group, Brisbane, Australia

    Graeme Smith

  2. School of Information Technology and Electrical Engineering, The University of Queensland, Brisbane, Australia

    Graeme Smith & Nicholas Coughlin

  3. School of Computing and Information Systems, The University of Melbourne, Melbourne, Australia

    Toby Murray

Authors
  1. Graeme Smith
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nicholas Coughlin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Toby Murray
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Graeme Smith .

Editor information

Editors and Affiliations

  1. Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. Macquarie University, Sydney, NSW, Australia

    Annabelle McIver

  3. University of Minho, Braga, Portugal

    José N. Oliveira

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Commonwealth of Australia

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Smith, G., Coughlin, N., Murray, T. (2019). Value-Dependent Information-Flow Security on Weak Memory Models. In: ter Beek, M., McIver, A., Oliveira, J. (eds) Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science(), vol 11800. Springer, Cham. https://doi.org/10.1007/978-3-030-30942-8_32

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30942-8_32

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30941-1

  • Online ISBN: 978-3-030-30942-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation