Using Z3 Theorem on AVR Firmware

As many of you may or may not be aware of, I have a serious obsession with embedded systems security. It wasn’t until about two years ago where I started my journey of incorporating my knowledge in reverse engineering software applications into pulling apart firmware from embedded devices. Additionally, I also started learning hardware security concepts such as side-channel attacks, fault-injections/glitch attacks, bit flipping, and more.

Anyone who has began their careers in embedded security will tell you that the Arduino board is the best device to get started on. They…