nach oben

Journal of Automated Reasoning

Erschienen in:

30.11.2017

System-Level Non-interference of Constant-Time Cryptography. Part I: Model

verfasst von: Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna

Erschienen in: Journal of Automated Reasoning | Ausgabe 1/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

This work focuses on the study of constant-time implementations; giving formal guarantees that such implementations are protected against cache-based timing attacks in virtualized platforms where their supporting operating system executes concurrently with other, potentially malicious, operating systems. We develop a model of virtualization that accounts for virtual addresses, physical and machine addresses, memory mappings, page tables, translation lookaside buffer, and cache; and provides an operational semantics for a representative set of actions, including reads and writes, allocation and deallocation, context switching, and hypercalls. We prove a non-interference result on the model that shows that an adversary cannot discover secret information using cache side-channels, from a constant-time victim.

Nächster Artikel Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nur mit Berechtigung zugänglich

The formal development is available at http://www.fing.edu.uy/inco/grupos/gsi/proyectos/VirtualCert/COQ/Model/constant-time_model.tar.gz, and can be verified using Coq .

Some modern processors now use a hierarchy of execution modes. Specifically, with the increased popularity of virtualization technologies, new modes have been added in order to more easily support hardware assisted virtualization. Examples include ARM virtualization extensions [81], Intel Vanderpool [80], AMD Pacifica [5], and more recently, Intel SGX [61].

Abramson, D., Jackson, J., Muthrasanallur, S., Neiger, G., Regnier, G., Sankaran, R., Schoinas, I., Uhlig, R., Vembu, B., Wiegert, J.: Intel virtualization technology for directed I/O. Intel Technol. J. 10(3), 179–192 (2006)CrossRef

Aciiçmez, O., Koç, Ç.: Trace-driven cache attacks on AES (short paper). In: 8th International Conference on Information and Communications Security (ICICS 2006), LNCS, vol. 4307, pp. 112–121. Springer (2006)

Aciiçmez, O., Schindler, W.: A vulnerability in RSA implementations due to instruction cache analysis and its demonstration on OpenSSL. In: CT-RSA’08, LNCS, vol. 4964, pp. 256–273. Springer (2008)

Alkassar, E., Cohen, E., Hillebrand, M., Kovalev, M., Paul, W.: Verifying shadow page table algorithms. In: Bloem, R., Sharygina, N. (eds.) Formal Methods in Computer-Aided Design, 10th International Conference (FMCAD’10). IEEE CS (2010)

AMD:AMD64 Virtualization Codenamed “Pacifica” Technology: Secure Virtual Machine Architecture Reference Manual. Publication no. 33047 Revision 3.0.1. May (2005)

Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: Berbers, Y., Zwaenepoel, W. (eds.) EuroSys, pp. 73–85. ACM, New York (2006)CrossRef

Barham, P., Dragovic, B., Fraser, K., Hand, S., Harris, T., Ho, A., Neugebauer, R., Pratt, I., Warfield, A.: Xen and the art of virtualization. In: SOSP ’03: Proceedings of the nineteenth ACM Symposium on Operating Systems Principles, pp. 164–177. ACM Press, New York (2003). https://doi.org/10.1145/945445.945462

Barthe, G., Betarte, G., Campo, J., Luna, C.: Formally verifying isolation and availability in an idealized model of virtualization. In: FM 2011, pp. 231–245. Springer-Verlag (2011)

Barthe, G., Betarte, G., Campo, J., Luna, C.: Cache-leakage resilient OS isolation in an idealized model of virtualization. CSF 2012, 186–197 (2012)

10.

Barthe, G., Betarte, G., Campo, J., Luna, C., Pichardie, D.: System-level non-interference for constant-time cryptography. In: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS’14, pp. 1267–1279. ACM, New York (2014). https://doi.org/10.1145/2660267.2660283

11.

Barthe, G., Betarte, G., Campo, J.D., Chimento, J.M., Luna, C.: Formally verified implementation of an idealized model of virtualization. In: Matthes, R., Schubert, A. (eds.) 19th International Conference on Types for Proofs and Programs, TYPES 2013, April 22–26, 2013, Toulouse, France, LIPIcs, vol. 26, pp. 45–63. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013). https://doi.org/10.4230/LIPIcs.TYPES.2013.45

12.

Baumann, C., Blasum, H., Bormer, T., Tverdyshev, S.: Proving memory separation in a microkernel by code level verification. In: Steiner, W., Obermaisser, R. (eds.) First International Workshop on Architectures and Applications for Mixed-Criticality Systems (AMICS 2011). IEEE Computer Society, Newport Beach (2011)

13.

Becker, H., Crespo, J.M., Galowicz, J., Hensel, U., Hirai, Y., Kunz, C., Nakata, K., Sacchini, J.L., Tews, H., Tuerk, T.: Combining mechanized proofs and model-based testing in the formal analysis of a hypervisor. In: Fitzgerald, J.S., Heitmeyer, C.L., Gnesi, S., Philippou A. (eds.) FM 2016: Formal Methods: 21st International Symposium, Limassol, Cyprus, November 9–11, 2016, Proceedings, Lecture Notes in Computer Science, vol. 9995, pp. 69–84 (2016). https://doi.org/10.1007/978-3-319-48989-6_5

14.

Bernstein, D.J.: Cache-timing attacks on AES (2005). Available from author’s webpage

15.

Biham, E.: A fast new DES implementation in software. In: Biham, E. (ed.) Fast Software Encryption, Lecture Notes in Computer Science, pp. 260–272. Springer, Berlin (1997). https://doi.org/10.1007/BFb0052352

16.

Blanchard, A., Kosmatov, N., Lemerre, M., Loulergue, F.: A case study on formal verification of the anaxagoros hypervisor paging system with frama-c. In: Núñez, M., Güdemann, M. (eds.) Formal Methods for Industrial Critical Systems: 20th International Workshop, FMICS 2015, Oslo, Norway, June 22–23, 2015 Proceedings, Lecture Notes in Computer Science, pp. 15–30. Springer (2015). https://doi.org/10.1007/978-3-319-19458-5_2

17.

Chardin, T., Fouque, P.A., Leresteux, D.: Cache timing analysis of RC4. In: ACNS 2011, LNCS, vol. 6715, pp. 110–129 (2011)

18.

Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M.E., Zeldovich, N.: Using crash hoare logic for certifying the FSCQ file system. In: Miller, E.L., Hand, S. (eds.) Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, pp. 18–37. ACM, Monterey (2015). https://doi.org/10.1145/2815400.2815402

19.

Chlipala, A.: Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press, Cambridge (2013)CrossRefMATH

20.

Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010)CrossRef

21.

Cohen, E.: Validating the Microsoft hypervisor. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM ’06, LNCS, vol. 4085, pp. 81–181. Springer (2006). https://doi.org/10.1007/11813040_6

22.

Coppens, B., Verbauwhede, I., Bosschere, K.D., Sutter, B.D.: Practical mitigations for timing-based side-channel attacks on modern x86 processors. In: S&P 2009, pp. 45–60 (2009)

23.

Dahlin, M., Johnson, R., Krug, R.B., McCoyd, M., Young, W.D.: Toward the verification of a simple hypervisor. In: Hardin, D., Schmaltz, J. (eds.) Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3–4, 2011, EPTCS, vol. 70, pp. 28–45 (2011). https://doi.org/10.4204/EPTCS.70.3

24.

Dam, M., Guanciale, R., Khakpour, N., Nemati, H., Schwarz, O.: Formal verification of information flow security for a simple ARM-based separation kernel. CCS 2013, 223–234 (2013)

25.

Dam, M., Guanciale, R., Nemati, H.: Machine code verification of a tiny ARM hypervisor. In: Sadeghi, A., Armknecht, F., Seifert, J. (eds.) TrustED’13, Proceedings of the 2013 ACM Workshop on Trustworthy Embedded Devices, Co-located with CCS 2013, pp. 3–12. ACM, Berlin (2013). https://doi.org/10.1145/2517300.2517302

26.

Domnitser, L., Jaleel, A., Loew, J., Abu-Ghazaleh, N., Ponomarev, D.: Non-monopolizable caches: low-complexity mitigation of cache side channel attacks. ACM Trans. Archit. Code Optim. 8(4), 35:1–35:21 (2012). https://doi.org/10.1145/2086696.2086714 CrossRef

27.

Feng, X., Shao, Z., Guo, Y., Dong, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. J. Autom. Reason. 42(2–4), 301–347 (2009)CrossRefMATH

28.

Franklin, J., Chaki, S., Datta, A., McCune, J., Vasudevan, A.: Parametric verification of address space separation. In: Degano, P., Guttman J.: (eds.) Proceedings of POST’12, LNCS, vol. 7215. (2012)

29.

Franklin, J., Chaki, S., Datta, A., Seshadri, A.: Scalable parametric verification of secure systems: how to verify reference monitors without worrying about data structure size. In: IEEE Symposium on Security and Privacy, pp. 365–379. IEEE Computer Society (2010)

30.

Freitas, L., McDermott, J.P.: Formal methods for security in the xenon hypervisor. STTT 13(5), 463–489 (2011). https://doi.org/10.1007/s10009-011-0195-9 CrossRef

31.

Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11–20 (1982)

32.

Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: IEEE Symposium on Security and Privacy, pp. 75–87 (1984)

33.

Goldberg, R.P.: Survey of virtual machine research. IEEE Comput. Mag. 7, 34–45 (1974)CrossRef

34.

Gotsman, A., Yang, H.: Modular verification of preemptive OS kernels. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) ICFP, pp. 404–417. ACM, New York (2011)

35.

Greve, D., Wilding, M., Eet, W.M.V.: A separation kernel formal security policy. In: Proceedings of the Fourth International Workshop on the ACL2 Theorem Prover and its Applications (2003)

36.

Gu, R., Koenig, J., Ramananandro, T., Shao, Z., Wu, X.N., Weng, S., Zhang, H., Guo, Y.: Deep specifications and certified abstraction layers. In: Rajamani, S.K., Walker, D.: (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15–17, 2015, pp. 595–608. ACM (2015). https://doi.org/10.1145/2676726.2676975

37.

Gullasch, D., Bangerter, E., Krenn, S.: Cache games - bringing access-based cache attacks on AES to practice. In: S&P 2011, pp. 490–505 (2011)

38.

Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad apps: End-to-end security via automated full-system verification. In: 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14), pp. 165–181. USENIX Association, Broomfield, CO (2014). https://www.usenix.org/conference/osdi14/technical-sessions/presentation/hawblitzel

39.

Heitmeyer, C.L., Archer, M., Leonard, E.I., McLean, J.: Formal specification and verification of data separation in a separation kernel for an embedded system. In: Proceedings of the 13th ACM conference on Computer and Communications Security, CCS’06, pp. 346–355. ACM, NY (2006). https://doi.org/10.1145/1180405.1180448

40.

Hunt, G.C., Larus, J.R.: Singularity: rethinking the software stack. SIGOPS Oper. Syst. Rev. 41(2), 37–49 (2007)CrossRef

41.

Hwang, J.Y., Suh, S.B., Heo, S.K., Park, C.J., Ryu, J.M., Park, S.Y., Kim, C.R.: Xen on ARM: System virtualization using xen hypervisor for ARM-based secure mobile phones. In: 5th IEEE Consumer and Communications Networking Conference (2008)

42.

Irazoqui, G., Inci, M., Eisenbarth, T., Sunar, B.: Wait a minute! a fast, cross-VM attack on AES. In: Stavrou, A., Bos, H., Portokalidis, G.: (eds.) Research in Attacks, Intrusions and Defenses, Lecture Notes in Computer Science, vol. 8688, pp. 299–319. Springer International Publishing (2014). https://doi.org/10.1007/978-3-319-11379-1_15

43.

Irazoqui, G., Inci, M.S., Eisenbarth, T., Sunar, B.: Fine grain cross-VM attacks on Xen and VMware are possible! IACR Cryptology ePrint Archive 2014, 248 (2014). http://eprint.iacr.org/2014/248

44.

Käsper, E., Schwabe, P.: Faster and timing-attack resistant AES-GCM. In: Clavier, C., Gaj, K.: (eds.) CHES, Lecture Notes in Computer Science, vol. 5747, pp. 1–17. Springer (2009)

45.

Khakpour, N., Schwarz, O., Dam, M.: Machine assisted proof of armv7 instruction level isolation properties. In: Gonthier, G., Norrish, M.: (eds.) Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11–13, 2013, Proceedings, Lecture Notes in Computer Science, vol. 8307, pp. 276–291. Springer (2013). https://doi.org/10.1007/978-3-319-03545-1_18

46.

Klein, G.: Operating system verification: an overview. Sadhana 34(1), 27–69 (2009). https://doi.org/10.1007/s12046-009-0002-4 MathSciNetCrossRefMATH

47.

Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. Commun. ACM (CACM) 53(6), 107–115 (2010)CrossRef

48.

Klein, G., Andronick, J., Elphinstone, K., Murray, T.C., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2 (2014). https://doi.org/10.1145/2560537 CrossRef

49.

Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: SOSP 2009, pp. 207–220. ACM (2009)

50.

Kolanski, R.: Verification of programs in virtual memory using separation logic. Ph.D. thesis, University of New South Wales (2011)

51.

Kong, J., Aciiçmez, O., Seifert, J., Zhou, H.: Hardware-software integrated approaches to defend against software cache-based side channel attacks. In: 15th International Conference on High-Performance Computer Architecture (HPCA-15 2009), 14–18 February 2009, Raleigh, North Carolina, USA, pp. 393–404. IEEE Computer Society (2009). https://doi.org/10.1109/HPCA.2009.4798277

52.

Krohn, M.N., Tromer, E.: Noninterference for a practical DIFC-based operating system. In: IEEE Symposium on Security and Privacy, pp. 61–76. IEEE Computer Society (2009)

53.

Krohn, M.N., Yip, A., Brodsky, M.Z., Cliffer, N., Kaashoek, M.F., Kohler, E., Morris, R.: Information flow control for standard OS abstractions. In: Bressoud, T.C., Kaashoek, M.F.: (eds.) SOSP, pp. 321–334. ACM (2007)

54.

Leinenbach, D., Santen, T.: Verifying the Microsoft Hyper-V hypervisor with VCC. In: Cavalcanti, A., Dams, D.: (eds.) FM 2009, LNCS, vol. 5850, pp. 806–809. Springer (2009)

55.

Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: POPL 2006, pp. 42–54. ACM (2006)

56.

Mai, H., Pek, E., Xue, H., King, S.T., Madhusudan, P.: Verifying security invariants in expressos. In: Sarkar, V., Bodík, R.: (eds.) Architectural Support for Programming Languages and Operating Systems, ASPLOS ’13, Houston, TX, USA, March 16–20, 2013, pp. 293–304. ACM (2013). https://doi.org/10.1145/2451116.2451148

57.

Mantel, H.: A uniform framework for the formal specification and verification of information flow security. Ph.D. thesis, Universität des Saarlandes (2003)

58.

Martin, W., White, P., Taylor, F., Goldberg, A.: Formal construction of the mathematically analyzed separation kernel. In: The Fifteenth IEEE International Conference on Automated Software Engineering (2000)

59.

McDermott, J.P., Freitas, L.: A formal security policy for xenon. In: Shmatikov, V.: (ed.) Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering, FMSE 2008, Alexandria, VA, USA, October 27, 2008, pp. 43–52. ACM (2008). https://doi.org/10.1145/1456396.1456401

60.

McDermott, J.P., Kirby, J., Montrose, B.E., Johnson, T., Kang, M.H.: Re-engineering Xen internals for higher-assurance security. Inf. Secur. Tech. Rep. 13(1), 17–24 (2008). https://doi.org/10.1016/j.istr.2008.01.001 CrossRef

61.

McKeen, F., Alexandrovich, I., Berenzon, A., Rozas, C.V., Shafi, H., Shanbhogue, V., Savagaonkar, U.R.: Innovative instructions and software model for isolated execution. In: Proceedings of the 2Nd International Workshop on Hardware and Architectural Support for Security and Privacy, HASP ’13, pp. 10:1–10:1. ACM, New York (2013). https://doi.org/10.1145/2487726.2488368

62.

Micali, S., Reyzin, L.: Physically observable cryptography (extended abstract). TCC 2004, 278–296 (2004)MathSciNetMATH

63.

Morrisett, G., Tan, G., Tassarotti, J., Tristan, J., Gan, E.: Rocksalt: better, faster, stronger SFI for the x86. In: Vitek, J., Lin, H., Tip, F.: (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, Beijing, China, June 11–16, 2012, pp. 395–404. ACM (2012). https://doi.org/10.1145/2254064.2254111

64.

Murray, T., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., G., X., Klein, G.: seL4: From general purpose to a proof of information flow enforcement. In: S&P 2013, pp. 415–429 (2013)

65.

Oheimb, D.v.: Information flow control revisited: Noninfluence = Noninterference + Nonleakage. In: Samarati, P., Ryan, P., Gollmann, D., Molva, R.: (eds.) Computer Security—ESORICS 2004, LNCS, vol. 3193, pp. 225–243. Springer (2004)

66.

Oheimb, Dv, Lotz, V., Walter, G.: Analyzing SLE 88 memory management security using interacting state machines. Int. J. Inf. Secur. 4(3), 155–171 (2005)CrossRef

67.

Osvik, D., Shamir, A., Tromer, E.: Cache attacks and countermeasures: the case of AES. In: Pointcheval, D.: (ed.) Topics in Cryptology—CT-RSA 2006, Lecture Notes in Computer Science, vol. 3860, pp. 1–20. Springer, Berlin (2006). https://doi.org/10.1007/11605805_1

68.

Page, D.: Theoretical use of cache memory as a cryptanalytic side-channel. Technical Report CSTR-02-003, University of Bristol, Department of Computer Science (2002)

69.

Ristenpart, T., Tromer, E., Shacham, H., Savage, S.: Hey, you, get off of my cloud! Exploring information leakage in third-party compute clouds. In: CCS 2009, pp. 199–212. ACM Press (2009)

70.

Rosenblum, M., Garfinkel, T.: Virtual machine monitors: Current technology and future trends. Computer 38(5), 39–47 (2005). https://doi.org/10.1109/MC.2005.176 CrossRef

71.

Rushby, J.M.: Noninterference, Transitivity, and Channel-Control Security Policies. Technical Report CSL-92-02, SRI International (1992)

72.

Sewell, T., Winwood, S., Gammie, P., Murray, T., Andronick, J., Klein, G.: seL4 enforces integrity. In: ITP 2011. Nijmegen (2011)

73.

Shao, Z.: Certified software. Commun. ACM 53(12), 56–66 (2010)CrossRef

74.

Steinberg, U., Kauer, B.: NOVA: a microhypervisor-based secure virtualization architecture. In: Morin, C., Muller, G.: (eds.) European Conference on Computer Systems, Proceedings of the 5th European conference on Computer systems, EuroSys 2010, Paris, France, April 13–16, 2010, pp. 209–222. ACM (2010). https://doi.org/10.1145/1755913.1755935

75.

Tews, H., Völp, M., Weber, T.: Formal memory models for the verification of low-level operating-system code. J. Autom. Reason. 42(2–4), 189–227 (2009)CrossRefMATH

76.

Tews, H., Völp, M., Weber, T.: Formal memory models for the verification of low-level operating-system code. J. Autom. Reason. 42(2–4), 189–227 (2009). https://doi.org/10.1007/s10817-009-9122-0 CrossRefMATH

77.

Tiwari, M., Oberg, J., Li, X., Valamehr, J., Levin, T.E., Hardekopf, B., Kastner, R., Chong, F.T., Sherwood, T.: Crafting a usable microkernel, processor, and i/o system with strict and provable information flow security. In: Iyer, R., Yang, Q., González, A. (eds.) ISCA, pp. 189–200. ACM, New York (2011)

78.

Tromer, E., Osvik, D.A., Shamir, A.: Efficient cache attacks on AES, and countermeasures. J. Cryptol. 23(1), 37–71 (2010)MathSciNetCrossRefMATH

79.

Tsunoo, Y., Saito, T., Suzaki, T., Shigeri, M., Miyauchi, H.: Cryptanalysis of DES implemented on computers with cache. In: CHES 2003, LNCS, vol. 2779, pp. 62–76. Springer (2003)

80.

Uhlig, R., Neiger, G., Rodgers, D., Santoni, A.L., Martins, F.C.M., Anderson, A.V., Bennett, S.M., Kagi, A., Leung, F.H., Smith, L.: Intel virtualization technology. Computer 38(5), 48–56 (2005). https://doi.org/10.1109/MC.2005.163 CrossRef

81.

Varanasi, P., Heiser, G.: Hardware-supported virtualization on arm. In: Proceedings of the Second Asia-Pacific Workshop on Systems, APSys ’11, pp. 11:1–11:5. ACM, New York (2011). https://doi.org/10.1145/2103799.2103813

82.

Vasudevan, A., Chaki, S., Jia, L., McCune, J.M., Newsome, J., Datta, A.: Design, implementation and verification of an extensible and modular hypervisor framework. In: 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19–22, 2013, pp. 430–444. IEEE Computer Society (2013). https://doi.org/10.1109/SP.2013.36

83.

VMWare: Security considerations and disallowing inter-Virtual Machine Transparent Page Sharing. Technical Report, VMWARE (2015). http://kb.vmware.com/selfservice/search.do?cmd=displayKC&docType=kc&docTypeID=DT_KB_1_1&externalId=2080735. Accessed May 2015

84.

Wang, X., Lazar, D., Zeldovich, N., Chlipala, A., Tatlock, Z.: Jitk: A trustworthy in-kernel interpreter infrastructure. In: Flinn, J., Levy, H.: (eds.) 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI ’14, Broomfield, CO, USA, October 6–8, 2014, pp. 33–47. USENIX Association (2014). https://www.usenix.org/conference/osdi14/technical-sessions/presentation/wang_xi

85.

Wang, Z., Lee, R.B.: New cache designs for thwarting software cache-based side channel attacks. In: ISCA 2007, pp. 494–505. ACM (2007)

86.

Wang, Z., Lee, R.B.: A novel cache architecture with enhanced performance and security. In: 41st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO-41 2008), November 8–12, 2008, Lake Como, Italy, pp. 83–93. IEEE Computer Society (2008). https://doi.org/10.1109/MICRO.2008.4771781

87.

Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: Proceedings of PLDI’10, pp. 99–110. ACM (2010)

88.

Yarom, Y., Falkner, K.: FLUSH+RELOAD: A high resolution, low noise, L3 cache side-channel attack. In: Fu, K., Jung, J.: (eds.) Proceedings of the 23rd USENIX Security Symposium, San Diego, CA, USA, August 20–22, 2014, pp. 719–732. USENIX Association (2014). https://www.usenix.org/conference/usenixsecurity14/technical-sessions/presentation/yarom

89.

Zeldovich, N., Boyd-Wickizer, S., Kohler, E., Mazières, D.: Making information flow explicit in HiStar. In: OSDI, pp. 263–278. USENIX Association (2006)

90.

Zhao, Y.: Formal specification and verification of separation kernels: an overview. CoRR (2015). arxiv:1508.07066

91.

Yarom,Y., Genkin, D., Heninger, N.: CacheBleed: a timing attack on open SSL constant-time RSA. J. Cryptogr. Eng. 7(2), 99–112 (2017). https://doi.org/10.1007/s13389-017-0152-y

92.

Irazoqui, G., Eisenbarth, T., Sunar, B.: Cross processor cache attacks. In: X. Chen, X. Wang, X. Huang (eds.) Proceedings of the 11th ACM on Asia Conference on Computer and Communications Security, AsiaCCS 2016, Xi’an, China, May 30–June 3, pp. 353–364. ACM (2016). https://doi.org/10.1145/2897845.2897867

93.

Lipp, M., Gruss, D., Spreitzer, R., Maurice, C., Mangard, S.: Armageddon: Cache attacks on mobile devices. In: T. Holz, S. Savage (eds.) 25th USENIX Security Symposium, USENIX Security 16, Austin, TX, USA, August 10–12, pp. 549–564. USENIX Association (2016). https://www.usenix.org/conference/ usenixsecurity16/technical-sessions/presentation/lipp

94.

Gruss, D., Maurice, C., Wagner, K., Mangard, S.: Flush+flush: A fast and stealthy cache attack. In: J. Caballero, U. Zurutuza, R.J. Rodríguez (eds.) Detection of Intrusions and Malware, and Vulnerability Assessment - 13th International Conference, DIMVA 2016, San Sebastián, Spain, July 7–8, 2016, Proceedings, Lecture Notes in Computer Science, vol. 9721, pp. 279–299. Springer (2016). https://doi.org/10.1007/978-3-319-40667-1_14

Titel: System-Level Non-interference of Constant-Time Cryptography. Part I: Model
verfasst von: Gilles Barthe
Gustavo Betarte
Juan Diego Campo
Carlos Luna
Publikationsdatum: 30.11.2017
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 1/2019
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-017-9441-5

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"