<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>17</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">José Bacelar Almeida</style></author><author><style face="normal" font="default" size="100%">Manuel Bernardo Barbosa</style></author><author><style face="normal" font="default" size="100%">Jorge Sousa Pinto</style></author><author><style face="normal" font="default" size="100%">Bárbara Vieira</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">Formal verification of side-channel countermeasures using self-composition</style></title><secondary-title><style face="normal" font="default" size="100%">Science Computer Programming</style></secondary-title></titles><keywords><keyword><style  face="normal" font="default" size="100%">Cryptographic algorithms</style></keyword><keyword><style  face="normal" font="default" size="100%">Program equivalence</style></keyword><keyword><style  face="normal" font="default" size="100%">Program verification</style></keyword><keyword><style  face="normal" font="default" size="100%">Self-composition</style></keyword><keyword><style  face="normal" font="default" size="100%">Side-channel countermeasures</style></keyword></keywords><dates><year><style  face="normal" font="default" size="100%">2013</style></year></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/jsp/files/11scp.pdf</style></url></related-urls></urls><number><style face="normal" font="default" size="100%">7</style></number><publisher><style face="normal" font="default" size="100%">Elsevier North-Holland, Inc.</style></publisher><pub-location><style face="normal" font="default" size="100%">Amsterdam, The Netherlands, The Netherlands</style></pub-location><volume><style face="normal" font="default" size="100%">78</style></volume><pages><style face="normal" font="default" size="100%">796–812</style></pages><language><style face="normal" font="default" size="100%">eng</style></language><abstract><style face="normal" font="default" size="100%">&lt;p&gt;Formal verification of cryptographic software implementations poses significant challenges for off-the-shelf tools. This is due to the domain-specific characteristics of the code, involving aggressive low-level optimizations and non-functional security requirements, namely the critical aspect of countermeasures against side-channel attacks. In this paper we extend previous results supporting the practicality of self-composition proofs of non-interference and generalisations thereof. We tackle the formal verification of high-level security policies adopted in the implementation of the recently proposed NaCl cryptographic library. We propose a formal verification framework to address these policies, extending the range of attacks that could previously be han- dled using self-composition. We demonstrate our techniques by addressing functional correctness and compliance with security policies for a practical use case.&lt;/p&gt;
</style></abstract><issue><style face="normal" font="default" size="100%">7</style></issue></record></records></xml>