Model-driven design & synthesis of the SHA-256 cryptographic hash function in rewire

William L. Harrison; Adam M. Procter; Gerard Allwein

doi:10.1145/2990299.2990318

Model-driven design & synthesis of the SHA-256 cryptographic hash function in rewire

William L. Harrison
, Adam M. Procter
, Gerard Allwein

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

5 Scopus citations

Abstract

There are many algorithms whose implementations can benefit both from hardware acceleration and formal verification and we would like to develop high assurance implementations as rapidly as possible. Critical computing infrastructure like cryptographic algorithms are prime candidates both for such acceleration and for formal verification. We show how to derive a verifiable, hardware-accelerated implementation of the SHA-256 cryptographic hash in the ReWire functional hardware description language in which the hardware-software partitioning of the implementation is reflected in the type system itself.

Original language	American English
Title of host publication	2016 International Symposium on Rapid System Prototyping (RSP)
Publisher	IEEE
Pages	1-7
Number of pages	7
ISBN (Print)	978-1-5090-3926-5
DOIs	https://doi.org/10.1145/2990299.2990318
State	Published - Oct 7 2016
Externally published	Yes
Event	2016 International Symposium on Rapid System Prototyping (RSP) - Pittsburgh, PA, USA Duration: Oct 6 2016 → Oct 7 2016

Conference

Conference	2016 International Symposium on Rapid System Prototyping (RSP)
Period	10/6/16 → 10/7/16

Keywords

Hardware
Semantics
Cryptography
Algorithm design and analysis
Software
Radiation detectors
Acceleration

Access to Document

10.1145/2990299.2990318

https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7909133

Cite this

@inproceedings{5f5ea2c7cc754dc2b47bc7ba02c16333,

title = "Model-driven design \& synthesis of the SHA-256 cryptographic hash function in rewire",

abstract = "There are many algorithms whose implementations can benefit both from hardware acceleration and formal verification and we would like to develop high assurance implementations as rapidly as possible. Critical computing infrastructure like cryptographic algorithms are prime candidates both for such acceleration and for formal verification. We show how to derive a verifiable, hardware-accelerated implementation of the SHA-256 cryptographic hash in the ReWire functional hardware description language in which the hardware-software partitioning of the implementation is reflected in the type system itself.",

keywords = "Hardware, Semantics, Cryptography, Algorithm design and analysis, Software, Radiation detectors, Acceleration",

author = "Harrison, \{William L.\} and Procter, \{Adam M.\} and Gerard Allwein",

year = "2016",

month = oct,

day = "7",

doi = "10.1145/2990299.2990318",

language = "American English",

isbn = "978-1-5090-3926-5",

pages = "1--7",

booktitle = "2016 International Symposium on Rapid System Prototyping (RSP)",

publisher = "IEEE",

note = "2016 International Symposium on Rapid System Prototyping (RSP) ; Conference date: 06-10-2016 Through 07-10-2016",

}

TY - GEN

T1 - Model-driven design & synthesis of the SHA-256 cryptographic hash function in rewire

AU - Harrison, William L.

AU - Procter, Adam M.

AU - Allwein, Gerard

PY - 2016/10/7

Y1 - 2016/10/7

N2 - There are many algorithms whose implementations can benefit both from hardware acceleration and formal verification and we would like to develop high assurance implementations as rapidly as possible. Critical computing infrastructure like cryptographic algorithms are prime candidates both for such acceleration and for formal verification. We show how to derive a verifiable, hardware-accelerated implementation of the SHA-256 cryptographic hash in the ReWire functional hardware description language in which the hardware-software partitioning of the implementation is reflected in the type system itself.

AB - There are many algorithms whose implementations can benefit both from hardware acceleration and formal verification and we would like to develop high assurance implementations as rapidly as possible. Critical computing infrastructure like cryptographic algorithms are prime candidates both for such acceleration and for formal verification. We show how to derive a verifiable, hardware-accelerated implementation of the SHA-256 cryptographic hash in the ReWire functional hardware description language in which the hardware-software partitioning of the implementation is reflected in the type system itself.

KW - Hardware

KW - Semantics

KW - Cryptography

KW - Algorithm design and analysis

KW - Software

KW - Radiation detectors

KW - Acceleration

UR - https://ieeexplore.ieee.org/document/7909133/

U2 - 10.1145/2990299.2990318

DO - 10.1145/2990299.2990318

M3 - Conference contribution

SN - 978-1-5090-3926-5

SP - 1

EP - 7

BT - 2016 International Symposium on Rapid System Prototyping (RSP)

PB - IEEE

T2 - 2016 International Symposium on Rapid System Prototyping (RSP)

Y2 - 6 October 2016 through 7 October 2016

ER -

Model-driven design & synthesis of the SHA-256 cryptographic hash function in rewire

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this