This web-site is a place-holder for the latest snapshots of CACE Work Package 5 tools.

Snapshots of the source-code for the following tools are available for download:

The following papers are related to CACE WP5 activities.

B. Brumley, M. Barbosa, D. Page and F. Vercauteren.
Practical realisation and elimination of an ECC-related software bug attack.
Accepted for publication in CT-RSA 2012.
(Source code, including CAOVerif input and implementation of software bug attack can be found here).

J. Almeida, M. Barbosa, J. Pinto and B. Vieira.
Formal Verification of Side-Channel Countermeasures Using Self-Composition.
Accepted for publication in Science of Computer Programming.

M. Barbosa, A. Moss, D. Page, N. Rodrigues, P. Silva.
Type-Checking Cryptography Implementations.
Fundamentals of Software Engineering, FSEN 2011.
(Full version including and a detailed formalization of the implemented type checker and semantics for CAO interpreter can be found here.)

M. Barbosa, J. Pinto, J.-C. Filliâtre, B. Vieira.
A Deductive Verification Platform for Cryptographic Software.
International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010), ECEASST 33, 2010.

J. Almeida, M. Barbosa, J. Pinto, B. Vieira:
Deductive Verification of Cryptographic Software
NASA Journal of Innovations in Systems and Software Engineering, 6, 203-218, 2010.
(Sample code for some of the examples in the paper can be found here.)

J. Almeida, M. Barbosa, J. Pinto and B. Vieira:
Verifying Cryptographic Software Correctness with Respect to Reference Implementations
Formal Methods for Industrial and Critical Systems. 37-52, 2009.

J. B. Almeida, M. Barbosa, J. S. Pinto, B. Vieira:
Deductive Verification of Cryptographic Software
NASA Formal Methods Symposium 2009.

For further documentation please consult the CACE WP5 Deliverables published at the CACE Web-site.

Please send all comments, suggestions or bug reports to Manuel Barbosa (mbb [AT]