Skip to main content
SpringerLink
Log in
Book cover

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

VSTTE 2017: Verified Software. Theories, Tools, and Experiments pp 66–83Cite as

Verifying Branch-Free Assembly Code in Why3

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,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.

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.

    As this version was not included in [9], we implemented it ourselves.

References

  1. Atmel Corporation: AVR Instruction Set Manual, revision 0856L (2016)

    Google Scholar 

  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. Bernstein, D.J.: qhasm: tools to help write high-speed software. http://cr.yp.to/qhasm.html. Accessed 01 Dec 2016

  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

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Chapter  Google Scholar 

  9. Hutter, M., Schwabe, P.: Multiprecision multiplication on AVR revisited. J. Cryptographic Eng. 5(3), 201–214 (2015)

    Article  Google Scholar 

  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

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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. Schwabe, P., Schmaltz, J.: Verification of optimised 48-bit multiplications on AVR. Radboud University, Technical report (2015)

    Google Scholar 

  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 

Download references

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

Author information

Authors and Affiliations

  1. Radboud University, Nijmegen, The Netherlands

    Marc Schoolderman

Authors
  1. Marc Schoolderman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marc Schoolderman .

Editor information

Editors and Affiliations

  1. Paris-Sud University, Orsay, France

    Andrei Paskevich

  2. New York University, New York, New York, USA

    Thomas Wies

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Schoolderman, M. (2017). Verifying Branch-Free Assembly Code in Why3. In: Paskevich, A., Wies, T. (eds) Verified Software. Theories, Tools, and Experiments. VSTTE 2017. Lecture Notes in Computer Science(), vol 10712. Springer, Cham. https://doi.org/10.1007/978-3-319-72308-2_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-72308-2_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-72307-5

  • Online ISBN: 978-3-319-72308-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation