Timing-Sensitive Information-Flow Analysis of AVR Assembly Programs 


A timing side channel leaks information during the execution of a program
by  variations in running time that depend on secret inputs. When a timing
side  channel is present in an implementation of a cryptographic mechanism,
used  secret encryption keys are in danger. 
This thesis introduces methods to analyze AVR assembly programs for the 
presence of timing side channels. The introduced methods include a timing- 
sensitive operational semantics, a timing-sensitive noninterference-like
security  property and a security type system that shall ensure the
accordance to our  security property. The introduced theory is implemented
into a tool we named  AVRTLC. We use AVRTLC to check the cryptographic
library μNaCl for the  presence of timing side channels. We can substantiate
the advertised security  of μNaCl against timing side channels.