×

Efficient information-flow verification under speculative execution. (English) Zbl 1437.68111

Chen, Yu-Fang (ed.) et al., Automated technology for verification and analysis. 17th international symposium, ATVA 2019, Taipei, Taiwan, October 28–31, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11781, 499-514 (2019).
Summary: We study the formal verification of information-flow properties in the presence of speculative execution and side-channels. First, we present a formal model of speculative execution semantics. This model can be parameterized by the depth of speculative execution and is amenable to a range of verification techniques. Second, we introduce a novel notion of information leakage under speculation, which is parameterized by the information that is available to an attacker through side-channels. Finally, we present one verification technique that uses our formalism and can be used to detect information leaks under speculation through cache side-channels, and can decide whether these are only possible under speculative execution. We implemented an instance of this verification technique that combines taint analysis and safety model checking. We evaluated this approach on a range of examples that have been proposed as benchmarks for mitigations of the Spectre vulnerability, and show that our approach correctly identifies all information leaks.
For the entire collection see [Zbl 1428.68012].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
94A60 Cryptography
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Agat, J.: Transforming out timing leaks. In: POPL, pp. 40-53. ACM (2000). https://doi.org/10.1145/325694.325702 · Zbl 1323.68399 · doi:10.1145/325694.325702
[2] Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F., Emmi, M.: Verifying constant-time implementations. In: USENIX Security, pp. 53-70. USENIX Association (2016). https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/almeida
[3] Almeida, J.B., Barbosa, M., Pinto, J.S., Vieira, B.: Formal verification of side-channel countermeasures using self-composition. Sci. Comput. Program. 78(7), 796-812 (2013). https://doi.org/10.1016/j.scico.2011.10.008 · Zbl 1284.68158 · doi:10.1016/j.scico.2011.10.008
[4] Arons, T., Pnueli, A.: A comparison of two verification methods for speculative instruction execution. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 487-502. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46419-0_33 · Zbl 0971.68576 · doi:10.1007/3-540-46419-0_33
[5] Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Computer Security Foundations Workshop, (CSFW-17), pp. 100-114 (2004)
[6] Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. Math. Struct. Comput. Sci. 21(6), 1207-1252 (2011). https://doi.org/10.1017/S0960129511000193 · Zbl 1252.68072 · doi:10.1017/S0960129511000193
[7] Bhattacharyya, A., et al.: Smotherspectre: exploiting speculative execution through port contention. CoRR abs/1903.01843 (2019). http://arxiv.org/abs/1903.01843
[8] Boudol, G., Petri, G.: A theory of speculative computation. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 165-184. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11957-6_10 · Zbl 1260.68086 · doi:10.1007/978-3-642-11957-6_10
[9] Canella, C., et al.: A systematic evaluation of transient execution attacks and defenses. CoRR. https://arxiv.org/abs/1811.05441 (2018)
[10] Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001) · doi:10.1016/B978-044450813-3/50026-6
[11] Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265-284. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54792-8_15 · doi:10.1007/978-3-642-54792-8_15
[12] Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504-513 (1977) · Zbl 0361.68033 · doi:10.1145/359636.359712
[13] Guarnieri, M., Köpf, B., Morales, J.F., Reineke, J., Sánchez, A.: SPECTECTOR: principled detection of speculative information flows. CoRR. http://arxiv.org/abs/1812.08639 (2018)
[14] Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343-361. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_20 · doi:10.1007/978-3-319-21690-4_20
[15] Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. Int. J. Inf. Secur. 8(6), 399-422 (2009) · doi:10.1007/s10207-009-0086-1
[16] Hosabettu, R., Gopalakrishnan, G., Srivas, M.: Verifying advanced microarchitectures that support speculation and exceptions. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 521-537. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_39 · Zbl 0974.68568 · doi:10.1007/10722167_39
[17] Intel: White paper: intel analysis of speculative execution side channels. Tech. Rep. 336983-001, Revision 1.0. https://newsroom.intel.com/wp-content/uploads/sites/11/2018/01/Intel-Analysis-of-Speculative-Execution-Side-Channels.pdf
[18] Intel: Q2 2018 speculative execution side channel update (2018). https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00115.html. Accessed May 2019
[19] Jhala, R., McMillan, K.L.: Microarchitecture verification by compositional model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 396-410. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44585-4_40 · Zbl 0991.68639 · doi:10.1007/3-540-44585-4_40
[20] Kiriansky, V., Waldspurger, C.: Speculative buffer overflows: attacks and defenses. CoRR. http://arxiv.org/abs/1807.03757 (2018)
[21] Kocher, P.: Spectre Mitigations in Microsoft’s C/C++ Compiler. https://www.paulkocher.com/doc/MicrosoftCompilerSpectreMitigation.html
[22] Kocher, P., et al.: Spectre attacks: exploiting speculative execution. CoRR. http://arxiv.org/abs/1801.01203 (2018)
[23] Lahiri, S.K., Bryant, R.E.: Deductive verification of advanced out-of-order microprocessors. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 341-354. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45069-6_33 · Zbl 1278.68180 · doi:10.1007/978-3-540-45069-6_33
[24] Maisuradze, G., Rossow, C.: ret2spec: speculative execution using return stack buffers. In: CCS, pp. 2109-2122. ACM (2018). https://doi.org/10.1145/3243734.3243761 · doi:10.1145/3243734.3243761
[25] Pardoe, A.: Spectre mitigations in MSVC (2018). https://blogs.msdn.microsoft.com/vcblog/2018/01/15/spectre-mitigations-in-msvc/. Accessed May 2019
[26] Pistoia, M., Flynn, R.J., Koved, L., Sreedhar, V.C.: Interprocedural analysis for privileged code placement and tainted variable detection. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 362-386. Springer, Heidelberg (2005). https://doi.org/10.1007/11531142_16 · doi:10.1007/11531142_16
[27] Rodrigues, B., Pereira, F.M.Q., Aranha, D.F.: Sparse representation of implicit flows with applications to side-channel detection. In: CC, pp. 110-120. ACM (2016). https://doi.org/10.1145/2892208.2892230 · doi:10.1145/2892208.2892230
[28] Sawada, J., Hunt, W.A.: Processor verification with precise exceptions and speculative execution. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 135-146. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028740 · doi:10.1007/BFb0028740
[29] Stecklina, J., Prescher, T.: Lazyfp: leaking FPU register state using microarchitectural side-channels. CoRR. http://arxiv.org/abs/1806.07480 (2018)
[30] Taram, M., Venkat, A., Tullsen, D.M.: Context-sensitive fencing: Securing speculative execution via microcode customization. In: ASPLOS, pp. 395-410. ACM (2019). https://doi.org/10.1145/3297858.3304060 · doi:10.1145/3297858.3304060
[31] Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352-367. Springer, Heidelberg (2005). https://doi.org/10.1007/11547662_24 · Zbl 1141.68380 · doi:10.1007/11547662_24
[32] Velev, M.N.: Formal verification of VLIW microprocessors with speculative execution. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 296-311. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_24 · Zbl 0974.68554 · doi:10.1007/10722167_24
[33] Wang, G., Chattopadhyay, S., Gotovchits, I., Mitra, T., Roychoudhury, A.: oo7: low-overhead defense against spectre attacks via binary analysis. CoRR. http://arxiv.org/abs/1807.05843 (2018)
[34] Yang, W. · Zbl 1511.68171 · doi:10.1007/978-3-319-96142-2_11
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.