Skip to main content
SpringerLink
Log in
Book cover

Working Conference on Verified Software: Theories, Tools, and Experiments

VSTTE 2018: Verified Software. Theories, Tools, and Experiments pp 215–228Cite as

SideTrail: Verifying Time-Balancing of Cryptosystems

  • Conference paper
  • First Online:

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

Abstract

Timing-based side-channel attacks are a serious security risk for modern cryptosystems. The time-balancing countermeasure used by several TLS implementations (e.g. s2n, GnuTLS) ensures that execution timing is negligibly influenced by secrets, and hence no attacker-observable timing behavior depends on secrets. These implementations can be difficult to validate, since time-balancing countermeasures depend on global properties across multiple executions. In this work we introduce the tool SideTrail, which we use to prove the correctness of time-balancing countermeasures in s2n, the open-source TLS implementation used across a range of products from AWS, including S3. SideTrail is used in s2n’s continuous integration process, and has detected three side-channel issues that the s2n team confirmed and repaired before the affected code was deployed to production systems.

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.

    Using integer arithmetic provides performance benefits at the cost of losing information about the underlying C types. In a few cases, we needed to annotate back this information, for example by adding after an assignment to a .

  2. 2.

    https://github.com/danielsn/s2n/tree/sidetrail-vstte-artifact/tests/sidewinder.

References

  1. AlFardan, N.J., Paterson, K.G.: Lucky thirteen: breaking the TLS and DTLS record protocols. In: 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, 19–22 May 2013, pp. 526–540. IEEE Computer Society (2013)

    Google Scholar 

  2. Somorovsky, V.J.: Curious Padding oracle in OpenSSL (CVE-2016-2107) (2016). https://web-in-security.blogspot.co.uk/2016/05/curious-padding-oracle-in-openssl-cve.html. Accessed 15 Jan 2018

  3. Amazon Web Services: s2n : an implementation of the TLS/SSL protocols (2018). https://github.com/awslabs/s2n

  4. Dodds, J.: Part one: verifying s2n HMAC with SAW (2016). https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/. Accessed 15 Jan 2018

  5. Albrecht, M.R., Paterson, K.G.: Lucky microseconds: a timing attack on Amazon’s s2n implementation of TLS. In: Fischlin, M., Coron, J.-S. (eds.) EUROCRYPT 2016. LNCS, vol. 9665, pp. 622–643. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49890-3_24

    Chapter  Google Scholar 

  6. Sidewinder: Time-balanced Verification Tests (2018). https://github.com/awslabs/s2n/tree/master/tests/sidewinder

  7. Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006). https://doi.org/10.1007/11804192_17

    Chapter  Google Scholar 

  8. Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: 2004 Proceedings of 17th IEEE Computer Security Foundations Workshop, pp. 100–114. IEEE (2004)

    Google Scholar 

  9. Amazon Web Services: s2n Travis CI integration page (2018). https://travis-ci.org/awslabs/s2n/

  10. Agat, J.: Transforming out timing leaks. In: Wegman, M.N., Reps, T.W. (eds.) POPL 2000, Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, 19–21 January 2000, pp. 40–53. ACM (2000)

    Google Scholar 

  11. 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 

  12. Svenningsson, J., Sands, D.: Specification and verification of side channel declassification. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol. 5983, pp. 111–125. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12459-4_9

    Chapter  Google Scholar 

  13. Stefan, D., et al.: Eliminating cache-based timing attacks with instruction-based scheduling. In: Crampton, J., Jajodia, S., Mayes, K. (eds.) ESORICS 2013. LNCS, vol. 8134, pp. 718–735. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40203-6_40

    Chapter  Google Scholar 

  14. 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)

    Article  Google Scholar 

  15. Barthe, G., Betarte, G., Campo, J.D., Luna, C.D., Pichardie, D.: System-level non-interference for constant-time cryptography. In: Ahn, G., Yung, M., Li, N. (eds.) Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, 3–7 November 2014, pp. 1267–1279. ACM (2014)

    Google Scholar 

  16. Zhang, D., Wang, Y., Suh, G.E., Myers, A.C.: A hardware design language for timing-sensitive information-flow security. In: Özturk, Ö., Ebcioglu, K., Dwarkadas, S. (eds.) Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2015, Istanbul, Turkey, 14–18 March 2015, pp. 503–516. ACM (2015)

    Google Scholar 

  17. Doychev, G., Köpf, B., Mauborgne, L., Reineke, J.: Cacheaudit: a tool for the static analysis of cache side channels. ACM Trans. Inf. Syst. Secur. 18(1), 4:1–4:32 (2015)

    Article  Google Scholar 

  18. Rodrigues, B., Pereira, F.M.Q., Aranha, D.F.: Sparse representation of implicit flows with applications to side-channel detection. In Zaks, A., Hermenegildo, M.V. (eds.) Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, 12–18 March 2016, pp. 110–120. ACM (2016)

    Google Scholar 

  19. Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F., Emmi, M.: Verifying constant-time implementations. In: 25th USENIX Security Symposium, USENIX Security 16, Austin, TX, USA, 10–12 August 2016, pp. 53–70 (2016)

    Google Scholar 

  20. Blazy, S., Pichardie, D., Trieu, A.: Verifying constant-time implementations by abstract interpretation. In: Foley, S.N., Gollmann, D., Snekkenes, E. (eds.) ESORICS 2017. LNCS, vol. 10492, pp. 260–277. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66402-6_16

    Chapter  Google Scholar 

  21. Fang, X., Luo, P., Fei, Y., Leeser, M.: Leakage evaluation on power balance countermeasure against side-channel attack on FPGAs. In: 2015 IEEE High Performance Extreme Computing Conference, HPEC 2015, Waltham, MA, USA, 15–17 September 2015, pp. 1–6. IEEE (2015)

    Google Scholar 

  22. Bond, B., et al.: Vale: verifying high-performance cryptographic assembly code. In: 26th USENIX Security Symposium, USENIX Security 2017, Vancouver, BC, Canada, 16–18 August 2017, pp. 917–934 (2017)

    Google Scholar 

  23. Bhargavan, K., et al.: Everest: towards a verified, drop-in replacement of HTTPS. In: Lerner, B.S., Bodík, R., Krishnamurthi, S. (eds.) 2nd Summit on Advances in Programming Languages, SNAPL 2017, Volume 71 of LIPIcs., Asilomar, CA, USA, 7–10 May 2017, pp. 1:1–1:12. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)

    Google Scholar 

  24. Antonopoulos, T., Gazzillo, P., Hicks, M., Koskinen, E., Terauchi, T., Wei, S.: Decomposition instead of self-composition for proving the absence of timing channels. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pp. 362–375. ACM, New York (2017)

    Google Scholar 

  25. Chen, J., Feng, Y., Dillig, I.: Precise detection of side-channel vulnerabilities using quantitative Cartesian hoare logic. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, pp. 875–890. ACM, New York (2017)

    Google Scholar 

  26. 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

    Chapter  Google Scholar 

  27. Zaks, A., Pnueli, A.: CoVaC: compiler validation by program analysis of the cross-product. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 35–51. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68237-0_5

    Chapter  Google Scholar 

  28. Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200–214. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21437-0_17

    Chapter  Google Scholar 

  29. Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. Math. Struct. Comput. Sci. 21(6), 1207–1252 (2011)

    Article  MathSciNet  Google Scholar 

  30. Pasareanu, C.S., Phan, Q.S., Malacaria, P.: Multi-run side-channel analysis using symbolic execution and max-SMT. In: 2016 IEEE 29th Conference on Computer Security Foundations Symposium (CSF), pp. 387–400. IEEE (2016)

    Google Scholar 

  31. Crosby, S.A., Wallach, D.S., Riedi, R.H.: Opportunities and limits of remote timing attacks. ACM Trans. Inf. Syst. Secur. 12(3), 17:1–17:29 (2009)

    Article  Google Scholar 

  32. Bleichenbacher, D.: Chosen ciphertext attacks against protocols based on the RSA encryption standard PKCS #1. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol. 1462, pp. 1–12. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055716

    Chapter  Google Scholar 

  33. Brumley, D., Boneh, D.: Remote timing attacks are practical. In: Proceedings of the 12th Conference on USENIX Security Symposium, SSYM 2003, vol. 12, p. 1. USENIX Association, Berkeley (2003)

    Google Scholar 

  34. Rescorla, E., Dierks, T.: The Transport Layer Security (TLS) Protocol Version 1.2. RFC 5246, August 2008

    Google Scholar 

  35. Rakamarić, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 106–113. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_7

    Chapter  Google Scholar 

  36. LLVM: clang: a C language family frontend for LLVM (2018). https://clang.llvm.org/

  37. Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO 2004), Palo Alto, California, March 2004

    Google Scholar 

  38. Schmidt, S.: s2n is now handling 100 percent of SSL traffic for Amazon S3 (2017). https://aws.amazon.com/blogs/security/s2n-is-now-handling-100-percent-of-of-ssl-traffic-for-amazon-s3/. Accessed 15 Jan 2018

  39. Schmidt, S.: Introducing s2n, a new open source TLS implementation (2015). https://aws.amazon.com/blogs/security/introducing-s2n-a-new-open-source-tls-implementation/. Accessed 15 Jan 2018

  40. MacCarthaigh, C.: s2n and Lucky 13 (2015). https://aws.amazon.com/blogs/security/s2n-and-lucky-13/. Accessed 15 Jan 2018

  41. Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F.: Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC. In: Peyrin, T. (ed.) FSE 2016. LNCS, vol. 9783, pp. 163–184. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-52993-5_9

    Chapter  Google Scholar 

  42. Brad Conte: Basic implementations of standard cryptography algorithms, like AES and SHA-1 (2018). https://github.com/B-Con/crypto-algorithms. Commit: 02b66ec38b474445d10a5d1f0114bc0e8326707e

  43. Krawczyk, H., Bellare, M., Canetti, R.: HMAC: Keyed-Hashing for Message Authentication. RFC 2104, RFC Editor, February 1997. http://www.rfc-editor.org/rfc/rfc2104.txt

  44. Freier, A., Karlton, P., Kocher, P.: The Secure Sockets Layer (SSL) Protocol Version 3.0. RFC 6101, RFC Editor, August 2011. http://www.rfc-editor.org/rfc/rfc6101.txt

Download references

Author information

Authors and Affiliations

  1. Northeastern University, Boston, USA

    Konstantinos Athanasiou

  2. Amazon Web Services, Seattle, USA

    Byron Cook, Colm MacCarthaigh, Daniel Schwartz-Narbonne & Serdar Tasiran

  3. SRI International, Menlo Park, USA

    Michael Emmi

Authors
  1. Konstantinos Athanasiou
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Byron Cook
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michael Emmi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Colm MacCarthaigh
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Daniel Schwartz-Narbonne
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Serdar Tasiran
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Daniel Schwartz-Narbonne .

Editor information

Editors and Affiliations

  1. Yale University, New Haven, CT, USA

    Ruzica Piskac

  2. Uppsala University, Uppsala, Sweden

    Philipp Rümmer

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Athanasiou, K., Cook, B., Emmi, M., MacCarthaigh, C., Schwartz-Narbonne, D., Tasiran, S. (2018). SideTrail: Verifying Time-Balancing of Cryptosystems. In: Piskac, R., Rümmer, P. (eds) Verified Software. Theories, Tools, and Experiments. VSTTE 2018. Lecture Notes in Computer Science(), vol 11294. Springer, Cham. https://doi.org/10.1007/978-3-030-03592-1_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-03592-1_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-03591-4

  • Online ISBN: 978-3-030-03592-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation