Top

Published in:

2017 | OriginalPaper | Chapter

AVR Processors as a Platform for Language-Based Security

Authors : Florian Dewald, Heiko Mantel, Alexandra Weber

Published in: Computer Security – ESORICS 2017

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

AVR processors are widely used in embedded devices. Hence, it is crucial for the security of such devices that cryptography on AVR processors is implemented securely. Timing-side-channel vulnerabilities and other possibilities for information leakage pose serious dangers to the security of cryptographic implementations. In this article, we propose a framework for verifying that AVR assembly programs are free from such vulnerabilities. In the construction of our framework, we exploit specifics of the 8-bit AVR architecture to make the static analysis of timing behavior reliable. We prove the soundness of our analysis against a formalization of the official AVR instruction-set specification.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Per-Session Security: Password-Based Cryptography Revisited

next chapter A Better Composition Operator for Quantitative Information Flow Analyses

The addendum to this article and the tool SCF\(^{{\text {AVR}}}\) are available under

http://www.mais.informatik.tu-darmstadt.de/scf2017.html.

All crypto functions in \(\mu \)NaCl satisfy the assumption of a unique return instruction.

Acıiçmez, O., Koç, Ç.K., Seifert, J.-P.: Predicting secret keys via branch prediction. In: CT-RSA, pp. 225–242 (2007)

Agat, J.: Transforming out timing leaks. In: POPL, pp. 40–53 (2000)

Appel, A.W.: Modern Compiler Implementation in Java. Cambridge University Press, Cambridge (2002)CrossRefMATH

Atmel Corporation: Atmel ATmega2564RFR2/ATmega1284RFR2/ATmega644RFR2 Datasheet. Rev. 42073B-MCU Wireless-09/14 (2014)

Atmel Corporation: Atmel ATmega640/V-1280/V-1281/V-2560/V-2561/V Datasheet. Rev. 2549Q-AVR-02/2014 (2014)

Atmel Corporation: Atmel AVR 8-bit Instruction Set: Instruction Set Manual. Rev. 0856K-AVR-05/2016 (2016)

Atmel Corporation: Automotive AVR Microcontrollers (2016). http://www.atmel.com/products/microcontrollers/avr/Automotive_AVR.aspx. Accessed 21 Mar 2017

Atmel Corporation: Rad Tolerant Devices (2016). http://www.atmel.com/products/rad-hard/rad-tolerant-devices/. Accessed 21 Mar 2017

Barthe, G., Betarte, G., Campo, J.D., Luna, C., Pichardie, D.: System-level Non-interference for Constant-time Cryptography. In: CCS, pp. 1267–1279 (2014)

10.

Barthe, G., Pichardie, D., Rezk, T.: A certified lightweight non-interference java bytecode verifier. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 125–140. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71316-6_10 CrossRef

11.

Barthe, G., Rezk, T., Warnier, M.: Preventing timing leaks through transactional branching instructions. ENTCS 153(2), 33–55 (2006)

12.

Bernstein, D.J.: Cache-timing attacks on AES. Technical report, University of Illinois at Chicago (2005)

13.

Bernstein, D.J.: The Salsa20 family of stream ciphers. In: Robshaw, M., Billet, O. (eds.) New Stream Cipher Designs. LNCS, vol. 4986, pp. 84–97. Springer, Heidelberg (2008). doi:10.1007/978-3-540-68351-3_8 CrossRef

14.

Bernstein, D.J.: Extending the Salsa20 nonce. In: SKEW (2011)

15.

Bernstein, D.J.: The Poly1305-AES message-authentication code. In: Gilbert, H., Handschuh, H. (eds.) FSE 2005. LNCS, vol. 3557, pp. 32–49. Springer, Heidelberg (2005). doi:10.1007/11502760_3 CrossRef

16.

Brumley, B.B., Tuveri, N.: Remote timing attacks are still practical. In: Atluri, V., Diaz, C. (eds.) ESORICS 2011. LNCS, vol. 6879, pp. 355–371. Springer, Heidelberg (2011). doi:10.1007/978-3-642-23822-2_20 CrossRef

17.

Brumley, D., Boneh, D.: Remote timing attacks are practical. Comput. Netw. 48(5), 701–716 (2005)CrossRef

18.

Cohen, E.S.: Information transmission in sequential programs. In: Foundations of Secure Computation, pp. 297–335. Academic Press(1978)

19.

Das Labor: AVR-Crypto-Lib (2014). http://avrcryptolib.das-labor.org/trac. Accessed 23 Mar 2017

20.

Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (1976)MathSciNetCrossRefMATH

21.

Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504–513 (1977)CrossRefMATH

22.

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

23.

Editors of the GCC Wiki: GCC Wiki page on avr-gcc: Calling Convention (2016). https://gcc.gnu.org/wiki/avr-gcc#Calling_Convention. Accessed 15 Apr 2017

24.

Fardan, N.J.A., Paterson, K.G.: Lucky thirteen: breaking the TLS and DTLS record protocols. In: S&P, pp. 526–540 (2013)

25.

Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM TOPLAS 9(3), 319–349 (1987)CrossRefMATH

26.

Goguen, J.A., Meseguer, J.: Security policies and security models. In: S&P, pp. 11–20 (1982)

27.

Hagberg, A.A., Schult, D.S., Swart, P.J.: Exploring network structure, dynamics, and function using NetworkX. In: SciPy, pp. 11–15 (2008)

28.

Hedin, D., Sands, D.: Timing aware information flow security for a javacard-like bytecode. ENTCS 141(1), 163–182 (2005)

29.

Hutter, M., Schwabe, P.: NaCl on 8-Bit AVR microcontrollers. In: Youssef, A., Nitaj, A., Hassanien, A.E. (eds.) AFRICACRYPT 2013. LNCS, vol. 7918, pp. 156–172. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38553-7_9 CrossRef

30.

Kizhvatov, I.: Side channel analysis of AVR XMEGA crypto engine. In: WESS, pp. 8:1–8:7 (2009)

31.

Kocher, P.C.: Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol. 1109, pp. 104–113. Springer, Heidelberg (1996). doi:10.1007/3-540-68697-5_9

32.

Kocher, P., Jaffe, J., Jun, B.: Differential power analysis. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 388–397. Springer, Heidelberg (1999). doi:10.1007/3-540-48405-1_25 CrossRef

33.

Köpf, B., Mantel, H.: Transformational typing and unification for automatically correcting insecure programs. Int. J. Inf. Sec. 6(2), 107–131 (2007)CrossRef

34.

Kucuk, G., Basaran, C.: Reducing energy dissipation of wireless sensor processors using silent-store-filtering MoteCache. In: Vounckx, J., Azemard, N., Maurine, P. (eds.) PATMOS 2006. LNCS, vol. 4148, pp. 256–266. Springer, Heidelberg (2006). doi:10.1007/11847083_25 CrossRef

35.

Liu, A., Ning, P.: TinyECC: a configurable library for elliptic curve cryptography in wireless sensor networks. In: IPSN, pp. 245–256 (2008)

36.

Liu, F., Yarom, Y., Ge, Q., Heiser, G., Lee, R.B.: Last-level cache side-channel attacks are practical. In: S&P, pp. 605–622 (2015)

37.

Lortz, S., Mantel, H., Starostin, A., Bähr, T., Schneider, D., Weber, A.: Cassandra: Towards a Certifying App. Store for Android. In: SPSM, pp. 93–104 (2014)

38.

Lux, A., Starostin, A.: A tool for static detection of timing channels in java. J. Crypt. Eng. 1(4), 303–313 (2011)CrossRef

39.

Mantel, H.: Information flow and noninterference. In: van Tilborg, H.C.A. Jajodia, S. (eds.) Encyclopedia of Cryptography and Security, 2nd edn. pp. 605–607. Springer, Heidelberg (2011)

40.

Mantel, H., Starostin, A.: Transforming out timing leaks, more or less. In: Pernul, G., Ryan, P.Y.A., Weippl, E. (eds.) ESORICS 2015. LNCS, vol. 9326, pp. 447–467. Springer, Cham (2015). doi:10.1007/978-3-319-24174-6_23 CrossRef

41.

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). doi:10.1007/11734727_14 CrossRef

42.

O’Flynn, C., Chen, Z.: ChipWhisperer: an open-source platform for hardware embedded security research. In: COSADE, pp. 243–260 (2014)

43.

O’Flynn, C., Chen, Z.: Power analysis attacks against IEEE 802.15.4 Nodes. In: COSADE, pp. 55–70 (2016)

44.

Page, D.: Theoretical use of cache memory as a cryptanalytic side-channel. IACR Cryptol. ePrint Arch. 2002(169), 1–23 (2002)

45.

Pastrana, S., Tapiador, J., Suarez-Tangil, G., Peris-López, P.: AVRAND: a software-based defense against code reuse attacks for AVR embedded devices. In: Caballero, J., Zurutuza, U., Rodríguez, R.J. (eds.) DIMVA 2016. LNCS, vol. 9721, pp. 58–77. Springer, Cham (2016). doi:10.1007/978-3-319-40667-1_4

46.

Prosser, R.T.: Applications of Boolean matrices to the analysis of flow diagrams. In: EJCC, pp. 133–138 (1959)

47.

Ronen, E., O’Flynn, C., Shamir, A., Weingarten, A.O.: IoT goes nuclear: creating a zigbee chain reaction. In: S&P, pp. 195–212 (2017)

48.

Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)CrossRef

49.

Volpano, D., Smith, G.: Eliminating covert flows with minimum typings. In: CSFW, pp. 156–168 (1997)

50.

Zhang, D., Askarov, A., Myers, A.C.: Language-based control and mitigation of timing channels. In: PLDI, pp. 99–109 (2012)

51.

Zhang, D., Wang, Y., Suh, G.E., Myers, A.C.: A hardware design language for timing-sensitive information-flow security. In: ASPLOS, pp. 503–516 (2015)

Title: AVR Processors as a Platform for Language-Based Security
Authors: Florian Dewald
Heiko Mantel
Alexandra Weber
Publisher: Springer International Publishing
Book: Computer Security – ESORICS 2017
Print ISBN: 978-3-319-66401-9

Electronic ISBN: 978-3-319-66402-6

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-66402-6_25

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner