×

System-level non-interference of constant-time cryptography. I: Model. (English) Zbl 1459.68026

Summary: 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.

MSC:

68M25 Computer security
94A60 Cryptography

Software:

ACL2; Coq; seL4; Rocksalt; VCC
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] 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) · doi:10.1535/itj.1003.02
[2] 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)
[3] 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) · Zbl 1153.94341
[4] 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)
[5] AMD:AMD64 Virtualization Codenamed “Pacifica” Technology: Secure Virtual Machine Architecture Reference Manual. Publication no. 33047 Revision 3.0.1. May (2005)
[6] Ball, T.; Bounimova, E.; Cook, B.; Levin, V.; Lichtenberg, J.; McGarvey, C.; Ondrusek, B.; Rajamani, SK; Ustuner, A.; Berbers, Y. (ed.); Zwaenepoel, W. (ed.), Thorough static analysis of device drivers, 73-85 (2006), New York · doi:10.1145/1217935.1217943
[7] 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
[8] 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)
[9] 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 · Zbl 1459.68027
[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 · Zbl 1359.68048
[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 · Zbl 1385.94014
[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) · Zbl 1288.68001 · doi:10.7551/mitpress/9153.001.0001
[20] Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157-1210 (2010) · doi:10.3233/JCS-2009-0393
[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 · doi:10.1145/2086696.2086714
[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) · Zbl 1191.68176 · doi:10.1007/s10817-009-9118-9
[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) · Zbl 1353.68177
[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 · doi:10.1007/s10009-011-0195-9
[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) · doi:10.1109/MC.1974.6323581
[34] Gotsman, A.; Yang, H.; Chakravarty, MMT (ed.); Hu, Z. (ed.); Danvy, O. (ed.), Modular verification of preemptive OS kernels, 404-417 (2011), New York · Zbl 1323.68195
[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 · Zbl 1345.68107
[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) · doi:10.1145/1243418.1243424
[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) · Zbl 1290.94102
[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 · Zbl 1426.68286
[46] Klein, G.: Operating system verification: an overview. Sadhana 34(1), 27-69 (2009). https://doi.org/10.1007/s12046-009-0002-4 · Zbl 1192.68432 · doi:10.1007/s12046-009-0002-4
[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) · doi:10.1145/1743546.1743574
[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 · doi:10.1145/2560537
[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) · Zbl 1369.68124
[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 · doi:10.1016/j.istr.2008.01.001
[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) · Zbl 1197.94197
[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) · doi:10.1007/s10207-004-0057-5
[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 · Zbl 1125.94326
[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 · doi:10.1109/MC.2005.176
[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) · Zbl 1342.68303
[73] Shao, Z.: Certified software. Commun. ACM 53(12), 56-66 (2010) · doi:10.1145/1859204.1859226
[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) · Zbl 1191.68178 · doi:10.1007/s10817-009-9122-0
[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 · Zbl 1191.68178 · doi:10.1007/s10817-009-9122-0
[77] Tiwari, M.; Oberg, J.; Li, X.; Valamehr, J.; Levin, TE; Hardekopf, B.; Kastner, R.; Chong, FT; Sherwood, T.; Iyer, R. (ed.); Yang, Q. (ed.); González, A. (ed.), Crafting a usable microkernel, processor, and i/o system with strict and provable information flow security, 189-200 (2011), New York
[78] Tromer, E., Osvik, D.A., Shamir, A.: Efficient cache attacks on AES, and countermeasures. J. Cryptol. 23(1), 37-71 (2010) · Zbl 1181.94106 · doi:10.1007/s00145-009-9049-y
[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 · doi:10.1109/MC.2005.163
[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
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.