Published in

Springer, Lecture Notes in Computer Science, p. 316-334, 2012

DOI: 10.1007/978-3-642-29320-7_21

Links

Tools

Export citation

Search in Google Scholar

Type checking cryptography implementations

Journal article published in 2012 by Manuel Barbosa, Andrew Moss, Dan Page, Nuno F. Rodrigues, Paulo F. Silva
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Red circle
Preprint: archiving forbidden
Orange circle
Postprint: archiving restricted
Upload
Red circle
Published version: archiving forbidden
Policy details
Data provided by SHERPA/RoMEO

Abstract

Proceedings da conferência Fundamentals of Software Engineering 2011 ; 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 specific 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 predefined sized vectors, matrices and bit strings, residue classes modulo an integer, finite fields and finite field extensions, allowing for extensive static validation of source code. We present the formalisation, validation and implementation of this type system.