More Web Proxy on the site http://driver.im/

research-article

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

Authors:

William L. Harrison,

Adam M. Procter,

Gerard AllweinAuthors Info & Claims

RSP '16: Proceedings of the 27th International Symposium on Rapid System Prototyping: Shortening the Path from Specification to Prototype

Pages 114 - 120

https://doi.org/10.1145/2990299.2990318

Published: 01 October 2016 Publication History

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.

References

[1]

S. Peyton Jones, Ed., Haskell 98 Language and Libraries, the Revised Report. Cambridge University Press, 2003.

[2]

A. Procter, W. L. Harrison, I. Graves, M. Becchi, and G. Allwein, "Semantics driven hardware design, implementation, and verification with ReWire," in LCTES, 2015.

[3]

I. Graves, A. Procter, W. L. Harrison, M. Becchi, and G. Allwein, "Hardware synthesis from functional embedded domain-specific languages: A case study in regular expression compilation," in ARC, 2015, pp. 41--52.

[4]

I. Graves, A. M. Procter, W. L. Harrison, and G. Allwein, "Provably correct development of reconfigurable hardware designs via equational reasoning," in FPT, 2015, pp. 160--171.

[5]

W. L. Harrison, I. Graves, A. M. Procter, M. Becchi, and G. Allwein, "A programming model for reconfigurable computing based in functional concurrency," in ReCoSoC, 2016.

[6]

R. Chaves, G. Kuzmanov, L. Sousa, and S. Vassiliadis, "Improving SHA-2 hardware implementations," in 8th International Workshop on Cryptographic Hardware and Embedded Systems, 2006, pp. 298--310.

Digital Library

[7]

I. Algredo-Badillo, C. Feregrino-Uribe, R. Cumplido, and M. Morales-Sandoval, "FPGA-based implementation alternatives for the inner loop of the secure hash algorithm SHA-256," Microprocessors and Microsystems, vol. 37, no. 6--7, pp. 750--757, 2013.

Digital Library

[8]

K. K. Ting, S. C. L. Yuen, K. H. Lee, and P. H. W. Leong, "An FPGA based SHA-256 processor," in FPL, 2002, pp. 577--585.

Digital Library

[9]

R. P. McEvoy, F. M. Crowe, C. C. Murphy, and W. P. Marnane, "Optimisation of the SHA-2 family of hash functions on FPGAs," in ISVLSI, 2006, pp. 317--322.

Digital Library

[10]

N. Sklavos and O. Koufopavlou, "Implementation of the sha-2 hash family standard using fpgas," J. Supercomput., vol. 31, no. 3, pp. 227--248, Mar. 2005.

Digital Library

[11]

F. Kahri, H. Mestiri, B. Bouallegue, and M. Machhout, "Efficient FPGA hardware implementation of secure hash function SHA-256/Blake-256," in 12th International Multi-Conference on Systems, Signals Devices (SSD), March 2015, pp. 1--5.

[12]

"Secure Hash Standard (SHS)," Federal Information Processing Standards Publication FIPS Pub 180--2, Aug. 2002.

[13]

L. Erkök, M. Carlsson, and A. Wick, "Hardware/software co-verification of cryptographic algorithms using cryptol," in FMCAD, 2009, pp. 188--191.

[14]

A. W. Appel, "Verification of a cryptographic primitive: Sha-256," ACM Trans. Program. Lang. Syst., vol. 37, no. 2, pp. 7:1--7:31, Apr. 2015.

Digital Library

[15]

R. Bird and P. Wadler, Introduction to Functional Programming. Prentice Hall, 1988.

Digital Library

[16]

"Code repository for rsp16." {Online}. Available: https://goo.gl/xuGkja

[17]

S. Liang, P. Hudak, and M. Jones, "Monad transformers and modular interpreters," in 22nd ACM POPL, 1995, pp. 333--343.

Digital Library

[18]

T. Melham, Higher Order Logic and Hardware Verification. Cambridge Univ. Press, 1993.

Digital Library

Cited By

Wu RZhang XWang MWang L(2020)A High-Performance Parallel Hardware Architecture of SHA-256 Hash in ASIC2020 22nd International Conference on Advanced Communication Technology (ICACT)10.23919/ICACT48636.2020.9061457(1242-1247)Online publication date: Feb-2020
https://doi.org/10.23919/ICACT48636.2020.9061457
Zhang XWU RWang MWang L(2019)A High-Performance Parallel Computation Hardware Architecture in ASIC of SHA-256 Hash2019 21st International Conference on Advanced Communication Technology (ICACT)10.23919/ICACT.2019.8701906(52-55)Online publication date: Feb-2019
https://doi.org/10.23919/ICACT.2019.8701906
Reynolds TProcter AHarrison WAllwein G(2019)The Mechanized Marriage of Effects and Monads with Applications to High-assurance HardwareACM Transactions on Embedded Computing Systems10.1145/327428218:1(1-26)Online publication date: 8-Jan-2019
https://dl.acm.org/doi/10.1145/3274282
Show More Cited By

Index Terms

Model-driven design & synthesis of the SHA-256 cryptographic hash function in ReWire
1. Computer systems organization
  1. Embedded and cyber-physical systems
    1. Embedded systems
      1. Embedded hardware
2. Security and privacy
  1. Formal methods and theory of security
    1. Logic and verification

Recommendations

Hardware implementation analysis of SHA-256 and SHA-512 algorithms on FPGAs

Hash functions are common and important cryptographic primitives, which are very critical for data integrity assurance and data origin authentication security services. Field programmable gate arrays (FPGAs) being reconfigurable, flexible and physically ...
From software to accelerators with LegUp high-level synthesis
CASES '13: Proceedings of the 2013 International Conference on Compilers, Architectures and Synthesis for Embedded Systems

Embedded system designers can achieve energy and performance benefits by using dedicated hardware accelerators. However, implementing custom hardware accelerators for an application can be difficult and time intensive. LegUp is an open-source high-level ...
Design, synthesis and verification of a smart imaging core using SystemC

In this paper the development of a smart imaging core following a SystemC-based design flow is presented. The smart imaging core integrates an ARM processor and two specific hardware blocks for image processing: a smart imaging coprocessor and a motion ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

RSP '16: Proceedings of the 27th International Symposium on Rapid System Prototyping: Shortening the Path from Specification to Prototype

October 2016

141 pages

ISBN:9781450345354

DOI:10.1145/2990299

Program Chairs:
Kenneth Kent
University of New Brunswick, Canada
,
Sungjoo Yoo
Seoul National University, South Korea

Copyright © 2016 ACM.

Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of the United States government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems
SIGDA: ACM Special Interest Group on Design Automation
IEEE CAS
IEEE-RS: Reliability Society
IEEE CEDA
SIGMICRO: ACM Special Interest Group on Microarchitectural Research and Processing

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 October 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ESWEEK'16

Sponsor:

ESWEEK'16: TWELFTH EMBEDDED SYSTEM WEEK

October 1 - 7, 2016

Pennsylvania, Pittsburgh

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
90
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)3

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wu RZhang XWang MWang L(2020)A High-Performance Parallel Hardware Architecture of SHA-256 Hash in ASIC2020 22nd International Conference on Advanced Communication Technology (ICACT)10.23919/ICACT48636.2020.9061457(1242-1247)Online publication date: Feb-2020
https://doi.org/10.23919/ICACT48636.2020.9061457
Zhang XWU RWang MWang L(2019)A High-Performance Parallel Computation Hardware Architecture in ASIC of SHA-256 Hash2019 21st International Conference on Advanced Communication Technology (ICACT)10.23919/ICACT.2019.8701906(52-55)Online publication date: Feb-2019
https://doi.org/10.23919/ICACT.2019.8701906
Reynolds TProcter AHarrison WAllwein G(2019)The Mechanized Marriage of Effects and Monads with Applications to High-assurance HardwareACM Transactions on Embedded Computing Systems10.1145/327428218:1(1-26)Online publication date: 8-Jan-2019
https://dl.acm.org/doi/10.1145/3274282
Qiuyun XLigang HQiming LShuqin GJinhui W(2017)The Verification of SHA-256 IP using a semi-automatic UVM platform2017 13th IEEE International Conference on Electronic Measurement & Instruments (ICEMI)10.1109/ICEMI.2017.8265733(111-115)Online publication date: Oct-2017
https://doi.org/10.1109/ICEMI.2017.8265733

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents