Skip to main content

Type Checking Cryptography Implementations

Manuel Barbosa, Andrew Moss, Dan Page, Nuno Rodrigues, Paulo Silva., Type Checking Cryptography Implementations. Fundamentals of Software Engineering (FSEN), pp. 316–334. June 2011. No electronic version available.


Cryptographic software development is a challenging field: high performance must be achieved, while ensuring correctness and compliance with low-level security policies. CAO is a domain speci c language designed to assist development of cryptographic software. An important feature of this language is the design of a novel type system introducing native types such as predefi ned sized vectors, matrices and bit strings, residue classes modulo an integer, fi nite fields and fi nite fi eld extensions, allowing for extensive static validation of source code. We present the formalisation, validation and implementation of this type system.

Bibtex entry.

Contact details

Publication Admin