Skip to content

Commit

Permalink
Merge pull request #4 from ilvn/eng/revamp
Browse files Browse the repository at this point in the history
Revamp
  • Loading branch information
ilvn authored Mar 7, 2022
2 parents 84d4a0a + 57f4a50 commit 28c561f
Show file tree
Hide file tree
Showing 8 changed files with 377 additions and 612 deletions.
4 changes: 3 additions & 1 deletion LICENSE
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
MIT License

Copyright (c) 2021 Ilya O. Levin
Copyright (c) 2010,2014 Literatecode, http://www.literatecode.com
Copyright (c) 2022 Ilia Levin (ilia@levin.sg)


Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
Expand Down
27 changes: 27 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
CC = clang
CFLAGS= -O3 -pedantic -Wall -Wextra -std=c99
CBMC = cbmc
TARGET = sha256

.PHONY: clean verify

$(TARGET).o: sha256.c sha256.h
$(CC) $(CFLAGS) -c -o $@ $<

test: sha256.c sha256.h
$(CC) $(CFLAGS) -o $(TARGET) -DSHA256_SELF_TEST__ $<

all: test $(TARGET)

clean:
rm -f $(TARGET) *.o

verify:
$(CBMC) sha256.c -DSHA256_SELF_TEST__ -D_cbmc_ $(if $(FUNC),--function $(FUNC),) \
--unwind 64 --partial-loops \
--bounds-check \
--memory-leak-check --malloc-may-fail --malloc-fail-null \
--pointer-check --pointer-primitive-check --pointer-overflow-check \
--div-by-zero-check --conversion-check \
--signed-overflow-check --unsigned-overflow-check \
--undefined-shift-check --float-overflow-check
54 changes: 46 additions & 8 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,13 +1,51 @@
# SHA256

SHA-256 implementation to compliment a portable byte-oriented AES-256
implementation in C at http://www.literatecode.com/aes256
This is an implementation of the SHA-256 secure hash algorithm defined in
[FIPS 180-4](https://csrc.nist.gov/publications/detail/fips/180/4/final)

There is also a newer version in the [mark2](mark2) directory. This version is
cleaner and closer to a reference implementation. It no longer has
built-in support features for endianness, but you may easily adapt
the code to different endianness shall you need that.
It is not a byte-oriented implementation. Still, it may complement
a portable byte-oriented C version of AES-256 at
[www.literatecode.com/aes256](http://www.literatecode.com/aes256)

Unlike the previous implementation, the Mark 2 one is formally
verifiable with [CBMC](http://www.cprover.org/cbmc/)

## Compile

This implementation supports `clang` (recommended) and `GCC` C compilers.
Other compilers may also work with some minor code tweaking. Apologies for
not caring about the seamless support of the MSVC compiler any longer.
Check the legacy section below if you still need that.

Use `make` or `sh sha256.c -c -o sha256.o` to compile into an object file
that you may link with your project later.

Use `make test` or `sh sha256.c -DSHA256_SELF_TEST__` to compile an
executable binary that will perform a few known answer tests for SHA-256.


## Formal verification

We rely on [C Bounded Model Checker](http://www.cprover.org/cbmc/) to formally
verify code properties.

Use `make verify` to verify the self-testing code.

If you want to focus verification on a single function, use
`make verify FUNC=XYZ`, where `XYZ` is a function name.

Check [https://github.com/diffblue/cbmc](https://github.com/diffblue/cbmc)
for the latest version of CBMC.


## History

* 2010: The original code was written.
* 2013: The original code was published on [GitHub](https://github.com/ilvn/SHA256).
* 2014: The Mark 2 version was written (cleaner, closer to a reference implementation, formally verifiable).
* 2017: The Mark 2 version was added to the repository.
* 2022: The revamped Mark 2 version superseded the original code.

### Legacy

The original version is still available under the tag
[legacy](https://github.com/ilvn/SHA256/releases/tag/legacy) and provided
only for reference. Therefore, it is no longer supported or recommended.
32 changes: 0 additions & 32 deletions mark2/Makefile

This file was deleted.

Loading

0 comments on commit 28c561f

Please sign in to comment.