Dewald, FlorianFlorianDewaldMantel, HeikoHeikoMantelWeber, AlexandraAlexandraWeber2022-11-012022-11-012017-09Lecture Notes in Computer Science 10492 LNCS: 427-445 (2017)http://hdl.handle.net/11420/13858AVR 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.enInformatikConference Paper10.1007/978-3-319-66402-6_25Other