A Tool-Chain for High-Assurance Cryptographic Software

Thumbnail Image
Date
2016
Authors
José Bacelar Almeida
Manuel Barbosa
Hugo Pereira Pacheco
Pereira,V
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Cryptography is an inherently interdisciplinary area and the development of high-quality cryptographic software is a time-consuming task drawing on skills from mathematics, computer science and electrical engineering, only achievable by highly skilled programmers. The challenge is to map high-level cryptographic specifications phrased using mathematical abstractions into efficient implementations at the level of C or assembly that can be deployed on a target computational platform, whilst adhering to the specification both in terms of correctness and security. The High Assurance Software Laboratory at INESC-TEC maintains a domain-specific toolchain for the specification, implementation and verification of cryptographic software centred on CAO, a cryptography analyses and operations-aware language.
Description
Keywords
Citation