<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>32</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">Vítor Pereira</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">A deductive verification tool for cryptographic software</style></title></titles><dates><year><style  face="normal" font="default" size="100%">2016</style></year><pub-dates><date><style  face="normal" font="default" size="100%">January</style></date></pub-dates></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/vm2p/files/vitor_pereira_dissertation.pdf</style></url></related-urls></urls><publisher><style face="normal" font="default" size="100%">Universidade do Minho-Escola de Engenharia</style></publisher><pub-location><style face="normal" font="default" size="100%">Braga, Portugal</style></pub-location><volume><style face="normal" font="default" size="100%">Master</style></volume><language><style face="normal" font="default" size="100%">eng</style></language><abstract><style face="normal" font="default" size="100%">&lt;p&gt;Security is notoriously diffcult to sell as a feature in software products. In addition to meeting a set&lt;br /&gt;
of security requirements, cryptographic software has to be cheap, fast, and use little resources. The&lt;br /&gt;
development of cryptographic software is an area with specific needs in terms of software development&lt;br /&gt;
processes and tools. In this thesis we explore how formal techniques, namely deductive verification&lt;br /&gt;
techniques, can be used to increase the guarantees that cryptographic software implementations indeed&lt;br /&gt;
work as prescribed.&lt;br /&gt;
CAO (C and OCCAM) is a programming language specific to the domain of Cryptography. Con-&lt;br /&gt;
trol structures are similar to C, but it incorporates data types that deal directly with the needs of a&lt;br /&gt;
programmer when translating specifications of cryptographic schemes (eg, from scientific papers or&lt;br /&gt;
standards) to the real world. CAO language is supported by a compiler and an interpreter developed&lt;br /&gt;
by HASLab, in a sequence of research and development projects.&lt;br /&gt;
The CAOVerif tool was designed to allow deductive verification programs written in CAO. This&lt;br /&gt;
tool follows the same paradigm as other tools available for high level programming languages, such&lt;br /&gt;
as Frama-C, according to which a CAO program annotated with a specification is converted in an&lt;br /&gt;
input program to the Jessie/Why3 tool-chain, where the specified properties are then analysed.&lt;br /&gt;
After the development of CAOVerif, a new tool, specific to the domain of Cryptography - named&lt;br /&gt;
EasyCrypt - was developed. The objective of this project is to evaluate EasyCrypt as a potential&lt;br /&gt;
backend for the CAOVerif tool, through the development of a prototype that demonstrates the advan-&lt;br /&gt;
tages and disadvantages of this solution.&lt;/p&gt;
</style></abstract><work-type><style face="normal" font="default" size="100%">Master dissertation-Master Degree in Computing Engineering</style></work-type><notes><style face="normal" font="default" size="100%">&lt;p&gt;n/a&lt;/p&gt;
</style></notes></record></records></xml>