Advertisement

Value-Dependent Information-Flow Security on Weak Memory Models

  • Graeme SmithEmail author
  • Nicholas Coughlin
  • Toby Murray
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, 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.

References

  1. 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. 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. 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. 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. 5.
    Chandy, K.M., Misra, J.: Asynchronous distributed simulation via a sequence of parallel computations. Commun. ACM 24(4), 198–206 (1981)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Colvin, R.J., Smith, G.: A high-level operational semantics for hardware weak memory models. CoRR, abs/1812.00996 (2018)Google Scholar
  7. 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_14CrossRefGoogle Scholar
  8. 8.
    Fitzpatrick, J.: An interview with Steve Furber. Commun. ACM 54(5), 34–39 (2011)CrossRefGoogle Scholar
  9. 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. 10.
    Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)Google Scholar
  11. 11.
    Kocher, P., et al.: Spectre attacks: exploiting speculative execution. CoRR, abs/1801.01203 (2018)Google Scholar
  12. 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. 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. 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. 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. 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. 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_14CrossRefzbMATHGoogle Scholar
  18. 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. 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. 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. 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-9CrossRefzbMATHGoogle Scholar
  22. 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. 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. 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)CrossRefGoogle Scholar
  25. 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)CrossRefGoogle Scholar
  26. 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. 27.
    Zheng, L., Myers, A.C.: Dynamic security labels and static information flow control. Int. J. Inf. Sec. 6(2–3), 67–84 (2007)CrossRefGoogle Scholar

Copyright information

© Commonwealth of Australia 2019

Authors and Affiliations

  1. 1.Defence Science and Technology GroupBrisbaneAustralia
  2. 2.School of Information Technology and Electrical EngineeringThe University of QueenslandBrisbaneAustralia
  3. 3.School of Computing and Information SystemsThe University of MelbourneMelbourneAustralia

Personalised recommendations