Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Accelerated AES and SHA2 implementations #878

Merged
merged 12 commits into from
Sep 21, 2020
Merged

Accelerated AES and SHA2 implementations #878

merged 12 commits into from
Sep 21, 2020

Conversation

robdockins
Copy link
Contributor

This is a bit of a work in progress, but the initial results are promising. Even a fairly naive Haskell implementation runs about 100x faster than interpreting a reference implementation.

Some questions:

  1. What underlying implementation(s) should we use? This one was simply the most convenient to get going.
  2. What should we do about the symbolic simulator(s)? I'm inclined to find a way to use either defined or uninterpreted functions, provided the underlying solver supports them, but it's a bit tricky to do generically.

@robdockins robdockins changed the title Accelerated SHA2 implementations Accelerated AES and SHA2 implementations Sep 15, 2020
@robdockins
Copy link
Contributor Author

@weaversa, I'm interested in your thoughts regarding the Cryptol API exposed via the new SuiteB module. Should there be additions or changes with respect to AES and SHA? Is there any appetite for, e.g., the other SHA512 variants?

@robdockins robdockins marked this pull request as ready for review September 17, 2020 17:45
@robdockins
Copy link
Contributor Author

This branch now contains built-in implementations of the following primitives: AES-128, AES-192, AES-256, SHA-224, SHA-256, SHA-384, and SHA-512. They pass a battery of test vectors taken from the NIST Cryptographic algorithm validation program website (https://csrc.nist.gov/projects/cryptographic-algorithm-validation-program), and agree with the reference implementations on randomly selected tests, so I'm reasonably confident they are correct. These implementations run about 100x faster than directly interpreting the reference implementations. At a later time, we may wish to replace these primitives with higher performance versions, and/or verified implementations.

Currently, these primitives are not implemented in the symbolic backends. Attempts to call :sat or :prove will result in an "unimplemented primitive" error message. I consider this acceptable for the time being, until we figure out what we want to do.

atomb
atomb approved these changes Sep 18, 2020
View reviewed changes
Copy link
Contributor

@atomb atomb left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this all looks good as it is, but it makes me think of two meta topics.

First, we have :dumptests command, and I wonder whether we should have some sort of way of reading and running tests in the same format. That would allow the AES and SHA test vectors to be purely declarative, rather than being interspersed with code.

Second, as of recently we now depend on the cryptonite library for part of the RPC API. Would it make sense, given that, to use it for these crypto primitives? Does it expose a useful API? I'm not sure it's worth the effort to change, given that we'll eventually be swapping in C code, but I thought I might as well mention it.

@robdockins
Copy link
Contributor Author

I haven't looked much at the :dumptests format, but that might be a good idea... I'm not really sure.

As to cryptonite, it seems to have the same problem a lot of the C libraries I looked at for this purpose have; which is that they really want to package up programmer-oriented APIs for larger schemes/modes, whereas we want pretty low-level access to the raw crypto primitives. The SHA algorithms, in particular, are all seem to be byte-oriented, whereas we want to expose (or be able to expose) the bit-oriented versions.

@atomb
Copy link
Contributor

atomb commented Sep 21, 2020

Ah, yeah, I guess it makes sense that cryptonite doesn't expose the low-level interface. Anyway, those are both future questions. Let this be merged!

@robdockins
Add a Haskell-native implementation of the SHA256 and SHA512
44dae69 
block functions, ripped out of the SHA package, and expose
it via new Cryptol primitives.

Using these primitives in place of the defined reference implementations
leads to approx 100x speed-up in larger protocols that do a lot of hashing.

I don't know if this is the implementation we'll actually end up using,
but this verifies the overall idea and helps design the API.
@robdockins
Rearrange the new SHA primitives into a separate built-in module
65090ac 
named `SuiteB`, and finish packaging up the primitives.
@robdockins
Remove the restrictions on message length in the SuiteB::sha*
cc63eb5 
implementations.  Not sure this is actually a good idea, but
propigating the constraints around in larger algorithms is
very inconvenient.
@robdockins
Separate the public API for SuiteB from the implementation details.
4494c43
@robdockins
Add a basic implementation of AES to the SuiteB module.
e8f7fa9 
This implementation is taken fairly directly from the SBV
tutorial module.  It is a Word32-oriented implementation using
TBoxes.  We make the implementation avalible via Cryptol primitives
that are similar to the AESNI instructions, with primitives for
the individual rounds and some utility primitives for performing
key expansion.
@robdockins
Cut down the AES implementation to just the primivite bits we need.
ad9e479 
Expand the lookup tables manually and remove the basic GF(2^8)
polynomial arithmetic algorithms.

Rename the SHA primitives.
@robdockins
Add docstrings to the SuiteB module
6ab3262
@robdockins
Whitespace: untabify
9125366
@robdockins
More precicely express the constraints on AES key expansion.
1262fcf
@robdockins
Add a battery of test vectors to test the primitive AES implementations.
00f4a02 
These are taken from the AESAVS document and associated sample test vectors,
which may be found here:
https://csrc.nist.gov/Projects/cryptographic-algorithm-validation-program/Block-Ciphers
@robdockins
Move the AES test vectors into a new suiteb test directory,
dcfae1a 
and add a battery of SHA test vectors as well.
@robdockins
Add a quick-test mode to the cry shell script.
2581849 
This excludes the new SuiteB tests, and moves the `allexamples`
test into a separate directory that is also excluded.  The
standard `test` command still runs all tests.
@robdockins robdockins merged commit ae4406d into master Sep 21, 2020
@RyanGlScott RyanGlScott deleted the accel-sha2 branch March 22, 2024 14:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@atomb atomb atomb approved these changes

@brianhuffman brianhuffman Awaiting requested review from brianhuffman

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@robdockins @atomb