Revamp

restyle the code

add shell compile

update the copyright comment

add const attribute to FN_ functions; uninline _addbits

extra check ctx->len in sha256_hash()

update Makefile

update self test

add assumptions for cbmc

get rid of MINIMIZE_STACK_IMPACT, move W to a context

replace legacy with Mark 2 as the only variant

update the README file

update copyright

Author: ilvn

LICENSE

@@ -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 ([email protected])
+
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

Makefile

@@ -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

README.md

@@ -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.