Formally Proved Security of Assembly Code Against Power Analysis: A Case Study on Balanced Logic Blog Posting