For our first milestone, we are not attempting necessarily to build entire libraries, but only focus on the minimal dependent slice to cover SHA2.

Thanks to Andrew!

Write requirements for our V&V infrastructure.

Write generic C API that refines EBON language-neutral API.

Write an API design in EBON to reify core crypto domain model elements. This API will be refined to C and Java initially. First order behavioral specifications must be included.

Write an EBON domain model for the basic crypto and infrastructure concepts.

Write a (set of) feature model(s) that cover the variance in our domain model of crypto as well as our goals and requirements for the V&V infrastructure.

http://research.microsoft.com/en-us/downloads/29f9385d-da4c-479a-b2ea-2a7bb335d727/

source: https://github.com/vincenthz/hs-cryptohash (mostly C with some haskell)... I'm very interested in that :)

Note that this harness needs to not only drive two library calls, but also two executables or Cryptol interpreter vs. concrete implementation.

Choose analyses to run on each SHA implementation

Including, e.g., concolic test generation, fuzzing, symbol evaluation to generate tests a la PEX, etc.

https://boringssl.googlesource.com/boringssl/

Currently, for experimental work on designing the V&V infrastructure we are manually extracting and building specific crypto functions. In the longer term, we want to support an automated "full build" mode whereby we synchronize with remote code drops or repositories and perform full build and tests of others' libraries, publishing all of our V&V results for the whole community via our continuous integration (CI) system. This means that developers on all crypto libraries, or developers that use those libraries, would be able to assess the build state and quality of any library quickly and accurately by simply visiting our CI site.

After auditing a dozen or more crypto libraries we have found that the best library authors do in terms of testing/validation is to run a handful of published test vectors (e.g., NIST standard or submission vectors). So, while these vectors are hand-encoded into unit/system tests in dozens of libraries, and thus we can run the vectors by triggering test runs, we'd rather encode them once-and-for-all, abstractly, generically, in the library/language-neutral specification we are writing. Then, with appropriate automated tool support in our V&V infrastructure, we can automatically inject the vectors into all implementations. The first stage of this work is showing how to encode the vectors, so I'll take responsibility for that in our EBON system design (#1, #3, #5).

For our first milestone, we are not attempting necessarily to build entire libraries, but only focus on the minimal dependent slice to cover SHA2.

Aaron, this is for you to delegate, including back to us after a brief conversation about :modernize.

For our first milestone, we are not attempting necessarily to build entire libraries, but only focus on the minimal dependent slice to cover SHA2.

Pick one or both for current stage

Decide if they are similar enough, and decide exactly what we want for the first round.

This'll run the pairwise harness across all variants automagically.

Write generic Java API that refines EBON language-neutral API.

Compare this one with OpenSSL and see if it is close enough to be considered the same

As Joey and I have no experience with the code emitter in Cryptol version 1, perhaps this is something best done over lunch with you or someone else who has familiarity with that code base. We'd love to have SHA2 in C and JVM.

I will reuse the ESC/Java2 build infrastructure.

The vector generator's design will be part of the overall hacrypto design and will probably just be a bit of C that does deterministic and non-deterministic, possibly cached, streaming and finite bit vector length, random test vector generation.

http://www.libressl.org

https://code.google.com/p/crypto-js/

Extract SHA256 code from Sodium/NaCL, NSS, and OpenSSL (VST version?)