diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 16e7b004..782b19b2 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -13,10 +13,10 @@ jobs: ci: runs-on: ubuntu-latest container: - image: ghcr.io/tillitis/tkey-builder:3 + image: ghcr.io/tillitis/tkey-builder:4 steps: - name: checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: # fetch-depth: 0 persist-credentials: false @@ -26,6 +26,21 @@ jobs: run: | git config --global --add safe.directory "$GITHUB_WORKSPACE" + - name: check indentation of our firmware C code + working-directory: hw/application_fpga + run: | + make -C fw/tk1 checkfmt + make -C fw/testfw checkfmt + + - name: run static analysis on firmware C code + working-directory: hw/application_fpga + run: | + make check + + - name: lint verilog using verilator + working-directory: hw/application_fpga + run: make lint + - name: compile ch552 firmware working-directory: hw/boards/mta1-usb-v1/ch552_fw run: make @@ -38,16 +53,6 @@ jobs: working-directory: hw/application_fpga run: make firmware.bin testfw.bin - - name: check fmt of our firmware C code - working-directory: hw/application_fpga - run: | - make -C fw/tk1 checkfmt - make -C fw/testfw checkfmt - - - name: lint verilog using verilator - working-directory: hw/application_fpga - run: make lint - # doing this last as it takes long time - name: make application FPGA gateware working-directory: hw/application_fpga diff --git a/contrib/Dockerfile b/contrib/Dockerfile index 3f3d73b4..f00f4ec2 100644 --- a/contrib/Dockerfile +++ b/contrib/Dockerfile @@ -42,7 +42,7 @@ RUN apt-get -qq update -y \ vim \ xdot \ sdcc \ - splint \ + splint \ cmake \ gcc-arm-none-eabi \ libnewlib-arm-none-eabi \ diff --git a/contrib/Makefile b/contrib/Makefile index d9aa7b1a..e38a0ce2 100644 --- a/contrib/Makefile +++ b/contrib/Makefile @@ -5,7 +5,7 @@ BUILDIMAGE=tkey-builder-local # default image used when running a container -IMAGE=ghcr.io/tillitis/tkey-builder:3 +IMAGE=ghcr.io/tillitis/tkey-builder:4 all: @echo "Targets:" diff --git a/hw/application_fpga/Makefile b/hw/application_fpga/Makefile index d570d330..25960395 100644 --- a/hw/application_fpga/Makefile +++ b/hw/application_fpga/Makefile @@ -149,6 +149,9 @@ firmware.elf: $(FIRMWARE_OBJS) $(P)/fw/tk1/firmware.lds .PHONY: check check: clang-tidy -header-filter=.* -checks=cert-* $(FIRMWARE_SOURCES) -- $(CFLAGS) + +.PHONY: splint +splint: splint -nolib -predboolint +boolint -nullpass -unrecog -infloops -initallelements -type -unreachable -unqualifiedtrans -fullinitblock $(FIRMWARE_SOURCES) testfw.elf: $(TESTFW_OBJS) $(P)/fw/tk1/firmware.lds @@ -165,6 +168,8 @@ testfw.hex: testfw.bin testfw_size_mismatch .PHONY: check-binary-hashes check-binary-hashes: + sha512sum firmware.bin + sha256sum application_fpga.bin sha512sum -c firmware.bin.sha512 sha256sum -c application_fpga.bin.sha256 @@ -350,6 +355,8 @@ help: @echo "Supported targets:" @echo "------------------" @echo "all Build all targets." + @echo "check Run static analysis on firmware." + @echo "splint Run splint static analysis on firmware." @echo "firmware.elf Build firmware ELF file." @echo "firmware.hex Build firmware converted to hex, to be included in bitstream." @echo "bram_fw.hex Build a fake BRAM file that will be filled in later after place-n-route." diff --git a/hw/application_fpga/application_fpga.bin.sha256 b/hw/application_fpga/application_fpga.bin.sha256 index fb9ba331..3e10e32c 100644 --- a/hw/application_fpga/application_fpga.bin.sha256 +++ b/hw/application_fpga/application_fpga.bin.sha256 @@ -1 +1 @@ -27a17eed9376111f5beb92d3c2c58dacca975a54534d05c25a92c5573920c291 application_fpga.bin +5b373c0ab86b8970b28270bb54825e1dc7f9723a80598ad85851c2b3aabed989 application_fpga.bin diff --git a/hw/application_fpga/firmware.bin.sha512 b/hw/application_fpga/firmware.bin.sha512 index e4097184..bcfcc7b8 100644 --- a/hw/application_fpga/firmware.bin.sha512 +++ b/hw/application_fpga/firmware.bin.sha512 @@ -1 +1 @@ -f53d7d86f92b796d750995c6540843b53346b58c4b97a57a290f6ae799e50d7e7afad519aa37277c17d476417d5a7d45f840dd2ed6ede3564602ff75c9007488 firmware.bin +e28f9f103e4f027ff9f137f94eef4218a486bd2b518a847b5ff7ccaa7eaf8308c07864d03d54dedcf9866e895fc119687381a6dd8f5d2f013b6a6d0437251f76 firmware.bin diff --git a/hw/application_fpga/fw/tk1/assert.c b/hw/application_fpga/fw/tk1/assert.c index adce820b..2c3d75e9 100644 --- a/hw/application_fpga/fw/tk1/assert.c +++ b/hw/application_fpga/fw/tk1/assert.c @@ -20,8 +20,10 @@ void assert_fail(const char *assertion, const char *file, unsigned int line, htif_puts(function); htif_lf(); +#ifndef S_SPLINT_S // Force illegal instruction to halt CPU asm volatile("unimp"); +#endif // Not reached __builtin_unreachable(); diff --git a/hw/application_fpga/fw/tk1/lib.c b/hw/application_fpga/fw/tk1/lib.c index 8c860eb9..ac8b69a8 100644 --- a/hw/application_fpga/fw/tk1/lib.c +++ b/hw/application_fpga/fw/tk1/lib.c @@ -104,6 +104,7 @@ void *memset(void *dest, int c, unsigned n) for (; n; n--, s++) *s = (uint8_t)c; + /*@ -temptrans @*/ return dest; } @@ -117,6 +118,11 @@ void memcpy_s(void *dest, size_t destsize, const void *src, size_t n) uint8_t *dest_byte = (uint8_t *)dest; for (size_t i = 0; i < n; i++) { + /*@ -nullderef @*/ + /* splint complains that dest_byte and src_byte can be + * NULL, but it seems it doesn't understand assert. + * See above. + */ dest_byte[i] = src_byte[i]; } } diff --git a/hw/application_fpga/fw/tk1/main.c b/hw/application_fpga/fw/tk1/main.c index cce3ca90..8022cff7 100644 --- a/hw/application_fpga/fw/tk1/main.c +++ b/hw/application_fpga/fw/tk1/main.c @@ -92,8 +92,8 @@ static uint32_t rnd_word(void) static void compute_cdi(const uint8_t *digest, const uint8_t use_uss, const uint8_t *uss) { - uint32_t local_uds[8]; - uint32_t local_cdi[8]; + uint32_t local_uds[8] = {0}; + uint32_t local_cdi[8] = {0}; blake2s_ctx secure_ctx = {0}; uint32_t rnd_sleep = 0; int blake2err = 0; @@ -115,7 +115,7 @@ static void compute_cdi(const uint8_t *digest, const uint8_t use_uss, // while on the firmware stack which is in the special fw_ram. wordcpy_s(local_uds, 8, (void *)uds, 8); blake2s_update(&secure_ctx, (const void *)local_uds, 32); - memset(local_uds, 0, 32); + (void)memset(local_uds, 0, 32); // Update with TKey program digest blake2s_update(&secure_ctx, digest, 32); @@ -268,7 +268,9 @@ static enum state loading_commands(const struct frame_header *hdr, nbytes = ctx->left; } memcpy_s(ctx->loadaddr, ctx->left, cmd + 1, nbytes); + /*@-mustfreeonly@*/ ctx->loadaddr += nbytes; + /*@+mustfreeonly@*/ ctx->left -= nbytes; if (ctx->left == 0) { @@ -396,7 +398,12 @@ int main(void) // Let the app know the function adddress for blake2s() *fw_blake2s_addr = (uint32_t)blake2s; + /*@-mustfreeonly@*/ + /* Yes, splint, this points directly to RAM and we don't care + * about freeing anything was pointing to 0x0 before. + */ ctx.loadaddr = (uint8_t *)TK1_RAM_BASE; + /*@+mustfreeonly@*/ ctx.use_uss = FALSE; scramble_ram(); @@ -436,5 +443,7 @@ int main(void) } } + /*@ -compdestroy @*/ + /* We don't care about memory leaks here. */ return (int)0xcafebabe; } diff --git a/hw/application_fpga/fw/tk1/proto.c b/hw/application_fpga/fw/tk1/proto.c index b01a3f79..4acbce48 100644 --- a/hw/application_fpga/fw/tk1/proto.c +++ b/hw/application_fpga/fw/tk1/proto.c @@ -167,7 +167,7 @@ static int read(uint8_t *buf, size_t bufsize, size_t nbytes) // bytelen returns the number of bytes a cmdlen takes static int bytelen(enum cmdlen cmdlen) { - int len; + int len = 0; switch (cmdlen) { case LEN_1: diff --git a/hw/application_fpga/fw/tk1/proto.h b/hw/application_fpga/fw/tk1/proto.h index 4bf225f0..1c13c5c4 100644 --- a/hw/application_fpga/fw/tk1/proto.h +++ b/hw/application_fpga/fw/tk1/proto.h @@ -50,6 +50,7 @@ struct frame_header { enum cmdlen len; }; +/*@ -exportlocal @*/ void writebyte(uint8_t b); uint8_t readbyte(void); void fwreply(struct frame_header hdr, enum fwcmd rspcode, uint8_t *buf);