/s2n

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.

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

SAW verification of HMAC #305

Merged
merged 161 commits into from Sep 7, 2016
+2,461 −2

Conversation

Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
5 participants
@jldodds @alexw91 @colmmacc @atomb @ntc2
@jldodds
Contributor

jldodds commented Sep 6, 2016

This pull request contains the following:

  1. A Cryptol specification of HMAC.
  2. A SAW-script proving s2n_hmac.c equivalent to the cryptol specification at a variety of hash functions, message sizes, and key sizes.
  3. Further saw tests to ensure SAW catches bugs. We do this by patching a copy of the s2n code to introduce bugs and then running SAW on the patched code to ensure the bugs are detected. The current tests include an incorrect constant and malicious code that behaves incorrectly only when a certain byte has a specific value.
  4. Integration of all SAW tests into the s2n build system, runnable by make saw at the s2n root directory. Prerequisites are SAW, Clang, and Z3
  5. An updated .travis.yaml file that will run SAW for the linux tests on travis. For an example run see here

atomb and others added some commits Mar 28, 2016

@atomb
Add README
a54ddd9
@atomb
Add rudimentary s2n Makefile 
This will clone the s2n source and build LLVM bitcode files of the appropriate
pieces.
0a6a18b
@atomb
Add specification of SHA1 
The includes the functional version of SHA1 that we had in the examples
directory of the Cryptol repository, as well as a more imperative
version (written in Cryptol) that consists of initialization, update,
and finalization functions. The SAWScript file proves that the
imperative version is equivalent to the functional version for various
specific message sizes.

It turns out that ABC is remarkably efficient at proving this! Probably
because the block function is completely identical on both sides of the
equality.

Note that I've included SHA1 simply as an example hash algorithm since
a clean specification of it was readily at hand. The same approach to
creating an imperative version should work equally well for any other
hash algorithm.
cb0ca75
@atomb
Add SHA256: both functional and imperative styles 
The two styles are proved equivalent for various sizes using ABC, as in
the SHA1 spec.
fd16ae5
@atomb
Create self-contained bitcode file for HMAC 
This contains everything needed for HMAC except the concrete hash
functions, which we're going to leave abstract anyway.
82731e4
@atomb
Add SAWScript file for SHA256 proofs 
These proofs show equivalence between the functional and imperative
versions of SHA256 (both in Cryptol) for several specific message sizes.
af8a740
@atomb
Add skeleton HMAC spec 
This includes a functional Cryptol spec of HMAC, as well as stubs for
the imperative version. It also includes stubs for the SAWScript
specifications of the C functions that abstract over specific hash
implementations in s2n.
45581a0
@atomb
More complete skeleton of s2n HMAC spec
9402e5a
@ntc2
Make `src/Makefile` work with a non OSX+Homebrew setup. 
But it should still work with OSX+Homebrew, too, although I couldn't
test it.
9457390
@atomb
First crack at imperative HMAC in Cryptol 
This version type checks and runs but isn't quite correct yet. Nathan is
going to take over from here.
335e910
@atomb
Prove SHA256 on a wider range of update sizes
33b58cd
@ntc2
Add imperative HMAC vs functional HMAC test. 
Turns out they are already equivalent:

    $ stack exec saw HMAC_imp_correct.saw
    Getting project config file from STACK_YAML environment
    Loading module Cryptol
    Loading file "HMAC_imp_correct.saw"
    Loading module SHA256
    Loading module HMAC
    Checking imp_correct for byte count 0
    Valid
    Time: 9.429029s
    Checking imp_correct for byte count 1
    Valid
    Time: 14.696618s
    Checking imp_correct for byte count 2
    Valid
    Time: 11.169244s
    Checking imp_correct for byte count 63
    Valid
    Time: 16.449585s
    Checking imp_correct for byte count 64
    Valid
    Time: 18.954719s
    Checking imp_correct for byte count 65
    Valid
    Time: 25.468452s
    Checking imp_correct for byte count 127
    Valid
    Time: 35.831754s
    Checking imp_correct for byte count 128
    Valid
    Time: 45.241426s
    Checking imp_correct for byte count 129
    Valid
    Time: 41.248373s
    Checking imp_correct for byte count 1000
    Valid
    Time: 257.975434s
    stack exec saw HMAC_imp_correct.saw  441.91s user 13.17s system 94% cpu 8:01.78 total
b53a0ab
@ntc2
Add `tmp/TAGS` target to `src/Makefile`. 
To generate Emacs tags for the s2n C sources.
bf83522
@ntc2
Make imperative HMAC closer to s2n. 
- Updated the `HMACState` to include all `s2n_hmac_state` fields except
  `alg`, which we've fixed to SHA256 for now.

- Modified the new fields in `hmac_init`, `hmac_update`, `hmac_reset`,
  and `hmac_digest`.

This Cryptol model still disagrees with s2n in a few places:

- the `outer` state coming out of `hmac_init` is not accurate: in s2n,
  it is used a scratch area for computing a hash on the key, when the
  key is too long. However, I think we want to avoid modeling this if
  possible, since this scratch value is never used again: `hmac_digest`
  calls `hash_reset` in `outer` before using it.

- the `outer` and `inner` state coming out of `hmac_digest` don't
  include update for the underlying hash's digest, since our Cryptol
  model of SHA256 has a digest ("Final") function which doesn't mutate
  the hash state. This may be because the hash digests are pure, but I
  have not verified this; the C interface allows them to change the hash
  state.
7c02c95
@ntc2
Add canonical s2n artifacts. 
To be sure we're all verifying the same thing.
78c400e
@ntc2
Axiomatize the `s2n_hash_init`. 
Specialized to SHA256.

I made a layout/endianness assumption here that I have not checked: when
a smaller struct is embedded in the bits of a larger struct in a union,
I assumed the smaller struct will be in the initial higher order bits.
ff1acba
@ntc2
Specify `s2n_hash_update` and `s2n_hash_digest`. 
And factor `setup_initial_hash_state` and `check_final_hash_state` out
of the `s2n_hash_init`, for reuse in the other specs. I wonder if this
abstraction would be possible if the state argument were not always
called `state`? I.e., could the arg name be a parameter?
e43f4f6
@ntc2
Make hash-state setup and check functions more abstract. 
The root of the "path" to the struct fields is now a parameter, so
that we can reuse the setup and check functions when setting up and
checking the hash states embedded in the hmac state.
d3b9d02
@ntc2
Add C-struct wrappers for imperative HMAC Cryptol model. 
I.e., translate between the C-struct as it appears in the LLVM, and
the Cryptol record we use in the imperative HMAC model. They're almost
the same, except that the nested hash states are treated differently
(they're much more complex in the C-struct).
88978ff
@ntc2
Axiomitize HMAC specs. 
These are still axioms, because running the proofs loops right
now. However, this is expected, and we'll need to treat some functions
as uninterpreted to make progress here.

Also, these specs are not complete: they don't enforce SHA256
everywhere yet.
58c46ef
@atomb
Enable simulation for hmac_update and hmac_digest 
These successfully run now, though I haven't tried to discharge the
resulting goals.

The hmac_init function still stalls. I expect it's for similar reasons
as the stalls that were affecting the update and digest functions, but
perhaps in a different instance.
6566098
@atomb
Prove s2n_hmac_update and s2n_hmac_digest
6c3a060
@ntc2
Make Cryptole `hmac_init` closure to s2n. 
And note why.
a782aba
@ntc2
Leave C hash state uninterpreted in `hmac_update_spec` and `hmac_dige… 
…st_spec`.

This brings us closer to a hash-algorithm-agnostic spec, which is the
next goal. We don't abstract `hmac_init_spec` yet, because symbolic
simulation is still not working there.
ed7d8a1
@ntc2
Add hash-alg-agnostic hash type `hash_ty` and use it in `hmac_update_… 
…spec`.

However, this approach isn't going to work for `hmac_digest_spec` yet,
since we need to call the hash update function at multiple msg sizes,
and it seems we can't have a higher rank (i.e. polymorphic `hash_ty`)
argument in Cryptol.
f584972
@ntc2
Start abstracting away from SHA256. 
Not complete yet. We replaced the SHA256-specific hash calls with
calls to generic `hash_init_c_state`, `hash_update_c_state`, and
`hash_digest_c_state`, which we define as `undefined` and
uninterpret. This allows us to eliminate most SHA256 specific code
from the spec, but we now need to deal with constraining values in the
HMAC state enough to allow the simulation to complete without error.

We are not verifying the `s2n_hash_*` function specs against a real
hash implemention right now, but the idea is to write them in such a
way that they would be verifiable.
ca98ca0
@jldodds
starting on travis
5a96dc9
@jldodds
-y to travis z3 install
89eb73c
@jldodds
another -y
01269af
@jldodds
testing if saw can run
f48a243
@jldodds
what if I break it?
5f3dc54
@jldodds
really breaking it this time...
3a30827
@ntc2
Distinguish `s2n_hash_update` calls as part of s2n build. 
The `hmac.ll` and `hmac.bc` files came from C code that was patched to
distinguish `s2n_hash_update` calls in `s2n_hmac_digest`, but the
patch was not recorded anywhere. Now it is recorded, and applied
automatically as part of our `s2n` build process.
61ae24d
@jldodds
start moving saw tests into makefile
e9e5582
@jldodds
add saw to all target 
move saw files into tests
put all bc files into the saw directory to avoid cluttering source dirs
make clean cleans bc files
5b58e30
@jldodds
stopped cleaning saw directory of bc files for now
b9a3fa8
@jldodds
better makefile orgainzation 
support for patching if code needs changing (not expected to be needed in the long run)
fixed bitcode generation and linking
moved bitcode out of s2n source directory
929b824
@jldodds
create empty patch file if one doesn't exist
35c7812
@jldodds
trying full s2n travis build
5b9d84b
@jldodds
always run saw from tests
a40dcc4

jldodds and others added some commits Jul 21, 2016

@jldodds
using new SAW test printout
20e2274
@jldodds
right path this time.
97ba28f
@jldodds
all of the stats
8eeb553
@jldodds
upgrade travis saw
11ca35b
@jldodds
redirect wget output this time
971fecb
@jldodds
Merge branch 'master' of github.com:jldodds/s2n
eb45a7c
@jldodds
Merge remote-tracking branch 'upstream/master' 
Conflicts:
	.travis.yml
67aa923
@jldodds
only export saw on linux travis builds
7d47a9c
@jldodds
travis fix
3491f24
@jldodds
added property about appending multiple HMAC-updates
5b6682a
@jldodds
removed intermediate representation
87c2090
@jldodds
break cryptol into files 
 - Hashing, for hash interface and state
 - HMAC for top level specification
 - HMAC_iterative for the iterative/stateful interface to HMAC
 - HMAC_properties for the statement of properties relating the other files
b16a531
@jldodds
fix references and imports for changed files
8998fe2
@jldodds
split driver code out of saw file, update references
2df2fd0
@jldodds
Merge remote-tracking branch 'upstream/master' 
Conflicts:
	.travis.yml
	tests/Makefile
c8b6df4
@jldodds
first attempt to install llvm-4.0
40f9d10
@jldodds
update apt-get
71fb21f
@jldodds
add key
1460797
@jldodds
try -f
a61101d
@jldodds
figure out where/which clang is already installed
ac8f446
@jldodds
just use the old clang
6acb249
@jldodds
echo information about clang
65129de
@jldodds
check which clang is used
5226daf
@jldodds
echo path
b17a6dc
@jldodds
fix path
fc50b2b
@jldodds
grab z3
6bb50c9
@jldodds
fix semicolon
371284a
@jldodds
chmod z3
94348e7
@jldodds
try old z3
4bf91c2
@jldodds
uncomment everything!
f93c208
@jldodds
Merge remote-tracking branch 'upstream/master'
a16578b
@jldodds
better comment about init 
fix travis typo

accidentally removed fuzzer install

fix python install
c9a730b
@jldodds
one more missing line
84a579b
@jldodds
prlmit
6d919c8
@atomb
Add append proof for hmac_update 
This proof shows that the imperative Cryptol version of hmac_update can
be called multiple times. That is, for any two messages, m1 and m2, the
result of calling update on m1 followed by update on m2 is equivalent to
calling update on m1 concatenated with m2.
526de7e
Show outdated Hide outdated s2nbc.mk

@colmmacc colmmacc merged commit e09e5e1 into awslabs:master Sep 7, 2016
1 check passed

1 check passed

continuous-integration/travis-ci/pr The Travis CI build passed
Details
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment