Cryptography Implementations
Barbosa MB, Castro D, Silva P.
2014.
Compiling CAO: From Cryptographic Specifications to C Implementations. Principles of Security and Trust. 8414:240-244.
AbstractWe present a compiler for CAO, an imperative DSL for the cryptographic domain. The tool takes high-level cryptographic algorithm specifications and translates them into C implementations through a series of security-aware transformations and optimizations.
The compiler back-end is highly configurable, allowing the targeting of very disparate platforms in terms of memory requirements and computing power.
Barbosa MB, Moss A, Page D, Rodrigues N, Silva P.
2011.
Type Checking Cryptography Implementations. Fundamentals of Software Engineering - 4th IPM International Conference, FSEN 2011, Revised Selected Papers. 7141:316-334.
AbstractCryptographic 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.
Barbosa MB, Moss A, Page D, Rodrigues N, Silva P.
2011.
Type Checking Cryptography Implementations. AbstractCryptographic 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.
