Addendum to "AVR Processors as a Platform for Language-Based Security"

This website is an addendum to the article

Florian Dewald, Heiko Mantel and Alexandra Weber. AVR Processors as a Platform for Language-Based Security. In Proceedings of the 22nd European Symposium on Research in Computer Security (ESORICS), pages 427-445, 2017.
BibTeX entry | PDF ]

The article presents a type system for checking AVR assembly programs against information leakage, including timing side channels. The type system is sound with respect to a timing-sensitive semantics of AVR assembly presented in the article. The type system is implemented in the tool Side-Channel FinderAVR (SCFAVR). The article also presents the tool and its evaluation on a case study from the cryptographic library muNaCl.

This website contains supplementary material for the article.

AVR-Semantics, Type System, and Soundness Proof

The full formalization of the type system from the article, the full soundness proof, and the operational semantics on which it is based are available in the addendum below.

Addendum to the Article


Side Channel FinderAVR (SCFAVR)

The tool SCFAVR (including the case study from the article) is available for download below.

 SCFAVR
A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang