Snapshots of the source-code for the following tools are available for download:
- CAO interpreter.
- CAOVerif deductive verification tool.
- CALF compiler.
- An Eclipse plug-in for CAO.
- An Eclipse plug-in for NaCl.
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 Veriﬁcation 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] di.uminho.pt).