A Tool-Chain for High-Assurance Cryptographic Software
- Citation:
- Almeida JB, Barbosa M, Pacheco H, Pereira V. 2016. A Tool-Chain for High-Assurance Cryptographic Software. ERCIM News. 2016
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.
Notes:
n/a
Citation Key:
DBLP:journals/ercim/AlmeidaBPP16Tags
- Coq (2)
- formalization (1)
- language closure (1)
- MEE-CBC (1)
- Pumping Lemma (2)
- s2n library (1)
- timing attacks (1)
Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.