Advertisement

Verifying Branch-Free Assembly Code in Why3

  • Marc SchooldermanEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10712)

Abstract

This paper discusses an approach to verification of assembly code using the Why3 platform. As a case study, we prove the functional correctness of hand-optimized routines for multiplying multiprecision integers on 8-bit microcontrollers which use an efficient version of Karatsuba’s algorithm. We find that by carefully constructing an underspecified model of an instruction set architecture in Why3, and specifying a few simple lemmas, verification can succeed using a high degree of automation in a short amount of time. Furthermore, our approach is sensitive to subtle memory aliasing issues, demonstrating that formal verification of security-critical assembly code is not only feasible, but also effective.

Keywords

Why3 Assembly language Karatsuba multiplication 

Notes

Acknowledgement

This work is part of the research programme ‘Sovereign’ with project number 14319 which is (partly) financed by the Netherlands Organisation for Scientific Research (NWO).

References

  1. 1.
    Atmel Corporation: AVR Instruction Set Manual, revision 0856L (2016)Google Scholar
  2. 2.
    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 2014, pp. 1267–1279. ACM, New York (2014)Google Scholar
  3. 3.
    Bernstein, D.J.: qhasm: tools to help write high-speed software. http://cr.yp.to/qhasm.html. Accessed 01 Dec 2016
  4. 4.
    Brumley, B.B., Barbosa, M., Page, D., Vercauteren, F.: Practical realisation and elimination of an ECC-related software bug attack. In: Dunkelman, O. (ed.) CT-RSA 2012. LNCS, vol. 7178, pp. 171–186. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-27954-6_11 CrossRefGoogle Scholar
  5. 5.
    Chen, Y.F., Hsu, C.H., Lin, H.H., Schwabe, P., Tsai, M.H., Wang, B.Y., Yang, B.Y., Yang, S.Y.: Verifying Curve25519 software. In: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS 2014, pp. 299–309. ACM (2014)Google Scholar
  6. 6.
    Düll, M., Haase, B., Hinterwälder, G., Hutter, M., Paar, C., Sánchez, A.H., Schwabe, P.: High-speed Curve25519 on 8-bit, 16-bit, and 32-bit microcontrollers. Des. Codes Crypt. 77(2–3), 493–514 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Filliâtre, J.-C., Gondelman, L., Paskevich, A.: The spirit of ghost code. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 1–16. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-08867-9_1 Google Scholar
  8. 8.
    Filliâtre, J.-C., Paskevich, A.: Why3 — Where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-37036-6_8 CrossRefGoogle Scholar
  9. 9.
    Hutter, M., Schwabe, P.: Multiprecision multiplication on AVR revisited. J. Cryptographic Eng. 5(3), 201–214 (2015)CrossRefGoogle Scholar
  10. 10.
    Jackson, P., Schanda, F., Wallenburg, A.: Auditing user-provided axioms in software verification conditions. In: Pecheur, C., Dierkes, M. (eds.) FMICS 2013. LNCS, vol. 8187, pp. 154–168. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-41010-9_11 CrossRefGoogle Scholar
  11. 11.
    Kocher, P., Jaffe, J., Jun, B.: Differential power analysis. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 388–397. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48405-1_25 Google Scholar
  12. 12.
    Liu, Z., Seo, H., Großschädl, J., Kim, H.: Reverse product-scanning multiplication and squaring on 8-bit AVR processors. In: Hui, L.C.K., Qing, S.H., Shi, E., Yiu, S.M. (eds.) ICICS 2014. LNCS, vol. 8958, pp. 158–175. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21966-0_12 CrossRefGoogle Scholar
  13. 13.
    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 CrossRefGoogle Scholar
  14. 14.
    Pereira, M., de Sousa, S.M.: Complexity checking of ARM programs, by deduction. In: Proceedings of the 29th Annual ACM Symposium on Applied Computing, SAC 2014, pp. 1309–1314. ACM, New York (2014)Google Scholar
  15. 15.
    Schwabe, P., Schmaltz, J.: Verification of optimised 48-bit multiplications on AVR. Radboud University, Technical report (2015)Google Scholar
  16. 16.
    Yu, Y.: Automated proofs of object code for a widely used microprocessor. University of Texas at Austin, Austin, TX, USA, Technical report (1993)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Radboud UniversityNijmegenThe Netherlands

Personalised recommendations