IACR News item: 04 September 2013
Pablo Rauzy, Sylvain Guilley, Zakaria Najm
ePrint ReportThis failure is due to the fact that formal methods work with models rather than implementations.
Of course, we can use formal methods to prove non-functional security properties such as the absence of side-channel leakages.
But a common obstacle is that those properties are very low-level and appear incompatible with formalization.
To avoid the discrepancy between the model and the implementation, we apply formal methods directly on the implementation.
Doing so, we can formally prove that an assembly code is leak-free, provided that the hardware it runs on satisfies a finite (and limited) set of properties that we show are realistic.
We apply this technique to prove that a PRESENT implementation in 8~bit AVR assembly code is leak-free.
Additional news items may be found on the IACR news page.