Type checking cryptography implementations

Document type: Conference Papers
Peer reviewed: Yes
Full text:
Author(s): Manuel Barbosa, Andrew Moss, Dan Page, Nuno Rodrigues, Paulo Silva
Title: Type checking cryptography implementations
Journal: Lecture Notes in Computer Science
Conference name: 4th IPM International Conference on Fundamentals of Software Engineering, FSEN 2011
Year: 2012
Volume: 7141
Pagination: 316-334
ISSN: 0302-9743
Publisher: Springer
URI/DOI: 10.1007/978-3-642-29320-7_21
Organization: Blekinge Institute of Technology
Department: School of Computing (Sektionen för datavetenskap och kommunikation)
School of Computing S-371 79 Karlskrona
+46 455 38 50 00
Language: English
Abstract: 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.
Subject: Software Engineering\General
Keywords: Bit-strings; Cryptographic software; Domain specific languages; Finite fields; Formalisation; Residue class; Security policy; Source codes; Type systems; Typechecking
Note: Conference site: Tehran