diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3a634279e0..81a2148ee3 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -571,6 +571,39 @@ jobs: chmod +x bin/* make ${{ matrix.s2n-target }} + exercises: + name: "Test SAW exercises" + needs: build + runs-on: ubuntu-22.04 + strategy: + matrix: + ghc: ["8.10.7"] + steps: + - uses: actions/checkout@v2 + - run: | + mkdir -p exercises/bin + + - name: Download previously-built SAW + uses: actions/download-artifact@v2 + with: + name: "${{ runner.os }}-bins" + path: ./exercises/bin + + - uses: satackey/action-docker-layer-caching@v0.0.11 + continue-on-error: true + + - shell: bash + name: "make exercises container" + working-directory: exercises + run: docker build -t exercises . + + - shell: bash + name: "run exercises" + working-directory: exercises + run: | + chmod +x bin/* + docker run -v $PWD/bin:/saw-bin exercises + # Indicates sufficient CI success for the purposes of mergify merging the pull # request, see .github/mergify.yml. This is done instead of enumerating each # instance of each job in the mergify configuration for a number of reasons: @@ -585,5 +618,6 @@ jobs: - saw-remote-api-tests - cabal-test - s2n-tests + - exercises steps: - run: "true" diff --git a/exercises/.dockerignore b/exercises/.dockerignore new file mode 100644 index 0000000000..ba077a4031 --- /dev/null +++ b/exercises/.dockerignore @@ -0,0 +1 @@ +bin diff --git a/exercises/.gitignore b/exercises/.gitignore new file mode 100644 index 0000000000..254658e6bc --- /dev/null +++ b/exercises/.gitignore @@ -0,0 +1 @@ +*.bc diff --git a/exercises/Dockerfile b/exercises/Dockerfile new file mode 100644 index 0000000000..53667ba1ca --- /dev/null +++ b/exercises/Dockerfile @@ -0,0 +1,11 @@ +FROM ubuntu:22.04 + +RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections +RUN apt-get update && apt-get install -y clang-12 make + +RUN find /usr/bin/ -name "*-12" -exec basename {} \; | sed "s/\-12//" | xargs -I{} ln -s /usr/bin/'{}'-12 /usr/bin/'{}' + +COPY . /workdir + +ENTRYPOINT [ "/workdir/ci-entrypoint.sh" ] +CMD [ "/bin/bash" ] diff --git a/exercises/README.md b/exercises/README.md new file mode 100644 index 0000000000..ad2858b9b2 --- /dev/null +++ b/exercises/README.md @@ -0,0 +1,44 @@ +# SAW Exercises # + +This directory contains exercises to help SAW learners gain confidence in their +proof writing abilities by working on simple, well-defined proofs. Each +exercise folder contains a well-commented `exercise.saw` file containing +problems to work on, as well as a `solutions.saw` file with a sample solution. +Some exercises have more than one valid solution, though the `solutions.saw` +file will only list one. We designed the exercises to be completed in +following order: + +1. `memory-safety/popcount` +2. `memory-safety/swap` +3. `memory-safety/u128` +4. `memory-safety/point` +5. `functional-correctness/popcount` +6. `functional-correctness/u128` +7. `functional-correctness/point` +8. `functional-correctness/swap` +9. `sha512` + +You'll also find a `salsa20` exercise in the `memory-safety` and +`functional-correctness` folders. Unlike the other exercises, these exercises +lack an `exercise.saw` file. It is an opportunity to test what you've learned +to write a proof from scratch. The `salsa20` proofs are simpler than the +`sha512` proof, but the challenge comes from writing a proof without any +signposting or helper functions. + +## Building Bitcode ## + +To run the exercises and solutions, you'll first need to build the bitcode for +all of the C programs. To do this, simply run the `Makefile` in `common`: + +```bash +cd common +make +``` + +## Continuous Integration (CI) ## + +To ensure these exercises stay up to date, we have integrated them with our CI +system. Our CI runs the `ci-entrypoint.sh` script in a docker container +defined by `Dockerfile`, which in term runs SAW over all of the exercises and +solutions. This script and docker image are not intended to be used outside of +a CI system. diff --git a/exercises/ci-entrypoint.sh b/exercises/ci-entrypoint.sh new file mode 100755 index 0000000000..136660e415 --- /dev/null +++ b/exercises/ci-entrypoint.sh @@ -0,0 +1,27 @@ +#!/usr/bin/env bash +set -xe + +# This script checks all of the exercise and solution files. It is only +# intended to be executed by the saw-script CI system. + +cd /workdir +mkdir bin +cp /saw-bin/saw bin/saw +cp /saw-bin/abc bin/abc +cp /saw-bin/yices bin/yices +cp /saw-bin/yices-smt2 bin/yices-smt2 +cp /saw-bin/z3 bin/z3 +chmod +x bin/* + +export PATH=/workdir/bin:$PATH + +abc -h || true +z3 --version +yices --version +yices-smt2 --version + +# Build bitcode for all C programs +(cd common && make) + +# Run SAW over all exercises and solutions +find . -name solution.saw -o -name exercise.saw | xargs -I % sh -c "saw % || exit 255" diff --git a/exercises/common/Makefile b/exercises/common/Makefile new file mode 100644 index 0000000000..b83d7072bf --- /dev/null +++ b/exercises/common/Makefile @@ -0,0 +1,10 @@ +.SUFFIXES: .c .bc +.PHONY: all + +C_FILES = $(shell find .. -name '*.c') +BC_FILES = $(patsubst %.c, %.bc, $(C_FILES)) + +all: $(BC_FILES) + +%.bc : %.c + clang -g -O0 -c -emit-llvm $< -o $@ diff --git a/exercises/common/helpers.saw b/exercises/common/helpers.saw new file mode 100644 index 0000000000..8ebf23a78e --- /dev/null +++ b/exercises/common/helpers.saw @@ -0,0 +1,60 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + +/* + * SAW helpers + */ +// Given a value `v` of type `ty`, allocates and returns a pointer to memory +// storing `v` +let alloc_init ty v = do { + p <- crucible_alloc ty; + crucible_points_to p v; + return p; +}; + +// Given a value `v` of type `ty`, allocates and returns a read only pointer to +// memory storing `v` +let alloc_init_readonly ty v = do { + p <- crucible_alloc_readonly ty; + crucible_points_to p v; + return p; +}; + +// Given a name `n` and a type `ty`, allocates a fresh variable `x` of type +// `ty` and returns a tuple of `x` and a pointer to `x`. +let ptr_to_fresh n ty = do { + x <- crucible_fresh_var n ty; + p <- alloc_init ty (crucible_term x); + return (x, p); +}; + +// Given a name `n` and a type `ty`, allocates a fresh variable `x` of type +// `ty` and returns a tuple of `x` and a read only pointer to `x`. +let ptr_to_fresh_readonly n ty = do { + x <- crucible_fresh_var n ty; + p <- alloc_init_readonly ty (crucible_term x); + return (x, p); +}; + +// Given a name `n` and a value `v`, assert that the `n` has a value of `v` +let global_points_to n v = do { + crucible_points_to (crucible_global n) (crucible_term v); +}; + +// Given a name `n` and a value `v`, declare that n is initialized, and assert that has value v +let global_alloc_init n v = do { + crucible_alloc_global n; + global_points_to n v; +}; + +// llvm integer type aliases +let i8 = llvm_int 8; +let i16 = llvm_int 16; +let i32 = llvm_int 32; +let i64 = llvm_int 64; +let i128 = llvm_int 128; +let i384 = llvm_int 384; +let i512 = llvm_int 512; + diff --git a/exercises/functional-correctness/complete-examples/add/add.c b/exercises/functional-correctness/complete-examples/add/add.c new file mode 100644 index 0000000000..2b9cea2b3a --- /dev/null +++ b/exercises/functional-correctness/complete-examples/add/add.c @@ -0,0 +1,3 @@ +#include + +uint32_t add(uint32_t x, uint32_t y) { return x + y; } \ No newline at end of file diff --git a/exercises/functional-correctness/complete-examples/add/solution.saw b/exercises/functional-correctness/complete-examples/add/solution.saw new file mode 100644 index 0000000000..8cf4e88fd8 --- /dev/null +++ b/exercises/functional-correctness/complete-examples/add/solution.saw @@ -0,0 +1,21 @@ +let add_spec = do { + // Create fresh variables for `x` and `y` + x <- llvm_fresh_var "x" (llvm_int 32); + y <- llvm_fresh_var "y" (llvm_int 32); + + // Invoke the function with the fresh variables + llvm_execute_func [llvm_term x, llvm_term y]; + + // The function returns a value containing the sum of x and y + llvm_return (llvm_term {{ x + y }}); +}; + +// Load LLVM bitcode to verify +m <- llvm_load_module "add.bc"; + +// Verify the `add` function satisfies its specification +llvm_verify m "add" [] true add_spec (do { + //simplify (cryptol_ss()); + //print_goal; + z3; +}); diff --git a/exercises/functional-correctness/point/Point.cry b/exercises/functional-correctness/point/Point.cry new file mode 100644 index 0000000000..6c51cdd2e8 --- /dev/null +++ b/exercises/functional-correctness/point/Point.cry @@ -0,0 +1,12 @@ +module Point where + +type Point = {x : [32], y : [32]} + +POINT_ZERO : Point +POINT_ZERO = zero + +point_add : Point -> Point -> Point +point_add p1 p2 = { x = p1.x + p2.x, y = p1.y + p2.y } + +point_add_commutes : Point -> Point -> Bit +property point_add_commutes p1 p2 = point_add p1 p2 == point_add p2 p1 \ No newline at end of file diff --git a/exercises/functional-correctness/point/exercise.saw b/exercises/functional-correctness/point/exercise.saw new file mode 100644 index 0000000000..2af062c3b8 --- /dev/null +++ b/exercises/functional-correctness/point/exercise.saw @@ -0,0 +1,87 @@ +/////////////////////////////////////////////////////////////////////////////// +// Exercise: Point Functional Correctness +/////////////////////////////////////////////////////////////////////////////// + + +include "../../common/helpers.saw"; +import "Point.cry"; + +m <- llvm_load_module "point.bc"; + +/////////////////////////////////////////////////////////////////////////////// +// Part 1: Simple Point Equality +/////////////////////////////////////////////////////////////////////////////// + +// Convert the memory safety spec below into a functional correctness +// specification. + +// You can specify the values in a struct by using llvm_struct_value: +// llvm_struct_value [ , , ... ]; + +let point_eq_spec = do { + (p1, p1_ptr) <- ptr_to_fresh_readonly "p1" (llvm_struct "struct.point"); + (p2, p2_ptr) <- ptr_to_fresh_readonly "p2" (llvm_struct "struct.point"); + + llvm_execute_func [p1_ptr, p2_ptr]; + + ret <- llvm_fresh_var "ret" (llvm_int 1); + llvm_return (llvm_term ret); +}; + +point_eq_ov <- llvm_verify m "point_eq" [] true point_eq_spec z3; + +/////////////////////////////////////////////////////////////////////////////// +// Part 2: Point Allocation +/////////////////////////////////////////////////////////////////////////////// + +// Convert the memory safety proofs below into functional correctness proofs. + +let point_new_spec = do { + p_x <- llvm_fresh_var "p_x" (llvm_int 32); + p_y <- llvm_fresh_var "p_y" (llvm_int 32); + + llvm_execute_func [ llvm_term p_x, llvm_term p_y ]; + + (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_struct "struct.point"); + llvm_return ret_ptr; +}; + +point_new_ov <- llvm_verify m "point_new" [] true point_new_spec z3; + +let point_copy_spec = do { + (p, p_ptr) <- ptr_to_fresh_readonly "p" (llvm_struct "struct.point"); + + llvm_execute_func [p_ptr]; + + (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_struct "struct.point"); + llvm_return ret_ptr; +}; + +point_copy_ov <- llvm_verify m "point_copy" [point_new_ov] true point_copy_spec z3; + +/////////////////////////////////////////////////////////////////////////////// +// Part 3: Point Addition +/////////////////////////////////////////////////////////////////////////////// + +// Convert the memory safety proof below into a proof that the C `point_add` +// function is equivalent to the Cryptol `point_add` function in Point.cry. + +let point_add_spec = do { + llvm_alloc_global "ZERO"; + zero_global <- llvm_fresh_var "zero_global" (llvm_struct "struct.point"); + llvm_points_to (llvm_global "ZERO") (llvm_term zero_global); + + (p1, p1_ptr) <- ptr_to_fresh_readonly "p1" (llvm_struct "struct.point"); + (p2, p2_ptr) <- ptr_to_fresh_readonly "p2" (llvm_struct "struct.point"); + + llvm_execute_func [p1_ptr, p2_ptr]; + + (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_struct "struct.point"); + llvm_return ret_ptr; +}; + +llvm_verify m "point_add" + [point_new_ov, point_copy_ov, point_eq_ov] + true + point_add_spec + z3; diff --git a/exercises/functional-correctness/point/point.c b/exercises/functional-correctness/point/point.c new file mode 100644 index 0000000000..148390fc08 --- /dev/null +++ b/exercises/functional-correctness/point/point.c @@ -0,0 +1,42 @@ +#include +#include +#include + +typedef struct point { + uint32_t x; + uint32_t y; +} point; + +point ZERO = {0, 0}; + +// Check whether two points are equal +bool point_eq(const point *p1, const point *p2) { + return p1->x == p2->x && p1->y == p2-> y; +} + +// Allocate and return a new point +point* point_new(uint32_t x, uint32_t y) { + point* ret = malloc(sizeof(point)); + ret->x = x; + ret->y = y; + return ret; +} + +// Return a new point containing a copy of `p` +point* point_copy(const point* p) { + return point_new(p->x, p->y); +} + +// Add two points +point* point_add(const point *p1, const point *p2) { + // Save an addition by checking for zero + if (point_eq(p1, &ZERO)) { + return point_copy(p2); + } + + if (point_eq(p2, &ZERO)) { + return point_copy(p1); + } + + return point_new(p1->x + p2->x, p1->y + p2->y); +} diff --git a/exercises/functional-correctness/point/solution.saw b/exercises/functional-correctness/point/solution.saw new file mode 100644 index 0000000000..95652c193e --- /dev/null +++ b/exercises/functional-correctness/point/solution.saw @@ -0,0 +1,82 @@ +include "../../common/helpers.saw"; +import "Point.cry"; + +m <- llvm_load_module "point.bc"; + +let fresh_point_readonly name = do { + p_ptr <- llvm_alloc_readonly (llvm_struct "struct.point"); + p_x <- llvm_fresh_var (str_concat name ".x") (llvm_int 32); + p_y <- llvm_fresh_var (str_concat name ".y") (llvm_int 32); + llvm_points_to p_ptr (llvm_struct_value [ llvm_term p_x, llvm_term p_y]); + let p = {{ { x = p_x, y = p_y } }}; + return (p, p_ptr); +}; + +let point_eq_spec = do { + (p1, p1_ptr) <- fresh_point_readonly "p1"; + (p2, p2_ptr) <- fresh_point_readonly "p2"; + + llvm_execute_func [p1_ptr, p2_ptr]; + + // This is confusing. p1 == p2 wont work because that produces a Bit, but + // this function wants a [1] as a response. + llvm_return (llvm_term {{ [p1 == p2] }}); +}; + +point_eq_ov <- llvm_verify m "point_eq" [] true + point_eq_spec + (w4_unint_z3 []); + +let alloc_assign_point p = do { + p_ptr <- llvm_alloc (llvm_struct "struct.point"); + llvm_points_to p_ptr (llvm_struct_value [ llvm_term {{ p.x }}, llvm_term {{ p.y }}]); + return p_ptr; +}; + +let point_new_spec = do { + p_x <- llvm_fresh_var "p_x" (llvm_int 32); + p_y <- llvm_fresh_var "p_y" (llvm_int 32); + + llvm_execute_func [ llvm_term p_x, llvm_term p_y ]; + + ret_ptr <- alloc_assign_point {{ {x = p_x, y = p_y } }}; + llvm_return ret_ptr; +}; + +point_new_ov <- llvm_verify m "point_new" [] true + point_new_spec + (w4_unint_z3 []); + +let point_copy_spec = do { + (p, p_ptr) <- fresh_point_readonly "p"; + + llvm_execute_func [p_ptr]; + + ret_ptr <- alloc_assign_point p; + llvm_return ret_ptr; +}; + +point_copy_ov <- llvm_verify m "point_copy" [point_new_ov] true + point_copy_spec + (w4_unint_z3 []); + +let point_add_spec = do { + let zero_term = llvm_term {{ 0 : [32] }}; + llvm_alloc_global "ZERO"; + llvm_points_to (llvm_global "ZERO") + (llvm_struct_value [zero_term, zero_term]); + + (p1, p1_ptr) <- fresh_point_readonly "p1"; + (p2, p2_ptr) <- fresh_point_readonly "p2"; + + llvm_execute_func [p1_ptr, p2_ptr]; + + res_ptr <- alloc_assign_point {{ point_add p1 p2 }}; + llvm_return res_ptr; +}; + +llvm_verify m "point_add" + [point_new_ov, point_copy_ov, point_eq_ov] + true + point_add_spec + (w4_unint_z3 []); diff --git a/exercises/functional-correctness/popcount/Popcount.cry b/exercises/functional-correctness/popcount/Popcount.cry new file mode 100644 index 0000000000..7d77cf246d --- /dev/null +++ b/exercises/functional-correctness/popcount/Popcount.cry @@ -0,0 +1,5 @@ +module Popcount where + +popCount : [32] -> [32] +popCount bits = ic ! 0 where + ic = [0] # [ if elt then prev + 1 else prev | elt <- bits | prev <- ic] \ No newline at end of file diff --git a/exercises/functional-correctness/popcount/exercise.saw b/exercises/functional-correctness/popcount/exercise.saw new file mode 100644 index 0000000000..a4bbef37a5 --- /dev/null +++ b/exercises/functional-correctness/popcount/exercise.saw @@ -0,0 +1,40 @@ +/////////////////////////////////////////////////////////////////////////////// +// Exercise: Popcount Functional Correctness +/////////////////////////////////////////////////////////////////////////////// + +/////////////////////////////////////////////////////////////////////////////// +// Part 1: Memory Safety to Functional Correctness +/////////////////////////////////////////////////////////////////////////////// + +// Convert the memory safety spec below to a function correctness spec. It +// should assert that the result of pop_count is equal to the result of popCount +// defined in "Popcount.cry" when applied to the same arguments. Ensure that +// the two llvm_verify commands at the end of this Part successfully verify. + +// Remember: +// * Use `import "some_cryptol_file.cry"` to make Cryptol definitions +// available in SAW. +// * Place inline cryptol between "{{" and "}}". + +let popcount_spec = do { + x <- llvm_fresh_var "x" (llvm_int 32); + llvm_execute_func [llvm_term x]; + ret <- llvm_fresh_var "ret" (llvm_int 32); + llvm_return ( llvm_term ret ); +}; + +popmod <- llvm_load_module "popcount.bc"; + +llvm_verify popmod "pop_count" [] true popcount_spec yices; +llvm_verify popmod "pop_count_mul" [] true popcount_spec yices; + +/////////////////////////////////////////////////////////////////////////////// +// Part 2: Performance +/////////////////////////////////////////////////////////////////////////////// + +// Uncomment the llvm_verify command below and re-run SAW on this file. You'll +// notice it takes much longer to verify this case than the others. Why do you +// think that is? + +// verify the while loop version +// llvm_verify popmod "pop_count_sparse" [] true popcount_spec yices; \ No newline at end of file diff --git a/exercises/functional-correctness/popcount/popcount.c b/exercises/functional-correctness/popcount/popcount.c new file mode 100644 index 0000000000..ea2afe430a --- /dev/null +++ b/exercises/functional-correctness/popcount/popcount.c @@ -0,0 +1,33 @@ +#include + +/* + * Returns a count of the set bits in a word. + * From Henry S. Warren Jr.'s Hacker's Delight + */ +int pop_count(uint32_t x) { + x = x - ((x >> 1) & 0x55555555); + x = (x & 0x33333333) + ((x >> 2) & 0x33333333); + x = (x + (x >> 4)) & 0x0F0F0F0F; + x = x + (x >> 8); + x = x + (x >> 16); + return x & 0x0000003F; +} + +/* A version of popcount that uses multiplication */ +int pop_count_mul(uint32_t x) { + x = x - ((x >> 1) & 0x55555555); + x = (x & 0x33333333) + ((x >> 2) & 0x33333333); + x = ((x + (x >> 4)) & 0x0F0F0F0F); + return (x * 0x01010101) >> 24; +} + +/* A version of popcount that uses an indefinite while loop(!) */ +int pop_count_sparse(uint32_t x) { + int n; + n = 0; + while (x != 0) { + n = n + 1; + x = x & (x - 1); + } + return n; +} \ No newline at end of file diff --git a/exercises/functional-correctness/popcount/solution.saw b/exercises/functional-correctness/popcount/solution.saw new file mode 100644 index 0000000000..c195f1b32d --- /dev/null +++ b/exercises/functional-correctness/popcount/solution.saw @@ -0,0 +1,24 @@ +import "Popcount.cry"; + +popmod <- llvm_load_module "popcount.bc"; + +let pop_cryptol_check = do { + x <- llvm_fresh_var "x" (llvm_int 32); + llvm_execute_func [llvm_term x]; + llvm_return ( llvm_term {{ popCount x }} ); +}; + +// same verification against Cryptol spec +llvm_verify popmod "pop_count" [] true pop_cryptol_check (do { + //unfolding ["popCount"]; + //simplify (cryptol_ss()); + //print_goal; + z3; +}); + +// Begin Cryptol additional verifications +// another tricky implementation +llvm_verify popmod "pop_count_mul" [] true pop_cryptol_check yices; + +// verify the while loop version +llvm_verify popmod "pop_count_sparse" [] true pop_cryptol_check yices; diff --git a/exercises/functional-correctness/salsa20/Salsa20.cry b/exercises/functional-correctness/salsa20/Salsa20.cry new file mode 100644 index 0000000000..74940405c6 --- /dev/null +++ b/exercises/functional-correctness/salsa20/Salsa20.cry @@ -0,0 +1,180 @@ +/* + * Copyright (c) 2013-2016 Galois, Inc. + * Distributed under the terms of the BSD3 license (see LICENSE file) + */ + +// see http://cr.yp.to/snuffle/spec.pdf + +module Salsa20 where + +quarterround : [4][32] -> [4][32] +quarterround [y0, y1, y2, y3] = [z0, z1, z2, z3] + where + z1 = y1 ^ ((y0 + y3) <<< 0x7) + z2 = y2 ^ ((z1 + y0) <<< 0x9) + z3 = y3 ^ ((z2 + z1) <<< 0xd) + z0 = y0 ^ ((z3 + z2) <<< 0x12) + +property quarterround_passes_tests = + (quarterround [0x00000000, 0x00000000, 0x00000000, 0x00000000] == [0x00000000, 0x00000000, 0x00000000, 0x00000000]) /\ + (quarterround [0x00000001, 0x00000000, 0x00000000, 0x00000000] == [0x08008145, 0x00000080, 0x00010200, 0x20500000]) /\ + (quarterround [0x00000000, 0x00000001, 0x00000000, 0x00000000] == [0x88000100, 0x00000001, 0x00000200, 0x00402000]) /\ + (quarterround [0x00000000, 0x00000000, 0x00000001, 0x00000000] == [0x80040000, 0x00000000, 0x00000001, 0x00002000]) /\ + (quarterround [0x00000000, 0x00000000, 0x00000000, 0x00000001] == [0x00048044, 0x00000080, 0x00010000, 0x20100001]) /\ + (quarterround [0xe7e8c006, 0xc4f9417d, 0x6479b4b2, 0x68c67137] == [0xe876d72b, 0x9361dfd5, 0xf1460244, 0x948541a3]) /\ + (quarterround [0xd3917c5b, 0x55f1c407, 0x52a58a7a, 0x8f887a3b] == [0x3e2f308c, 0xd90a8f36, 0x6ab2a923, 0x2883524c]) + +rowround : [16][32] -> [16][32] +rowround [y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15] = + [z0, z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11, z12, z13, z14, z15] + where + [ z0, z1, z2, z3] = quarterround [ y0, y1, y2, y3] + [ z5, z6, z7, z4] = quarterround [ y5, y6, y7, y4] + [z10, z11, z8, z9] = quarterround [y10, y11, y8, y9] + [z15, z12, z13, z14] = quarterround [y15, y12, y13, y14] + +property rowround_passes_tests = + (rowround [0x00000001, 0x00000000, 0x00000000, 0x00000000, + 0x00000001, 0x00000000, 0x00000000, 0x00000000, + 0x00000001, 0x00000000, 0x00000000, 0x00000000, + 0x00000001, 0x00000000, 0x00000000, 0x00000000] == + [0x08008145, 0x00000080, 0x00010200, 0x20500000, + 0x20100001, 0x00048044, 0x00000080, 0x00010000, + 0x00000001, 0x00002000, 0x80040000, 0x00000000, + 0x00000001, 0x00000200, 0x00402000, 0x88000100]) /\ + (rowround [0x08521bd6, 0x1fe88837, 0xbb2aa576, 0x3aa26365, + 0xc54c6a5b, 0x2fc74c2f, 0x6dd39cc3, 0xda0a64f6, + 0x90a2f23d, 0x067f95a6, 0x06b35f61, 0x41e4732e, + 0xe859c100, 0xea4d84b7, 0x0f619bff, 0xbc6e965a] == + [0xa890d39d, 0x65d71596, 0xe9487daa, 0xc8ca6a86, + 0x949d2192, 0x764b7754, 0xe408d9b9, 0x7a41b4d1, + 0x3402e183, 0x3c3af432, 0x50669f96, 0xd89ef0a8, + 0x0040ede5, 0xb545fbce, 0xd257ed4f, 0x1818882d]) + +rowround_opt : [16][32] -> [16][32] +rowround_opt ys = join [ (quarterround (yi<<>>i | yi <- split ys | i <- [0 .. 3] ] + +property rowround_opt_is_rowround ys = rowround ys == rowround_opt ys + +columnround : [16][32] -> [16][32] +columnround [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15] = + [y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15] + where + [ y0, y4, y8, y12] = quarterround [ x0, x4, x8, x12] + [ y5, y9, y13, y1] = quarterround [ x5, x9, x13, x1] + [y10, y14, y2, y6] = quarterround [x10, x14, x2, x6] + [y15, y3, y7, y11] = quarterround [x15, x3, x7, x11] + +property columnround_passes_tests = + (columnround [0x00000001, 0x00000000, 0x00000000, 0x00000000, + 0x00000001, 0x00000000, 0x00000000, 0x00000000, + 0x00000001, 0x00000000, 0x00000000, 0x00000000, + 0x00000001, 0x00000000, 0x00000000, 0x00000000] == + [0x10090288, 0x00000000, 0x00000000, 0x00000000, + 0x00000101, 0x00000000, 0x00000000, 0x00000000, + 0x00020401, 0x00000000, 0x00000000, 0x00000000, + 0x40a04001, 0x00000000, 0x00000000, 0x00000000]) /\ + (columnround [0x08521bd6, 0x1fe88837, 0xbb2aa576, 0x3aa26365, + 0xc54c6a5b, 0x2fc74c2f, 0x6dd39cc3, 0xda0a64f6, + 0x90a2f23d, 0x067f95a6, 0x06b35f61, 0x41e4732e, + 0xe859c100, 0xea4d84b7, 0x0f619bff, 0xbc6e965a] == + [0x8c9d190a, 0xce8e4c90, 0x1ef8e9d3, 0x1326a71a, + 0x90a20123, 0xead3c4f3, 0x63a091a0, 0xf0708d69, + 0x789b010c, 0xd195a681, 0xeb7d5504, 0xa774135c, + 0x481c2027, 0x53a8e4b5, 0x4c1f89c5, 0x3f78c9c8]) + +columnround_opt : [16][32] -> [16][32] +columnround_opt xs = join (transpose [ (quarterround (xi<<>>i | xi <- transpose(split xs) | i <- [0 .. 3] ]) + +columnround_opt_is_columnround xs = columnround xs == columnround_opt xs + +property columnround_is_transpose_of_rowround ys = + rowround ys == join(transpose(split`{4}(columnround xs))) + where xs = join(transpose(split`{4} ys)) + +doubleround : [16][32] -> [16][32] +doubleround(xs) = rowround(columnround(xs)) + +property doubleround_passes_tests = + (doubleround [0x00000001, 0x00000000, 0x00000000, 0x00000000, + 0x00000000, 0x00000000, 0x00000000, 0x00000000, + 0x00000000, 0x00000000, 0x00000000, 0x00000000, + 0x00000000, 0x00000000, 0x00000000, 0x00000000] == + [0x8186a22d, 0x0040a284, 0x82479210, 0x06929051, + 0x08000090, 0x02402200, 0x00004000, 0x00800000, + 0x00010200, 0x20400000, 0x08008104, 0x00000000, + 0x20500000, 0xa0000040, 0x0008180a, 0x612a8020]) /\ + (doubleround [0xde501066, 0x6f9eb8f7, 0xe4fbbd9b, 0x454e3f57, + 0xb75540d3, 0x43e93a4c, 0x3a6f2aa0, 0x726d6b36, + 0x9243f484, 0x9145d1e8, 0x4fa9d247, 0xdc8dee11, + 0x054bf545, 0x254dd653, 0xd9421b6d, 0x67b276c1] == + [0xccaaf672, 0x23d960f7, 0x9153e63a, 0xcd9a60d0, + 0x50440492, 0xf07cad19, 0xae344aa0, 0xdf4cfdfc, + 0xca531c29, 0x8e7943db, 0xac1680cd, 0xd503ca00, + 0xa74b2ad6, 0xbc331c5c, 0x1dda24c7, 0xee928277]) + +littleendian : [4][8] -> [32] +littleendian b = join(reverse b) + +property littleendian_passes_tests = + (littleendian [ 0, 0, 0, 0] == 0x00000000) /\ + (littleendian [ 86, 75, 30, 9] == 0x091e4b56) /\ + (littleendian [255, 255, 255, 250] == 0xfaffffff) + +littleendian_inverse : [32] -> [4][8] +littleendian_inverse b = reverse(split b) + +property littleendian_is_invertable b = littleendian_inverse(littleendian b) == b + +Salsa20 : [64][8] -> [64][8] +Salsa20 xs = join ar + where + ar = [ littleendian_inverse words | words <- xw + zs@10 ] + xw = [ littleendian xi | xi <- split xs ] + zs = [xw] # [ doubleround zi | zi <- zs ] + +property Salsa20_passes_tests = + (Salsa20 [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] == + [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]) /\ + (Salsa20 [211, 159, 13, 115, 76, 55, 82, 183, 3, 117, 222, 37, 191, 187, 234, 136, + 49, 237, 179, 48, 1, 106, 178, 219, 175, 199, 166, 48, 86, 16, 179, 207, + 31, 240, 32, 63, 15, 83, 93, 161, 116, 147, 48, 113, 238, 55, 204, 36, + 79, 201, 235, 79, 3, 81, 156, 47, 203, 26, 244, 243, 88, 118, 104, 54] == + [109, 42, 178, 168, 156, 240, 248, 238, 168, 196, 190, 203, 26, 110, 170, 154, + 29, 29, 150, 26, 150, 30, 235, 249, 190, 163, 251, 48, 69, 144, 51, 57, + 118, 40, 152, 157, 180, 57, 27, 94, 107, 42, 236, 35, 27, 111, 114, 114, + 219, 236, 232, 135, 111, 155, 110, 18, 24, 232, 95, 158, 179, 19, 48, 202]) /\ + (Salsa20 [ 88, 118, 104, 54, 79, 201, 235, 79, 3, 81, 156, 47, 203, 26, 244, 243, + 191, 187, 234, 136, 211, 159, 13, 115, 76, 55, 82, 183, 3, 117, 222, 37, + 86, 16, 179, 207, 49, 237, 179, 48, 1, 106, 178, 219, 175, 199, 166, 48, + 238, 55, 204, 36, 31, 240, 32, 63, 15, 83, 93, 161, 116, 147, 48, 113] == + [179, 19, 48, 202, 219, 236, 232, 135, 111, 155, 110, 18, 24, 232, 95, 158, + 26, 110, 170, 154, 109, 42, 178, 168, 156, 240, 248, 238, 168, 196, 190, 203, + 69, 144, 51, 57, 29, 29, 150, 26, 150, 30, 235, 249, 190, 163, 251, 48, + 27, 111, 114, 114, 118, 40, 152, 157, 180, 57, 27, 94, 107, 42, 236, 35]) + +property Salsa20_has_no_collisions x1 x2 = + if(x1 != x2) then (doubleround x1) != (doubleround x2) else True + +// Salsa 20 supports two key sizes, [16][8] and [32][8] +Salsa20_expansion : {a} (a >= 1, 2 >= a) => ([16*a][8], [16][8]) -> [64][8] +Salsa20_expansion(k, n) = z + where + [s0, s1, s2, s3] = split "expand 32-byte k" : [4][4][8] + [t0, t1, t2, t3] = split "expand 16-byte k" : [4][4][8] + x = if(`a == 2) then s0 # k0 # s1 # n # s2 # k1 # s3 + else t0 # k0 # t1 # n # t2 # k0 # t3 + z = Salsa20(x) + [k0, k1] = (split(k#zero)):[2][16][8] + +Salsa20_encrypt : {a, l} (a >= 1, 2 >= a, l <= 2^^70) => ([16*a][8], [8][8], [l][8]) -> [l][8] +Salsa20_encrypt(k, v, m) = c + where + salsa = take (join [ Salsa20_expansion(k, v#(reverse (split i))) | i <- [0, 1 ... ] ]) + c = m ^ salsa diff --git a/exercises/functional-correctness/salsa20/salsa20.c b/exercises/functional-correctness/salsa20/salsa20.c new file mode 100644 index 0000000000..d7530c15ff --- /dev/null +++ b/exercises/functional-correctness/salsa20/salsa20.c @@ -0,0 +1,189 @@ +#include +#include +#include "salsa20.h" + +// Implements DJB's definition of '<<<' +static uint32_t rotl(uint32_t value, int shift) +{ + return (value << shift) | (value >> (32 - shift)); +} + +static void s20_quarterround(uint32_t *y0, uint32_t *y1, uint32_t *y2, uint32_t *y3) +{ + *y1 = *y1 ^ rotl(*y0 + *y3, 7); + *y2 = *y2 ^ rotl(*y1 + *y0, 9); + *y3 = *y3 ^ rotl(*y2 + *y1, 13); + *y0 = *y0 ^ rotl(*y3 + *y2, 18); +} + +static void s20_rowround(uint32_t y[static 16]) +{ + s20_quarterround(&y[0], &y[1], &y[2], &y[3]); + s20_quarterround(&y[5], &y[6], &y[7], &y[4]); + s20_quarterround(&y[10], &y[11], &y[8], &y[9]); + s20_quarterround(&y[15], &y[12], &y[13], &y[14]); +} + +static void s20_columnround(uint32_t x[static 16]) +{ + s20_quarterround(&x[0], &x[4], &x[8], &x[12]); + s20_quarterround(&x[5], &x[9], &x[13], &x[1]); + s20_quarterround(&x[10], &x[14], &x[2], &x[6]); + s20_quarterround(&x[15], &x[3], &x[7], &x[11]); +} + +static void s20_doubleround(uint32_t x[static 16]) +{ + s20_columnround(x); + s20_rowround(x); +} + +// Creates a little-endian word from 4 bytes pointed to by b +static uint32_t s20_littleendian(uint8_t *b) +{ + return b[0] + + (b[1] << 8) + + (b[2] << 16) + + (b[3] << 24); +} + +// Moves the little-endian word into the 4 bytes pointed to by b +static void s20_rev_littleendian(uint8_t *b, uint32_t w) +{ + b[0] = w; + b[1] = w >> 8; + b[2] = w >> 16; + b[3] = w >> 24; +} + +// The core function of Salsa20 +static void s20_hash(uint8_t seq[static 64]) +{ + int i; + uint32_t x[16]; + uint32_t z[16]; + + // Create two copies of the state in little-endian format + // First copy is hashed together + // Second copy is added to first, word-by-word + for (i = 0; i < 16; ++i) + x[i] = z[i] = s20_littleendian(seq + (4 * i)); + + for (i = 0; i < 10; ++i) + s20_doubleround(z); + + for (i = 0; i < 16; ++i) { + z[i] += x[i]; + s20_rev_littleendian(seq + (4 * i), z[i]); + } +} + +// The 16-byte (128-bit) key expansion function +static void s20_expand16(uint8_t *k, + uint8_t n[static 16], + uint8_t keystream[static 64]) +{ + int i, j; + // The constants specified by the Salsa20 specification, 'tau' + // "expand 16-byte k" + uint8_t t[4][4] = { + { 'e', 'x', 'p', 'a' }, + { 'n', 'd', ' ', '1' }, + { '6', '-', 'b', 'y' }, + { 't', 'e', ' ', 'k' } + }; + + // Copy all of 'tau' into the correct spots in our keystream block + for (i = 0; i < 64; i += 20) + for (j = 0; j < 4; ++j) + keystream[i + j] = t[i / 20][j]; + + // Copy the key and the nonce into the keystream block + for (i = 0; i < 16; ++i) { + keystream[4+i] = k[i]; + keystream[44+i] = k[i]; + keystream[24+i] = n[i]; + } + + s20_hash(keystream); +} + +// The 32-byte (256-bit) key expansion function +static void s20_expand32(uint8_t *k, + uint8_t n[static 16], + uint8_t keystream[static 64]) +{ + int i, j; + // The constants specified by the Salsa20 specification, 'sigma' + // "expand 32-byte k" + uint8_t o[4][4] = { + { 'e', 'x', 'p', 'a' }, + { 'n', 'd', ' ', '3' }, + { '2', '-', 'b', 'y' }, + { 't', 'e', ' ', 'k' } + }; + + // Copy all of 'sigma' into the correct spots in our keystream block + for (i = 0; i < 64; i += 20) + for (j = 0; j < 4; ++j) + keystream[i + j] = o[i / 20][j]; + + // Copy the key and the nonce into the keystream block + for (i = 0; i < 16; ++i) { + keystream[4+i] = k[i]; + keystream[44+i] = k[i+16]; + keystream[24+i] = n[i]; + } + + s20_hash(keystream); +} + +// Performs up to 2^32-1 bytes of encryption or decryption under a +// 128- or 256-bit key. +enum s20_status_t s20_crypt32(uint8_t *key, + uint8_t nonce[static 8], + uint32_t si, + uint8_t *buf, + uint32_t buflen) +{ + uint8_t keystream[64]; + // 'n' is the 8-byte nonce (unique message number) concatenated + // with the per-block 'counter' value (4 bytes in our case, 8 bytes + // in the standard). We leave the high 4 bytes set to zero because + // we permit only a 32-bit integer for stream index and length. + uint8_t n[16] = { 0 }; + uint32_t i; + + // If any of the parameters we received are invalid + if (key == NULL || nonce == NULL || buf == NULL) + return S20_FAILURE; + + // Set up the low 8 bytes of n with the unique message number + for (i = 0; i < 8; ++i) + n[i] = nonce[i]; + + // If we're not on a block boundary, compute the first keystream + // block. This will make the primary loop (below) cleaner + if (si % 64 != 0) { + // Set the second-to-highest 4 bytes of n to the block number + s20_rev_littleendian(n+8, si / 64); + // Expand the key with n and hash to produce a keystream block + s20_expand32(key, n, keystream); + } + + // Walk over the plaintext byte-by-byte, xoring the keystream with + // the plaintext and producing new keystream blocks as needed + for (i = 0; i < buflen; ++i) { + // If we've used up our entire keystream block (or have just begun + // and happen to be on a block boundary), produce keystream block + if ((si + i) % 64 == 0) { + s20_rev_littleendian(n+8, ((si + i) / 64)); + s20_expand32(key, n, keystream); + } + + // xor one byte of plaintext with one byte of keystream + buf[i] ^= keystream[(si + i) % 64]; + } + + return S20_SUCCESS; +} diff --git a/exercises/functional-correctness/salsa20/salsa20.h b/exercises/functional-correctness/salsa20/salsa20.h new file mode 100644 index 0000000000..df94eed6b1 --- /dev/null +++ b/exercises/functional-correctness/salsa20/salsa20.h @@ -0,0 +1,72 @@ +#ifndef _SALSA20_H_ +#define _SALSA20_H_ + +#include +#include + +/** + * Return codes for s20_crypt + */ +enum s20_status_t +{ + S20_SUCCESS, + S20_FAILURE +}; + +/** + * Key size + * Salsa20 only permits a 128-bit key or a 256-bit key, so these are + * the only two options made available by this library. + */ +enum s20_keylen_t +{ + S20_KEYLEN_256, + S20_KEYLEN_128 +}; + +/** + * Performs up to 2^32-1 bytes of encryption or decryption under a + * 128- or 256-bit key in blocks of arbitrary size. Permits seeking + * to any point within a stream. + * + * key Pointer to either a 128-bit or 256-bit key. + * No key-derivation function is applied to this key, and no + * entropy is gathered. It is expected that this key is already + * appropriate for direct use by the Salsa20 algorithm. + * + * keylen Length of the key. + * Must be S20_KEYLEN_256 or S20_KEYLEN_128. + * + * nonce Pointer to an 8-byte nonce. + * Does not have to be random, but must be unique for every + * message under a single key. Nonce reuse destroys message + * confidentiality. + * + * si Stream index. + * The position within the stream. When encrypting/decrypting + * a message sequentially from beginning to end in fixed-size + * chunks of length L, this value is increased by L on every + * call. Care must be taken not to select values that cause + * overlap. Example: encrypting 1000 bytes at index 100, and + * then encrypting 1000 bytes at index 500. Doing so will + * result in keystream reuse, which destroys message + * confidentiality. + * + * buf The data to encrypt or decrypt. + * + * buflen Length of the data in buf. + * + * This function returns either S20_SUCCESS or S20_FAILURE. + * A return of S20_SUCCESS indicates that basic sanity checking on + * parameters succeeded and encryption/decryption was performed. + * A return of S20_FAILURE indicates that basic sanity checking on + * parameters failed and encryption/decryption was not performed. + */ +enum s20_status_t s20_crypt(uint8_t *key, + enum s20_keylen_t keylen, + uint8_t nonce[static 8], + uint32_t si, + uint8_t *buf, + uint32_t buflen); + +#endif diff --git a/exercises/functional-correctness/salsa20/solution.saw b/exercises/functional-correctness/salsa20/solution.saw new file mode 100644 index 0000000000..c2af404ea4 --- /dev/null +++ b/exercises/functional-correctness/salsa20/solution.saw @@ -0,0 +1,74 @@ +include "../../common/helpers.saw"; +import "Salsa20.cry"; + +let oneptr_update_func (type : LLVMType) (name : String) (f : Term) = do { + (x, p) <- ptr_to_fresh name type; + llvm_execute_func [p]; + llvm_points_to p (llvm_term {{ f x }}); +}; + +let quarterround_setup : CrucibleSetup () = do { + (y0, p0) <- ptr_to_fresh "y0" (llvm_int 32); + (y1, p1) <- ptr_to_fresh "y1" (llvm_int 32); + (y2, p2) <- ptr_to_fresh "y2" (llvm_int 32); + (y3, p3) <- ptr_to_fresh "y3" (llvm_int 32); + + llvm_execute_func [p0, p1, p2, p3]; + + let zs = {{ quarterround [y0,y1,y2,y3] }}; + llvm_points_to p0 (llvm_term {{ zs@0 }}); + llvm_points_to p1 (llvm_term {{ zs@1 }}); + llvm_points_to p2 (llvm_term {{ zs@2 }}); + llvm_points_to p3 (llvm_term {{ zs@3 }}); +}; + +let rowround_setup = + oneptr_update_func (llvm_array 16 (llvm_int 32)) "y" {{ rowround }}; + +let columnround_setup = + oneptr_update_func (llvm_array 16 (llvm_int 32)) "x" {{ columnround }}; + +let doubleround_setup = + oneptr_update_func (llvm_array 16 (llvm_int 32)) "x" {{ doubleround }}; + +let salsa20_setup = + oneptr_update_func (llvm_array 64 (llvm_int 8)) "seq" {{ Salsa20 }}; + +let salsa20_expansion_32 = do { + (n, pn) <- ptr_to_fresh_readonly "n" (llvm_array 16 (llvm_int 8)); + (k, pk) <- ptr_to_fresh_readonly "k" (llvm_array 32 (llvm_int 8)); + + pks <- llvm_alloc (llvm_array 64 (llvm_int 8)); + + llvm_execute_func [pk, pn, pks]; + + let rks = {{ Salsa20_expansion`{a=2}(k, n)}}; + llvm_points_to pks (llvm_term rks); +}; + +let s20_encrypt32 n = do { + (key, pkey) <- ptr_to_fresh_readonly "key" (llvm_array 32 (llvm_int 8)); + (v, pv) <- ptr_to_fresh_readonly "nonce" (llvm_array 8 (llvm_int 8)); + (m, pm) <- ptr_to_fresh "buf" (llvm_array n (llvm_int 8)); + + llvm_execute_func [ pkey + , pv + , llvm_term {{ 0 : [32] }} + , pm + , llvm_term {{ `n : [32] }} + ]; + + llvm_points_to pm (llvm_term {{ Salsa20_encrypt (key, v, m) }}); + llvm_return (llvm_term {{ 0 : [32] }}); +}; + +m <- llvm_load_module "salsa20.bc"; +qr <- llvm_verify m "s20_quarterround" [] true quarterround_setup z3; +rr <- llvm_verify m "s20_rowround" [qr] true rowround_setup z3; +cr <- llvm_verify m "s20_columnround" [qr] true columnround_setup z3; +dr <- llvm_verify m "s20_doubleround" [cr,rr] true doubleround_setup z3; +s20 <- llvm_verify m "s20_hash" [dr] true salsa20_setup z3; +s20e32 <- llvm_verify m "s20_expand32" [s20] true salsa20_expansion_32 z3; +s20encrypt_63 <- llvm_verify m "s20_crypt32" [s20e32] true (s20_encrypt32 63) z3; +s20encrypt_64 <- llvm_verify m "s20_crypt32" [s20e32] true (s20_encrypt32 64) z3; +s20encrypt_65 <- llvm_verify m "s20_crypt32" [s20e32] true (s20_encrypt32 65) z3; diff --git a/exercises/functional-correctness/swap/Swap.cry b/exercises/functional-correctness/swap/Swap.cry new file mode 100644 index 0000000000..6eda8f76dc --- /dev/null +++ b/exercises/functional-correctness/swap/Swap.cry @@ -0,0 +1,46 @@ +module Swap where + +// Given a list and two indices, return a new list with the values at the +// indices swapped. +swap_list : {n} [n][32] -> [64] -> [64] -> [n][32] +swap_list lst i j = update (update lst i jval) j ival + where ival = lst @ i + jval = lst @ j + + +// Returns the index of the smallest element in a list +argmin : {n} (fin n) => [n][32] -> [64] +argmin lst = + (foldl' min (-1 : [32], -1 : [64]) [(x, i) | x <- lst | i <- [0...]]).1 + +selection_sort : {n} (fin n, 64 >= width n) => [n][32] -> [n][32] +selection_sort lst = go`{0} lst + where + // Recursively process `lst`. Places the smallest value at `idx` and + // recurses with `idx + 1`. + go : {idx} (fin idx, fin n, 64 >= width idx, 64 >= width n, n >= idx) + => [n][32] + -> [n][32] + go acc = + if `idx == `n + then acc + // Note to the curious: The `min n (idx + 1)` type parameter below + // is a weird hack. Cryptol is concerned about overflowing `idx` on + // the recursive call to `go` and needs to be reassured that `idx` + // will never exceed `n` (which itself is constrained to be a 64-bit + // value by the `64 >= width n` type constraint). You should not + // feel like you need to deeply understand this. Cryptol is not + // well suited for situations where a list changes sizes in a + // recursive function. Thankfully this case is rare in + // cryptography. + else go`{min n (idx + 1)} + (swap_list acc `idx (`idx + (argmin (drop`{idx} acc)))) + +// Check that if you pass the same value for i and j to swap_list, you get the +// same list back. +swap_list_same : {n} (fin n) => [64] -> [n][32] -> Bit +property swap_list_same i lst = undefined + +// Check that selection_sort is equivalent to Cryptol's built in 'sort' function +sort_eq : {n} (fin n, 64 >= width n) => [n][32] -> Bit +property sort_eq lst = undefined diff --git a/exercises/functional-correctness/swap/exercise.saw b/exercises/functional-correctness/swap/exercise.saw new file mode 100644 index 0000000000..8e8d857102 --- /dev/null +++ b/exercises/functional-correctness/swap/exercise.saw @@ -0,0 +1,162 @@ +//////////////////////////////////////////////////////////////////////////////// +// Exercise: Swap +//////////////////////////////////////////////////////////////////////////////// + +include "../../common/helpers.saw"; +swapmod <- llvm_load_module "swap.bc"; +import "Swap.cry"; + +//////////////////////////////////////////////////////////////////////////////// +// Part 1: Swap Functional Correctness +//////////////////////////////////////////////////////////////////////////////// + +// Convert the memory safety specs below into function correctness specs and +// re-run the proofs. + +let swap_diff_spec = do { + (x, xp) <- ptr_to_fresh "x" (llvm_int 32); + (y, yp) <- ptr_to_fresh "y" (llvm_int 32); + + llvm_execute_func [xp, yp]; + + x' <- llvm_fresh_var "x'" (llvm_int 32); + y' <- llvm_fresh_var "y'" (llvm_int 32); + + llvm_points_to xp (llvm_term x'); + llvm_points_to yp (llvm_term y'); +}; + +// Verify swap satisfies swap_diff_spec +swap_diff_ov <- llvm_verify swapmod "swap" [] true swap_diff_spec z3; + +// Verify xor_swap satisfies swap_diff_spec +llvm_verify swapmod "xor_swap" [] true swap_diff_spec z3; + +let swap_same_spec = do { + (x, x_ptr) <- ptr_to_fresh "x" (llvm_int 32); + + llvm_execute_func [x_ptr, x_ptr]; + + x' <- llvm_fresh_var "x'" (llvm_int 32); + llvm_points_to x_ptr (llvm_term x'); +}; + +// Verify swap satisfies swap_same_spec +swap_same_ov <- llvm_verify swapmod "swap" [] true swap_same_spec z3; + +//////////////////////////////////////////////////////////////////////////////// +// Part 2: Swap XOR Same Pointer +//////////////////////////////////////////////////////////////////////////////// + +// Try to prove that swap_xor satisfies your swap_same_spec specification. Why +// does the proof fail? + +//////////////////////////////////////////////////////////////////////////////// +// Part 3: swap_list_same Cryptol +//////////////////////////////////////////////////////////////////////////////// + +// Look through and understand the Cryptol in "Swap.cry". To gain confidence in +// the `swap_list` Cryptol function, fill in the property definition for +// `swap_list_same`. Prove the property using :prove for a few different values +// of `n`. + +// Hint: You will also need to provide a concrete value for `i` when using +// :prove. Why? + +//////////////////////////////////////////////////////////////////////////////// +// Part 4: sort_eq Cryptol +//////////////////////////////////////////////////////////////////////////////// + +// To gain confidence in the `selection_sort` function, fill in the property +// definition for sort_eq. Prove the property using :prove for n=4. +// Quickcheck the property using :check for larger n values (such as n=128). + +//////////////////////////////////////////////////////////////////////////////// +// Part 5: selection_sort Decomposition +//////////////////////////////////////////////////////////////////////////////// + +// Below you'll find a complete functional correctness proof for +// `selection_sort`. The specification takes a configurable size parameter +// `len`, and the proof itself sets `len` to 4. This proof works, but it has +// some problems: +// * The proof is inefficient and does not terminate in a reasonable time for +// larger `len` values. +// * The generated SAW terms are massive and unreadable. Debugging this proof +// during development would be tricky. + +let selection_sort_spec len = do { + (a, a_ptr) <- ptr_to_fresh "a" (llvm_array len (llvm_int 32)); + + llvm_execute_func [a_ptr, (llvm_term {{ `len : [64]}})]; + + llvm_points_to a_ptr (llvm_term {{ selection_sort a }}); +}; + +// Uncomment the llvm_verify command below to check that the proof works. + +let a_len = 4; +/* +llvm_verify + swapmod + "selection_sort" + [swap_diff_ov, swap_same_ov] + true + (selection_sort_spec a_len) + z3; + */ + +// To remedy this, break the body of the outer loop in the selection_sort C +// implementation into `swap_array` and `argmin` functions like the Cryptol +// specification. Write a new function `selection_sort_composed` that uses +// your new C helper functions. Rebuild the `swap.bc` LLVM bitcode file. The +// C functions should have the following type signatures: + +// void swap_array(uint32_t *a, size_t i, size_t j); +// size_t argmin(const uint32_t *a, size_t len); +// void selection_sort_composed(uint32_t *a, size_t len); + +//////////////////////////////////////////////////////////////////////////////// +// Part 6: Helper Function Functional Correctness +//////////////////////////////////////////////////////////////////////////////// + +// Prove your C `swap_array` and `argmin` functions equal to their Cryptol +// counterparts for lists of size 8. + +// Remember: Use `llvm_precond` to further restrict inputs: +// * llvm_precond {{ }}; + +//////////////////////////////////////////////////////////////////////////////// +// Part 7: Functional Correctness +//////////////////////////////////////////////////////////////////////////////// + +// Uncomment the loop below and verify that all of the proofs pass. If they +// don't, fix your argmin spec or implementation. + +/* +let a_len = 8; +argmin_ovs <- for (eval_list {{ [1..a_len] : [a_len][64]}}) (\len -> + llvm_verify swapmod "argmin" [] true (argmin_spec (eval_int len)) z3; +); +*/ + +//////////////////////////////////////////////////////////////////////////////// +// Part 8: selection_sort_composed Functional Correctness +//////////////////////////////////////////////////////////////////////////////// + +// Use `llvm_verify` to prove that your `selection_sort_composed` implementation +// satisfies the `selection_sort_spec` spec from Part 5 for `len=8`. Use the +// overrides from your `swap_array` and `argmin` proofs. + +// Remember: Use `concat` to join lists of overrides together +// * concat + +//////////////////////////////////////////////////////////////////////////////// +// Part 9: wacky_sort Functional Correctness +//////////////////////////////////////////////////////////////////////////////// + +// Uncomment `wacky_sort` in `swap.c` and rebuild `swap.bc`. Use `llvm_verify` +// to prove that `wacky_sort` satisfies the `selection_sort_spec` from Part 5 +// for `len=8`. Use overrides for all of the function calls within. + +// Remember: Use `w4_unint_z3` to leave Cryptol functions uninterpreted +// * w4_unint_z3 ["some_function"] diff --git a/exercises/functional-correctness/swap/solution/Swap.cry b/exercises/functional-correctness/swap/solution/Swap.cry new file mode 100644 index 0000000000..03833e637e --- /dev/null +++ b/exercises/functional-correctness/swap/solution/Swap.cry @@ -0,0 +1,29 @@ +module Swap where + +// Given a list and two indices, return a new list with the values at the +// indices swapped. +swap_list : {n} [n][32] -> [64] -> [64] -> [n][32] +swap_list lst i j = update (update lst i jval) j ival + where ival = lst @ i + jval = lst @ j + +argmin : {n} (fin n) => [n][32] -> [64] +argmin lst = + (foldl' min (-1 : [32], -1 : [64]) [(x, i) | x <- lst | i <- [0...]]).1 + +selection_sort : {n} (fin n, 64 >= width n) => [n][32] -> [n][32] +selection_sort lst = go`{0} lst + where + go : {idx} (fin idx, fin n, 64 >= width idx, 64 >= width n, n >= idx) => [n][32] -> [n][32] + go acc = + if `idx == `n + then acc + else go`{min n (idx + 1)} + (swap_list acc `idx (`idx + (argmin (drop`{idx} acc)))) + +// NOTE: Have to be careful. Just running :check on this will likely crash because a random index is likely out of bounds (especailly because `n will default to 0) +swap_list_same : {n} (fin n) => [64] -> [n][32] -> Bit +property swap_list_same i lst = (swap_list lst i i) == lst + +sort_eq : {n} (fin n, 64 >= width n) => [n][32] -> Bit +property sort_eq lst = selection_sort lst == sort lst diff --git a/exercises/functional-correctness/swap/solution/solution.saw b/exercises/functional-correctness/swap/solution/solution.saw new file mode 100644 index 0000000000..0756adafd3 --- /dev/null +++ b/exercises/functional-correctness/swap/solution/solution.saw @@ -0,0 +1,126 @@ +include "../../../common/helpers.saw"; +import "Swap.cry"; +swapmod <- llvm_load_module "swap.bc"; + +let swap_diff_spec = do { + // NOTE: Could use ptr_to_fresh instead + x <- llvm_fresh_var "x" (llvm_int 32); + xp <- llvm_alloc (llvm_int 32); + llvm_points_to xp (llvm_term x); + + y <- llvm_fresh_var "y" (llvm_int 32); + yp <- llvm_alloc (llvm_int 32); + llvm_points_to yp (llvm_term y); + + llvm_execute_func [xp, yp]; + + llvm_points_to yp (llvm_term x); + llvm_points_to xp (llvm_term y); +}; + +// Verify swap +swap_diff_ov <- llvm_verify swapmod "swap" [] true swap_diff_spec z3; + +let swap_same_spec = do { + (x, x_ptr) <- ptr_to_fresh "x" (llvm_int 32); + + llvm_execute_func [x_ptr, x_ptr]; + + llvm_points_to x_ptr (llvm_term x); +}; + +swap_same_ov <- llvm_verify swapmod "swap" [] true swap_same_spec z3; + +// Verify xor_swap +llvm_verify swapmod "xor_swap" [] true swap_diff_spec z3; + +let selection_sort_spec len = do { + (a, a_ptr) <- ptr_to_fresh "a" (llvm_array len (llvm_int 32)); + + llvm_execute_func [a_ptr, (llvm_term {{ `len : [64]}})]; + + llvm_points_to a_ptr (llvm_term {{ selection_sort a }}); +}; + +let a_len = 4; + +// Play with the `len` paramter for this exercise. At len=4 it solves quickly. +// At len=8, the term has blown up. Will it solve at all? +llvm_verify swapmod "selection_sort" [swap_diff_ov, swap_same_ov] true (selection_sort_spec a_len) (do { + //simplify (cryptol_ss()); + //print_goal; + z3; +}); + +// Now we crank a_len up and show the original proof blow up. How can we fix +// it? +let a_len = 8; + +let argmin_spec len = do { + // NOTE: Need to be careful to use "ptr_to_fresh_readonly" here. I + // originally made the mistake of making this a "ptr_to_fresh", which + // broke the input to swap afterwards by effectively wiping the array. + (a, a_ptr) <- ptr_to_fresh_readonly "a" (llvm_array len (llvm_int 32)); + + llvm_execute_func [a_ptr, (llvm_term {{ `len : [64]}})]; + + llvm_return (llvm_term {{ argmin a }}); +}; + +// NOTE: Another mistake I made was to use the override below. +// This works for size a_len, but on the second time through the loop the override +// doesn't match because the size of the list has changed! Ultimately need a +// loop here. +/* +argmin_ov <- llvm_verify swapmod "argmin" [] true (argmin_spec a_len) (do { + print_goal; + z3; +}); +*/ + +argmin_ovs <- for (eval_list {{ [1..a_len] : [a_len][64]}}) (\len -> + llvm_verify swapmod "argmin" [] true (argmin_spec (eval_int len)) z3 +); + +// NOTE: The reason we created a swap_array function was to get "swap_list" in +// our goal and reduce the number of ITEs, which in turn will help the solver +let swap_array_spec len = do { + (a, a_ptr) <- ptr_to_fresh "a" (llvm_array len (llvm_int 32)); + + i <- llvm_fresh_var "i" (llvm_int 64); + j <- llvm_fresh_var "j" (llvm_int 64); + + llvm_precond {{ i < `len }}; + llvm_precond {{ j < `len }}; + + llvm_execute_func [ a_ptr, llvm_term i, llvm_term j ]; + + llvm_points_to a_ptr (llvm_term {{ swap_list a i j }}); +}; + +swap_array_ov <- llvm_verify swapmod "swap_array" + [swap_diff_ov, swap_same_ov] + true + (swap_array_spec a_len) + (w4_unint_z3 []); + +sort_ov <- llvm_verify swapmod "selection_sort_composed" + (concat [swap_diff_ov, swap_same_ov, swap_array_ov] argmin_ovs) + true + (selection_sort_spec a_len) + (do { + //unfolding ["selection_sort"]; + //simplify (cryptol_ss()); + //print_goal; + w4_unint_z3 []; +}); + +llvm_verify swapmod "wacky_sort" + (concat argmin_ovs [sort_ov, swap_array_ov]) + true + (selection_sort_spec a_len) + (do { + //simplify (cryptol_ss()); + //print_goal; + w4_unint_z3 ["selection_sort"]; +}); diff --git a/exercises/functional-correctness/swap/solution/swap.c b/exercises/functional-correctness/swap/solution/swap.c new file mode 100644 index 0000000000..bdd7df707d --- /dev/null +++ b/exercises/functional-correctness/swap/solution/swap.c @@ -0,0 +1,57 @@ +#include +#include + +void swap(uint32_t *x, uint32_t *y) { + uint32_t tmp = *x; + *x = *y; + *y = tmp; +} + +void xor_swap(uint32_t *x, uint32_t *y) { + *x ^= *y; + *y ^= *x; + *x ^= *y; +} + +// selection sort +void selection_sort(uint32_t *a, size_t len) { + for (size_t i = 0; i < len - 1; ++i) { + size_t j_min = i; + for (size_t j = i; j < len; ++j) { + if (a[j] < a[j_min]) { + j_min = j; + } + } + swap(a+i, a+j_min); + } +} + +size_t argmin(const uint32_t *a, size_t len) { + size_t j_min = 0; + for (size_t j = 0; j < len; ++j) { + if (a[j] < a[j_min]) { + j_min = j; + } + } + return j_min; +} + +void swap_array(uint32_t *a, size_t i, size_t j) { + swap(a+i, a+j); +} + +void selection_sort_composed(uint32_t *a, size_t len) { + for (size_t i = 0; i < len - 1; ++i) { + size_t j_min = i + argmin(a+i, len-i); + swap_array(a, i, j_min); + } +} + +void wacky_sort(uint32_t *a, size_t len) { + for (size_t i = 0; i < 4; ++i) { + size_t swap_idx = (argmin(a, len) + i) % len; + swap_array(a, 0, swap_idx); + swap_array(a, 0, swap_idx); + } + selection_sort_composed(a, len); +} \ No newline at end of file diff --git a/exercises/functional-correctness/swap/swap.c b/exercises/functional-correctness/swap/swap.c new file mode 100644 index 0000000000..5fe37df64e --- /dev/null +++ b/exercises/functional-correctness/swap/swap.c @@ -0,0 +1,42 @@ +#include +#include + +void swap(uint32_t *x, uint32_t *y) { + uint32_t tmp = *x; + *x = *y; + *y = tmp; +} + +void xor_swap(uint32_t *x, uint32_t *y) { + *x ^= *y; + *y ^= *x; + *x ^= *y; +} + +// selection sort +void selection_sort(uint32_t *a, size_t len) { + for (size_t i = 0; i < len - 1; ++i) { + size_t j_min = i; + for (size_t j = i; j < len; ++j) { + if (a[j] < a[j_min]) { + j_min = j; + } + } + swap(a+i, a+j_min); + } +} + +// Leave wacky_sort commented out until told to uncomment +/* +void wacky_sort(uint32_t *a, size_t len) { + // This loop swaps values around a bunch, but after it is done `a` is + // unchanged. + for (size_t i = 0; i < 4; ++i) { + size_t swap_idx = (argmin(a, len) + i) % len; + swap_array(a, 0, swap_idx); + swap_array(a, 0, swap_idx); + } + + selection_sort_composed(a, len); +} +*/ \ No newline at end of file diff --git a/exercises/functional-correctness/u128/exercise.saw b/exercises/functional-correctness/u128/exercise.saw new file mode 100644 index 0000000000..b7d5ac21f5 --- /dev/null +++ b/exercises/functional-correctness/u128/exercise.saw @@ -0,0 +1,73 @@ +/////////////////////////////////////////////////////////////////////////////// +// Exercise: 128-bit Unsigned Int Functional Correctness +/////////////////////////////////////////////////////////////////////////////// + +include "../../common/helpers.saw"; + +m <- llvm_load_module "u128.bc"; + +/////////////////////////////////////////////////////////////////////////////// +// Part 1: Fix increment_u128 +/////////////////////////////////////////////////////////////////////////////// + +// Below you'll find a correct specification of increment_u128. However, the C +// implementation contains an error. To help diagnose the issue, uncomment the +// llvm_verify command and run SAW to see the error. +// Use `simplify (cryptol_ss())` and `print_goal` to aid in debugging. +// Correct the C code, recompile `u128.bc`, and verify that the proof goes +// through. + +let increment_u128_spec = do { + (x, x_ptr) <- ptr_to_fresh "x" (llvm_int 128); + + llvm_execute_func [x_ptr]; + + llvm_points_to x_ptr (llvm_term {{ x + 1 }}); +}; + +/* +llvm_verify m "increment_u128" + [] + true + increment_u128_spec + z3; +*/ + +//////////////////////////////////////////////////////////////////////////////// +// Part 2: eq_u128 proofs +//////////////////////////////////////////////////////////////////////////////// + +// Turn the memory safety specs below into functional correctness specs. Ensure +// the corresponding llvm_verify command passes. To simplify the specs, you may +// assume that bcmp returns 1 for non-equal inputs. + +// "The bcmp() function compares the two byte sequences s1 and s2 of length n +// each. If they are equal, and in particular if n is zero, bcmp() returns 0. +// Otherwise it returns a nonzero result." +let bcmp_spec size = do { + (s1, s1_ptr) <- ptr_to_fresh_readonly "s1" (llvm_array size (llvm_int 8)); + (s2, s2_ptr) <- ptr_to_fresh_readonly "s2" (llvm_array size (llvm_int 8)); + + llvm_execute_func [ s1_ptr, s2_ptr, llvm_term {{ `size : [64]}} ]; + + ret <- llvm_fresh_var "ret" (llvm_int 32); + llvm_return (llvm_term ret); +}; + +bcmp_16_ov <- llvm_unsafe_assume_spec m "bcmp" (bcmp_spec 16); + +let eq_u128_spec = do { + (x, x_ptr) <- ptr_to_fresh_readonly "x" (llvm_int 128); + (y, y_ptr) <- ptr_to_fresh_readonly "y" (llvm_int 128); + + llvm_execute_func [x_ptr, y_ptr]; + + ret <- llvm_fresh_var "ret" (llvm_int 1); + llvm_return (llvm_term ret); +}; + +llvm_verify m "eq_u128" + [bcmp_16_ov] + true + eq_u128_spec + z3; diff --git a/exercises/functional-correctness/u128/solution.saw b/exercises/functional-correctness/u128/solution.saw new file mode 100644 index 0000000000..75d6c07a8b --- /dev/null +++ b/exercises/functional-correctness/u128/solution.saw @@ -0,0 +1,62 @@ +include "../../common/helpers.saw"; + +m <- llvm_load_module "u128.bc"; + +let increment_u128_spec = do { + (x, x_ptr) <- ptr_to_fresh "x" (llvm_int 128); + + llvm_execute_func [x_ptr]; + + llvm_points_to x_ptr (llvm_term {{ x + 1 }}); +}; + +// NOTE: Solution below is commented out because you need to fix the C code by +// changing `x[1]` to `x[0]` on line 7, and `x[0]` to `x[1]` on line 8. Then +// the proof below will go through. +/* +llvm_verify m "increment_u128" + [] + true + increment_u128_spec + (do { + simplify (cryptol_ss()); + print_goal; + w4_unint_z3 []; +}); +*/ + +//////////////////////////////////////////////////////////////////////////////// +// eq_u128 proofs +//////////////////////////////////////////////////////////////////////////////// + +// "The bcmp() function compares the two byte sequences s1 and s2 of length n +// each. If they are equal, and in particular if n is zero, bcmp() returns 0. +// Otherwise it returns a nonzero result." +let bcmp_spec size = do { + (s1, s1_ptr) <- ptr_to_fresh "s1" (llvm_array size (llvm_int 8)); + (s2, s2_ptr) <- ptr_to_fresh "s2" (llvm_array size (llvm_int 8)); + + llvm_execute_func [ s1_ptr, s2_ptr, llvm_term {{ `size : [64]}} ]; + + llvm_return (llvm_term {{ zext`{32} [s1 != s2] }}); +}; + +bcmp_16_ov <- llvm_unsafe_assume_spec m "bcmp" (bcmp_spec 16); + +let eq_u128_spec = do { + (x, x_ptr) <- ptr_to_fresh "x" (llvm_int 128); + (y, y_ptr) <- ptr_to_fresh "y" (llvm_int 128); + + llvm_execute_func [x_ptr, y_ptr]; + + llvm_return (llvm_term {{ [x == y] : [1] }}); +}; + +llvm_verify m "eq_u128" + [bcmp_16_ov] + true + eq_u128_spec + (do { + //print_goal; + w4_unint_z3 []; +}); diff --git a/exercises/functional-correctness/u128/u128.c b/exercises/functional-correctness/u128/u128.c new file mode 100644 index 0000000000..d18bc2c533 --- /dev/null +++ b/exercises/functional-correctness/u128/u128.c @@ -0,0 +1,14 @@ +#include +#include +#include +#include + +void increment_u128(uint64_t x[2]) { + if (++x[1] == 0) { + ++x[0]; + } +} + +bool eq_u128(uint64_t x[2], uint64_t y[2]) { + return !bcmp(x, y, 16); +} \ No newline at end of file diff --git a/exercises/memory-safety/complete-examples/add/add.c b/exercises/memory-safety/complete-examples/add/add.c new file mode 100644 index 0000000000..2b9cea2b3a --- /dev/null +++ b/exercises/memory-safety/complete-examples/add/add.c @@ -0,0 +1,3 @@ +#include + +uint32_t add(uint32_t x, uint32_t y) { return x + y; } \ No newline at end of file diff --git a/exercises/memory-safety/complete-examples/add/solution.saw b/exercises/memory-safety/complete-examples/add/solution.saw new file mode 100644 index 0000000000..22cc5c5288 --- /dev/null +++ b/exercises/memory-safety/complete-examples/add/solution.saw @@ -0,0 +1,18 @@ +let add_spec = do { + // Create fresh variables for `x` and `y` + x <- llvm_fresh_var "x" (llvm_int 32); + y <- llvm_fresh_var "y" (llvm_int 32); + + // Invoke the function with the fresh variables + llvm_execute_func [llvm_term x, llvm_term y]; + + // The function returns another 32 bit value at a different memory location from `x` and `y` + ret <- llvm_fresh_var "ret" (llvm_int 32); + llvm_return ( llvm_term ret ); +}; + +// Load LLVM bitcode to verify +m <- llvm_load_module "add.bc"; + +// Verify the `add` function satisfies its specification +llvm_verify m "add" [] true add_spec z3; \ No newline at end of file diff --git a/exercises/memory-safety/point/exercise.saw b/exercises/memory-safety/point/exercise.saw new file mode 100644 index 0000000000..5ede25d626 --- /dev/null +++ b/exercises/memory-safety/point/exercise.saw @@ -0,0 +1,28 @@ +//////////////////////////////////////////////////////////////////////////////// +// Exercise: Points +//////////////////////////////////////////////////////////////////////////////// + +include "../../common/helpers.saw"; + +//////////////////////////////////////////////////////////////////////////////// +// Part 1: Structs +//////////////////////////////////////////////////////////////////////////////// + +// Write memory safety specs and proofs for point_eq, point_new, and point_copy. +// Use the override your point_new proof returns in your point_copy proof. + +// Remember: You can declare struct types with: +// llvm_struct "struct." + +//////////////////////////////////////////////////////////////////////////////// +// Part 2: Global Variables +//////////////////////////////////////////////////////////////////////////////// + +// Write the memory safety spec and proof for point_add. Use overrides from +// all of the proofs from part 1 here. Initially write the spec without +// initializing the global variable `ZERO`. Familiarize yourself with the +// error message. Then, fix your spec and re-run the proof. + +// Useful commands: +// Declare a global: llvm_alloc_global "" +// Get a pointer to a global: llvm_global "" diff --git a/exercises/memory-safety/point/point.c b/exercises/memory-safety/point/point.c new file mode 100644 index 0000000000..fceb9684f9 --- /dev/null +++ b/exercises/memory-safety/point/point.c @@ -0,0 +1,38 @@ +#include +#include +#include + +typedef struct point { + uint32_t x; + uint32_t y; +} point; + +point ZERO = {0, 0}; + +bool point_eq(const point *p1, const point *p2) { + return p1->x == p2->x && p1->y == p2-> y; +} + +point* point_new(uint32_t x, uint32_t y) { + point* ret = malloc(sizeof(point)); + ret->x = x; + ret->y = y; + return ret; +} + +point* point_copy(const point* p) { + return point_new(p->x, p->y); +} + +point* point_add(const point *p1, const point *p2) { + // Save an addition by checking for zero + if (point_eq(p1, &ZERO)) { + return point_copy(p2); + } + + if (point_eq(p2, &ZERO)) { + return point_copy(p1); + } + + return point_new(p1->x + p2->x, p1->y + p2->y); +} \ No newline at end of file diff --git a/exercises/memory-safety/point/solution.saw b/exercises/memory-safety/point/solution.saw new file mode 100644 index 0000000000..16b9b573eb --- /dev/null +++ b/exercises/memory-safety/point/solution.saw @@ -0,0 +1,64 @@ +include "../../common/helpers.saw"; + +m <- llvm_load_module "point.bc"; + +let point_eq_spec = do { + (p1, p1_ptr) <- ptr_to_fresh_readonly "p1" (llvm_struct "struct.point"); + (p2, p2_ptr) <- ptr_to_fresh_readonly "p2" (llvm_struct "struct.point"); + + llvm_execute_func [p1_ptr, p2_ptr]; + + ret <- llvm_fresh_var "ret" (llvm_int 1); + llvm_return (llvm_term ret); +}; + +point_eq_ov <- llvm_verify m "point_eq" [] true + point_eq_spec + (w4_unint_z3 []); + +let point_new_spec = do { + p_x <- llvm_fresh_var "p_x" (llvm_int 32); + p_y <- llvm_fresh_var "p_y" (llvm_int 32); + + llvm_execute_func [ llvm_term p_x, llvm_term p_y ]; + + (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_struct "struct.point"); + llvm_return ret_ptr; +}; + +point_new_ov <- llvm_verify m "point_new" [] true + point_new_spec + (w4_unint_z3 []); + +let point_copy_spec = do { + (p, p_ptr) <- ptr_to_fresh_readonly "p" (llvm_struct "struct.point"); + + llvm_execute_func [p_ptr]; + + (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_struct "struct.point"); + llvm_return ret_ptr; +}; + +point_copy_ov <- llvm_verify m "point_copy" [point_new_ov] true + point_copy_spec + (w4_unint_z3 []); + +let point_add_spec = do { + llvm_alloc_global "ZERO"; + zero_global <- llvm_fresh_var "zero_global" (llvm_struct "struct.point"); + llvm_points_to (llvm_global "ZERO") (llvm_term zero_global); + + (p1, p1_ptr) <- ptr_to_fresh_readonly "p1" (llvm_struct "struct.point"); + (p2, p2_ptr) <- ptr_to_fresh_readonly "p2" (llvm_struct "struct.point"); + + llvm_execute_func [p1_ptr, p2_ptr]; + + (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_struct "struct.point"); + llvm_return ret_ptr; +}; + +llvm_verify m "point_add" + [point_new_ov, point_copy_ov, point_eq_ov] + true + point_add_spec + (w4_unint_z3 []); diff --git a/exercises/memory-safety/popcount/exercise.saw b/exercises/memory-safety/popcount/exercise.saw new file mode 100644 index 0000000000..fcab362a4a --- /dev/null +++ b/exercises/memory-safety/popcount/exercise.saw @@ -0,0 +1,23 @@ +/////////////////////////////////////////////////////////////////////////////// +// Exercise: Popcount memory safety +/////////////////////////////////////////////////////////////////////////////// + +/////////////////////////////////////////////////////////////////////////////// +// Part 1: Popcount spec +/////////////////////////////////////////////////////////////////////////////// + +// Write a SAW memory safety specification for popcount. Use the "add" example +// as a guide. Before continuing on to the next part, load this file in SAW to +// check for any syntax errors. If all is successful, you should see something +// like: +// +// [00:47:16.610] Loading file "/workspaces/exercises/memory-safety/popcount/exercise.saw" +// +// with no further output. + +/////////////////////////////////////////////////////////////////////////////// +// Part 2: Popcount proof +/////////////////////////////////////////////////////////////////////////////// + +// Now prove that all of the popcount C implementations satisfy your +// specification. Again, use the "add" example as a guide. diff --git a/exercises/memory-safety/popcount/popcount.c b/exercises/memory-safety/popcount/popcount.c new file mode 100644 index 0000000000..ea2afe430a --- /dev/null +++ b/exercises/memory-safety/popcount/popcount.c @@ -0,0 +1,33 @@ +#include + +/* + * Returns a count of the set bits in a word. + * From Henry S. Warren Jr.'s Hacker's Delight + */ +int pop_count(uint32_t x) { + x = x - ((x >> 1) & 0x55555555); + x = (x & 0x33333333) + ((x >> 2) & 0x33333333); + x = (x + (x >> 4)) & 0x0F0F0F0F; + x = x + (x >> 8); + x = x + (x >> 16); + return x & 0x0000003F; +} + +/* A version of popcount that uses multiplication */ +int pop_count_mul(uint32_t x) { + x = x - ((x >> 1) & 0x55555555); + x = (x & 0x33333333) + ((x >> 2) & 0x33333333); + x = ((x + (x >> 4)) & 0x0F0F0F0F); + return (x * 0x01010101) >> 24; +} + +/* A version of popcount that uses an indefinite while loop(!) */ +int pop_count_sparse(uint32_t x) { + int n; + n = 0; + while (x != 0) { + n = n + 1; + x = x & (x - 1); + } + return n; +} \ No newline at end of file diff --git a/exercises/memory-safety/popcount/solution.saw b/exercises/memory-safety/popcount/solution.saw new file mode 100644 index 0000000000..3502f561a9 --- /dev/null +++ b/exercises/memory-safety/popcount/solution.saw @@ -0,0 +1,18 @@ +popmod <- llvm_load_module "popcount.bc"; + +let pop_cryptol_check = do { + x <- llvm_fresh_var "x" (llvm_int 32); + llvm_execute_func [llvm_term x]; + ret <- llvm_fresh_var "ret" (llvm_int 32); + llvm_return ( llvm_term ret ); +}; + +// same verification against Cryptol spec +llvm_verify popmod "pop_count" [] true pop_cryptol_check yices; + +// Begin Cryptol additional verifications +// another tricky implementation +llvm_verify popmod "pop_count_mul" [] true pop_cryptol_check yices; + +// verify the while loop version +llvm_verify popmod "pop_count_sparse" [] true pop_cryptol_check yices; diff --git a/exercises/memory-safety/salsa20/salsa20.c b/exercises/memory-safety/salsa20/salsa20.c new file mode 100644 index 0000000000..d7530c15ff --- /dev/null +++ b/exercises/memory-safety/salsa20/salsa20.c @@ -0,0 +1,189 @@ +#include +#include +#include "salsa20.h" + +// Implements DJB's definition of '<<<' +static uint32_t rotl(uint32_t value, int shift) +{ + return (value << shift) | (value >> (32 - shift)); +} + +static void s20_quarterround(uint32_t *y0, uint32_t *y1, uint32_t *y2, uint32_t *y3) +{ + *y1 = *y1 ^ rotl(*y0 + *y3, 7); + *y2 = *y2 ^ rotl(*y1 + *y0, 9); + *y3 = *y3 ^ rotl(*y2 + *y1, 13); + *y0 = *y0 ^ rotl(*y3 + *y2, 18); +} + +static void s20_rowround(uint32_t y[static 16]) +{ + s20_quarterround(&y[0], &y[1], &y[2], &y[3]); + s20_quarterround(&y[5], &y[6], &y[7], &y[4]); + s20_quarterround(&y[10], &y[11], &y[8], &y[9]); + s20_quarterround(&y[15], &y[12], &y[13], &y[14]); +} + +static void s20_columnround(uint32_t x[static 16]) +{ + s20_quarterround(&x[0], &x[4], &x[8], &x[12]); + s20_quarterround(&x[5], &x[9], &x[13], &x[1]); + s20_quarterround(&x[10], &x[14], &x[2], &x[6]); + s20_quarterround(&x[15], &x[3], &x[7], &x[11]); +} + +static void s20_doubleround(uint32_t x[static 16]) +{ + s20_columnround(x); + s20_rowround(x); +} + +// Creates a little-endian word from 4 bytes pointed to by b +static uint32_t s20_littleendian(uint8_t *b) +{ + return b[0] + + (b[1] << 8) + + (b[2] << 16) + + (b[3] << 24); +} + +// Moves the little-endian word into the 4 bytes pointed to by b +static void s20_rev_littleendian(uint8_t *b, uint32_t w) +{ + b[0] = w; + b[1] = w >> 8; + b[2] = w >> 16; + b[3] = w >> 24; +} + +// The core function of Salsa20 +static void s20_hash(uint8_t seq[static 64]) +{ + int i; + uint32_t x[16]; + uint32_t z[16]; + + // Create two copies of the state in little-endian format + // First copy is hashed together + // Second copy is added to first, word-by-word + for (i = 0; i < 16; ++i) + x[i] = z[i] = s20_littleendian(seq + (4 * i)); + + for (i = 0; i < 10; ++i) + s20_doubleround(z); + + for (i = 0; i < 16; ++i) { + z[i] += x[i]; + s20_rev_littleendian(seq + (4 * i), z[i]); + } +} + +// The 16-byte (128-bit) key expansion function +static void s20_expand16(uint8_t *k, + uint8_t n[static 16], + uint8_t keystream[static 64]) +{ + int i, j; + // The constants specified by the Salsa20 specification, 'tau' + // "expand 16-byte k" + uint8_t t[4][4] = { + { 'e', 'x', 'p', 'a' }, + { 'n', 'd', ' ', '1' }, + { '6', '-', 'b', 'y' }, + { 't', 'e', ' ', 'k' } + }; + + // Copy all of 'tau' into the correct spots in our keystream block + for (i = 0; i < 64; i += 20) + for (j = 0; j < 4; ++j) + keystream[i + j] = t[i / 20][j]; + + // Copy the key and the nonce into the keystream block + for (i = 0; i < 16; ++i) { + keystream[4+i] = k[i]; + keystream[44+i] = k[i]; + keystream[24+i] = n[i]; + } + + s20_hash(keystream); +} + +// The 32-byte (256-bit) key expansion function +static void s20_expand32(uint8_t *k, + uint8_t n[static 16], + uint8_t keystream[static 64]) +{ + int i, j; + // The constants specified by the Salsa20 specification, 'sigma' + // "expand 32-byte k" + uint8_t o[4][4] = { + { 'e', 'x', 'p', 'a' }, + { 'n', 'd', ' ', '3' }, + { '2', '-', 'b', 'y' }, + { 't', 'e', ' ', 'k' } + }; + + // Copy all of 'sigma' into the correct spots in our keystream block + for (i = 0; i < 64; i += 20) + for (j = 0; j < 4; ++j) + keystream[i + j] = o[i / 20][j]; + + // Copy the key and the nonce into the keystream block + for (i = 0; i < 16; ++i) { + keystream[4+i] = k[i]; + keystream[44+i] = k[i+16]; + keystream[24+i] = n[i]; + } + + s20_hash(keystream); +} + +// Performs up to 2^32-1 bytes of encryption or decryption under a +// 128- or 256-bit key. +enum s20_status_t s20_crypt32(uint8_t *key, + uint8_t nonce[static 8], + uint32_t si, + uint8_t *buf, + uint32_t buflen) +{ + uint8_t keystream[64]; + // 'n' is the 8-byte nonce (unique message number) concatenated + // with the per-block 'counter' value (4 bytes in our case, 8 bytes + // in the standard). We leave the high 4 bytes set to zero because + // we permit only a 32-bit integer for stream index and length. + uint8_t n[16] = { 0 }; + uint32_t i; + + // If any of the parameters we received are invalid + if (key == NULL || nonce == NULL || buf == NULL) + return S20_FAILURE; + + // Set up the low 8 bytes of n with the unique message number + for (i = 0; i < 8; ++i) + n[i] = nonce[i]; + + // If we're not on a block boundary, compute the first keystream + // block. This will make the primary loop (below) cleaner + if (si % 64 != 0) { + // Set the second-to-highest 4 bytes of n to the block number + s20_rev_littleendian(n+8, si / 64); + // Expand the key with n and hash to produce a keystream block + s20_expand32(key, n, keystream); + } + + // Walk over the plaintext byte-by-byte, xoring the keystream with + // the plaintext and producing new keystream blocks as needed + for (i = 0; i < buflen; ++i) { + // If we've used up our entire keystream block (or have just begun + // and happen to be on a block boundary), produce keystream block + if ((si + i) % 64 == 0) { + s20_rev_littleendian(n+8, ((si + i) / 64)); + s20_expand32(key, n, keystream); + } + + // xor one byte of plaintext with one byte of keystream + buf[i] ^= keystream[(si + i) % 64]; + } + + return S20_SUCCESS; +} diff --git a/exercises/memory-safety/salsa20/salsa20.h b/exercises/memory-safety/salsa20/salsa20.h new file mode 100644 index 0000000000..df94eed6b1 --- /dev/null +++ b/exercises/memory-safety/salsa20/salsa20.h @@ -0,0 +1,72 @@ +#ifndef _SALSA20_H_ +#define _SALSA20_H_ + +#include +#include + +/** + * Return codes for s20_crypt + */ +enum s20_status_t +{ + S20_SUCCESS, + S20_FAILURE +}; + +/** + * Key size + * Salsa20 only permits a 128-bit key or a 256-bit key, so these are + * the only two options made available by this library. + */ +enum s20_keylen_t +{ + S20_KEYLEN_256, + S20_KEYLEN_128 +}; + +/** + * Performs up to 2^32-1 bytes of encryption or decryption under a + * 128- or 256-bit key in blocks of arbitrary size. Permits seeking + * to any point within a stream. + * + * key Pointer to either a 128-bit or 256-bit key. + * No key-derivation function is applied to this key, and no + * entropy is gathered. It is expected that this key is already + * appropriate for direct use by the Salsa20 algorithm. + * + * keylen Length of the key. + * Must be S20_KEYLEN_256 or S20_KEYLEN_128. + * + * nonce Pointer to an 8-byte nonce. + * Does not have to be random, but must be unique for every + * message under a single key. Nonce reuse destroys message + * confidentiality. + * + * si Stream index. + * The position within the stream. When encrypting/decrypting + * a message sequentially from beginning to end in fixed-size + * chunks of length L, this value is increased by L on every + * call. Care must be taken not to select values that cause + * overlap. Example: encrypting 1000 bytes at index 100, and + * then encrypting 1000 bytes at index 500. Doing so will + * result in keystream reuse, which destroys message + * confidentiality. + * + * buf The data to encrypt or decrypt. + * + * buflen Length of the data in buf. + * + * This function returns either S20_SUCCESS or S20_FAILURE. + * A return of S20_SUCCESS indicates that basic sanity checking on + * parameters succeeded and encryption/decryption was performed. + * A return of S20_FAILURE indicates that basic sanity checking on + * parameters failed and encryption/decryption was not performed. + */ +enum s20_status_t s20_crypt(uint8_t *key, + enum s20_keylen_t keylen, + uint8_t nonce[static 8], + uint32_t si, + uint8_t *buf, + uint32_t buflen); + +#endif diff --git a/exercises/memory-safety/salsa20/solution.saw b/exercises/memory-safety/salsa20/solution.saw new file mode 100644 index 0000000000..32574299b2 --- /dev/null +++ b/exercises/memory-safety/salsa20/solution.saw @@ -0,0 +1,81 @@ +include "../../common/helpers.saw"; + +let oneptr_update_func (type : LLVMType) (name : String) = do { + (x, p) <- ptr_to_fresh name type; + llvm_execute_func [p]; + x' <- llvm_fresh_var (str_concat name "'") type; + llvm_points_to p (llvm_term x'); +}; + +let quarterround_setup : CrucibleSetup () = do { + (y0, p0) <- ptr_to_fresh "y0" (llvm_int 32); + (y1, p1) <- ptr_to_fresh "y1" (llvm_int 32); + (y2, p2) <- ptr_to_fresh "y2" (llvm_int 32); + (y3, p3) <- ptr_to_fresh "y3" (llvm_int 32); + + llvm_execute_func [p0, p1, p2, p3]; + + y0' <- llvm_fresh_var "y0'" (llvm_int 32); + y1' <- llvm_fresh_var "y1'" (llvm_int 32); + y2' <- llvm_fresh_var "y2'" (llvm_int 32); + y3' <- llvm_fresh_var "y3'" (llvm_int 32); + + llvm_points_to p0 (llvm_term y0'); + llvm_points_to p1 (llvm_term y1'); + llvm_points_to p2 (llvm_term y2'); + llvm_points_to p3 (llvm_term y3'); +}; + +let rowround_setup = + oneptr_update_func (llvm_array 16 (llvm_int 32)) "y"; + +let columnround_setup = + oneptr_update_func (llvm_array 16 (llvm_int 32)) "x"; + +let doubleround_setup = + oneptr_update_func (llvm_array 16 (llvm_int 32)) "x"; + +let salsa20_setup = + oneptr_update_func (llvm_array 64 (llvm_int 8)) "seq"; + +let salsa20_expansion_32 = do { + (n, pn) <- ptr_to_fresh_readonly "n" (llvm_array 16 (llvm_int 8)); + (k, pk) <- ptr_to_fresh_readonly "k" (llvm_array 32 (llvm_int 8)); + + pks <- llvm_alloc (llvm_array 64 (llvm_int 8)); + + llvm_execute_func [pk, pn, pks]; + + rks <- llvm_fresh_var "rks" (llvm_array 64 (llvm_int 8)); + llvm_points_to pks (llvm_term rks); +}; + +let s20_encrypt32 n = do { + (key, pkey) <- ptr_to_fresh_readonly "key" (llvm_array 32 (llvm_int 8)); + (v, pv) <- ptr_to_fresh_readonly "nonce" (llvm_array 8 (llvm_int 8)); + (m, pm) <- ptr_to_fresh "buf" (llvm_array n (llvm_int 8)); + + llvm_execute_func [ pkey + , pv + , llvm_term {{ 0 : [32] }} + , pm + , llvm_term {{ `n : [32] }} + ]; + + m' <- llvm_fresh_var "m'" (llvm_array n (llvm_int 8)); + llvm_points_to pm (llvm_term m'); + + ret <- llvm_fresh_var "ret" (llvm_int 32); + llvm_return (llvm_term ret); +}; + +m <- llvm_load_module "salsa20.bc"; +qr <- llvm_verify m "s20_quarterround" [] true quarterround_setup z3; +rr <- llvm_verify m "s20_rowround" [qr] true rowround_setup z3; +cr <- llvm_verify m "s20_columnround" [qr] true columnround_setup z3; +dr <- llvm_verify m "s20_doubleround" [cr,rr] true doubleround_setup z3; +s20 <- llvm_verify m "s20_hash" [dr] true salsa20_setup z3; +s20e32 <- llvm_verify m "s20_expand32" [s20] true salsa20_expansion_32 z3; +s20encrypt_63 <- llvm_verify m "s20_crypt32" [s20e32] true (s20_encrypt32 63) z3; +s20encrypt_64 <- llvm_verify m "s20_crypt32" [s20e32] true (s20_encrypt32 64) z3; +s20encrypt_65 <- llvm_verify m "s20_crypt32" [s20e32] true (s20_encrypt32 65) z3; diff --git a/exercises/memory-safety/swap/exercise.saw b/exercises/memory-safety/swap/exercise.saw new file mode 100644 index 0000000000..037b8f6780 --- /dev/null +++ b/exercises/memory-safety/swap/exercise.saw @@ -0,0 +1,79 @@ +/////////////////////////////////////////////////////////////////////////////// +// Exercise: Swap Memory Safety +/////////////////////////////////////////////////////////////////////////////// + +// `include` in SAW works like #include in C: it inlines the contents of the +// included file. +include "../../common/helpers.saw"; + +/////////////////////////////////////////////////////////////////////////////// +// Part 1: Swap Different Pointers Spec +/////////////////////////////////////////////////////////////////////////////// + +// Write a memory safety spec for `swap`. Assume that the caller passes in two +// different pointers for both arguments. Use `ptr_to_fresh` from +// `helpers.saw` in your specification. Feel free to use both the `add` example +// and your `popcount` exercises as a guide! + +/////////////////////////////////////////////////////////////////////////////// +// Part 2: Swap Different Pointers Proofs +/////////////////////////////////////////////////////////////////////////////// + +// Use `llvm_verify` to prove that `swap` and `xor_swap` both satisfy your SAW +// spec. You will need to use separate invocations of `llvm_verify` for each +// proof. + +/////////////////////////////////////////////////////////////////////////////// +// Part 3: Swap Same Pointers Spec +/////////////////////////////////////////////////////////////////////////////// + +// Write a memory safety spec for `swap` like in part 1, but this time, assume +// that the caller passes in the same pointer for both arguments. + +/////////////////////////////////////////////////////////////////////////////// +// Part 4: Swap Same Pointers Proofs +/////////////////////////////////////////////////////////////////////////////// + +// Use `llvm_verify` to prove that `swap` satisfies the spec you wrote in part +// 3. + +/////////////////////////////////////////////////////////////////////////////// +// Part 5: Selection Sort Spec +/////////////////////////////////////////////////////////////////////////////// + +// Uncomment and fill in in the parameterized memory safety proof for selection sort below +// Remember: +// * Use `llvm_array ` to specify an array type +// * Use `{{ }}` to inline Cryptol +// * SAW function parameters are Cryptol type variables + +/* +let selection_sort_spec size = do { + +}; +*/ + +/////////////////////////////////////////////////////////////////////////////// +// Part 6: Selection Sort Proofs +/////////////////////////////////////////////////////////////////////////////// + +// Prove `selection_sort` satisfies `selection_sort_spec` for `size` values of +// 2, 3, and 8. + + +/////////////////////////////////////////////////////////////////////////////// +// Part 7: Selection Sort Proof Composition +/////////////////////////////////////////////////////////////////////////////// + +// Modify your selection sort proof to use your `swap` proofs as overrides. +// How does this change SAW's output? + + +/////////////////////////////////////////////////////////////////////////////// +// Part 8: Selection Sort Errors +/////////////////////////////////////////////////////////////////////////////// + +// Introduce a memory error into the selection_sort C implementation (for +// example, causing an out-of-bounds write) and rebuild `swap.bc`. What +// happens now when you run your proof? Can you fool SAW with a memory error +// it fails to detect? diff --git a/exercises/memory-safety/swap/solution.saw b/exercises/memory-safety/swap/solution.saw new file mode 100644 index 0000000000..e176290063 --- /dev/null +++ b/exercises/memory-safety/swap/solution.saw @@ -0,0 +1,80 @@ +include "../../common/helpers.saw"; +swapmod <- llvm_load_module "swap.bc"; + +/////////////////////////////////////////////////////////////////////////////// +// Part 1: Swap Different Pointers Spec +/////////////////////////////////////////////////////////////////////////////// + +let swap_diff_spec = do { + (x, xp) <- ptr_to_fresh "x" (llvm_int 32); + (y, yp) <- ptr_to_fresh "y" (llvm_int 32); + + llvm_execute_func [xp, yp]; + + x' <- llvm_fresh_var "x'" (llvm_int 32); + y' <- llvm_fresh_var "y'" (llvm_int 32); + + llvm_points_to xp (llvm_term x'); + llvm_points_to yp (llvm_term y'); +}; + +/////////////////////////////////////////////////////////////////////////////// +// Part 2: Swap Different Pointers Proofs +/////////////////////////////////////////////////////////////////////////////// + +// Verify swap +swap_diff_ov <- llvm_verify swapmod "swap" [] true swap_diff_spec z3; + +// Verify xor_swap +llvm_verify swapmod "xor_swap" [] true swap_diff_spec z3; + +/////////////////////////////////////////////////////////////////////////////// +// Part 3: Swap Same Pointers Spec +/////////////////////////////////////////////////////////////////////////////// + +let swap_same_spec = do { + (x, xp) <- ptr_to_fresh "x" (llvm_int 32); + + llvm_execute_func [xp, xp]; + + x' <- llvm_fresh_var "x'" (llvm_int 32); + llvm_points_to xp (llvm_term x'); +}; + +/////////////////////////////////////////////////////////////////////////////// +// Part 4: Swap Same Pointers Proofs +/////////////////////////////////////////////////////////////////////////////// + +swap_same_ov <- llvm_verify swapmod "swap" [] true swap_same_spec z3; + +/////////////////////////////////////////////////////////////////////////////// +// Part 5: Selection Sort Spec +/////////////////////////////////////////////////////////////////////////////// + +let selection_sort_spec len = do { + (a, a_ptr) <- ptr_to_fresh "a" (llvm_array len (llvm_int 32)); + + llvm_execute_func [a_ptr, (llvm_term {{ `len : [64]}})]; + + a' <- llvm_fresh_var "a'" (llvm_array len (llvm_int 32)); + + llvm_points_to a_ptr (llvm_term a'); +}; + +llvm_verify swapmod "selection_sort" [swap_diff_ov, swap_same_ov] true (selection_sort_spec 2) (do { + //simplify (cryptol_ss()); + //print_goal; + z3; +}); + +llvm_verify swapmod "selection_sort" [swap_diff_ov, swap_same_ov] true (selection_sort_spec 3) (do { + //simplify (cryptol_ss()); + //print_goal; + z3; +}); + +llvm_verify swapmod "selection_sort" [swap_diff_ov, swap_same_ov] true (selection_sort_spec 8) (do { + //simplify (cryptol_ss()); + //print_goal; + z3; +}); diff --git a/exercises/memory-safety/swap/swap.c b/exercises/memory-safety/swap/swap.c new file mode 100644 index 0000000000..b1d9d9cac5 --- /dev/null +++ b/exercises/memory-safety/swap/swap.c @@ -0,0 +1,29 @@ +#include +#include + +// Swap two pointers using a temporary variable +void swap(uint32_t *x, uint32_t *y) { + uint32_t tmp = *x; + *x = *y; + *y = tmp; +} + +// Swap two pointers using XOR +void xor_swap(uint32_t *x, uint32_t *y) { + *x ^= *y; + *y ^= *x; + *x ^= *y; +} + +// selection sort on an array `a` with `len` elements +void selection_sort(uint32_t *a, size_t len) { + for (size_t i = 0; i < len - 1; ++i) { + size_t j_min = i; + for (size_t j = i; j < len; ++j) { + if (a[j] < a[j_min]) { + j_min = j; + } + } + swap(a+i, a+j_min); + } +} \ No newline at end of file diff --git a/exercises/memory-safety/u128/exercise.saw b/exercises/memory-safety/u128/exercise.saw new file mode 100644 index 0000000000..6b16b92e8c --- /dev/null +++ b/exercises/memory-safety/u128/exercise.saw @@ -0,0 +1,42 @@ +/////////////////////////////////////////////////////////////////////////////// +// Exercise: 128-bit Unsigned Int Memory Safety +/////////////////////////////////////////////////////////////////////////////// + +include "../../common/helpers.saw"; + +m <- llvm_load_module "u128.bc"; + +/////////////////////////////////////////////////////////////////////////////// +// Part 1: increment_u128 +/////////////////////////////////////////////////////////////////////////////// + +// Write a memory safety spec for increment_u128 that interprets its input +// argument as a single 128-bit integer, rather than an array. Prove that the C +// function satisfies your specification + +/////////////////////////////////////////////////////////////////////////////// +// Part 2: eq_u128 error +/////////////////////////////////////////////////////////////////////////////// + +// Below you'll find a specification for eq_u128. However, uncommenting the +// `llvm_verify` command yields an error. Why? Fix the proof. + +let eq_u128_spec = do { + (x, x_ptr) <- ptr_to_fresh "x" (llvm_int 128); + (y, y_ptr) <- ptr_to_fresh "y" (llvm_int 128); + + llvm_execute_func [x_ptr, y_ptr]; + + // NOTE: A C `bool` has type `llvm_int 1`. + ret <- llvm_fresh_var "ret" (llvm_int 1); + llvm_return (llvm_term ret); +}; + +// llvm_verify m "eq_u128" [] true eq_u128_spec z3; + +/////////////////////////////////////////////////////////////////////////////// +// Part 3: eq_u128 Readonly Arguments +/////////////////////////////////////////////////////////////////////////////// + +// Adapt your specs from Part 2 to make use of readonly pointers. Check that +// you did so correctly by re-running your eq_u128 proof. diff --git a/exercises/memory-safety/u128/solution.saw b/exercises/memory-safety/u128/solution.saw new file mode 100644 index 0000000000..601d12ca87 --- /dev/null +++ b/exercises/memory-safety/u128/solution.saw @@ -0,0 +1,58 @@ +include "../../common/helpers.saw"; + +m <- llvm_load_module "u128.bc"; + +// The interesting thing about this is that we can model it as a 128-bit int directly in Cryptol! Not an array of 2 64-bit ints. +let increment_u128_spec = do { + (x, x_ptr) <- ptr_to_fresh "x" (llvm_int 128); + + llvm_execute_func [x_ptr]; + + x' <- llvm_fresh_var "x'" (llvm_int 128); + llvm_points_to x_ptr (llvm_term x'); +}; + +llvm_verify m "increment_u128" + [] + true + increment_u128_spec + (do { + //print_goal; + w4_unint_z3 []; +}); + +///////////////////////////////////////////////////////////////////////////////// +// eq_u128 proofs +///////////////////////////////////////////////////////////////////////////////// + +// "The bcmp() function compares the two byte sequences s1 and s2 of length n each. If they are equal, and in particular if n is zero, bcmp() returns 0. Otherwise it returns a nonzero result." +let bcmp_spec size = do { + (s1, s1_ptr) <- ptr_to_fresh_readonly "s1" (llvm_array size (llvm_int 8)); + (s2, s2_ptr) <- ptr_to_fresh_readonly "s2" (llvm_array size (llvm_int 8)); + + llvm_execute_func [ s1_ptr, s2_ptr, llvm_term {{ `size : [64]}} ]; + + ret <- llvm_fresh_var "ret" (llvm_int 32); + llvm_return (llvm_term ret); +}; + +bcmp_16_ov <- llvm_unsafe_assume_spec m "bcmp" (bcmp_spec 16); + +let eq_u128_spec = do { + (x, x_ptr) <- ptr_to_fresh_readonly "x" (llvm_int 128); + (y, y_ptr) <- ptr_to_fresh_readonly "y" (llvm_int 128); + + llvm_execute_func [x_ptr, y_ptr]; + + ret <- llvm_fresh_var "ret" (llvm_int 1); + llvm_return (llvm_term ret); +}; + +llvm_verify m "eq_u128" + [bcmp_16_ov] + true + eq_u128_spec + (do { + //print_goal; + w4_unint_z3 []; +}); diff --git a/exercises/memory-safety/u128/u128.c b/exercises/memory-safety/u128/u128.c new file mode 100644 index 0000000000..8938699483 --- /dev/null +++ b/exercises/memory-safety/u128/u128.c @@ -0,0 +1,20 @@ +#include +#include +#include +#include + +// Increment a 128-bit uint (represented as an array of 2 64-bit uints) +void increment_u128(uint64_t x[2]) { + if (++x[0] == 0) { + ++x[1]; + } +} + +bool eq_u128(const uint64_t x[2], const uint64_t y[2]) { + // "The bcmp() function compares the two byte sequences s1 and s2 of length + // n each. If they are equal, and in particular if n is zero, bcmp() returns + // 0. Otherwise it returns a nonzero result." --bcmp man page + // The type signature for bcmp is: + // int bcmp(const void *b1, const void *b2, size_t len); + return !bcmp(x, y, 16); +} \ No newline at end of file diff --git a/exercises/sha512/SHA.cry b/exercises/sha512/SHA.cry new file mode 100644 index 0000000000..eb27cb7ae7 --- /dev/null +++ b/exercises/sha512/SHA.cry @@ -0,0 +1,224 @@ +/* + Copyright (c) 2018, Galois Inc. + www.cryptol.net + You can freely use this source code for educational purposes. +*/ + +module SHA where + +sha : {L} (2 * w >= width L) => [L] -> [digest_size] +sha M = take (join (SHA_2_Common' [ split x | x <- parse`{num_blocks L} (pad`{L} M) ])) + +parameter + + /** Word size + Specifications are based on word size w, rather than digest size (8 * w) + or block size (m == 16 * w), in order to avoid confusing Cryptol's type + constraint verifier with integer division. + */ + + type w : # + type constraint (fin w, w >= 2, 32 >= width w) + + type digest_size : # + type constraint (fin digest_size, 8*w >= digest_size) + + /** The number of iterations in the hash computation + (i.e. the number of words in K) */ + + type j : # + type constraint (fin j, j >= 17) + + H0 : [8][w] + K : [j][w] + + /* FIPS 180-4 defines lowercase and uppercase + (respective to the Greek alphabet) sigma functions for SHA-256 and SHA-512. + (4.4)-(4.7) SHA-224, SHA-256 (w==32) + (4.10)-(4.13) SHA-384, SHA-512, SHA-512/224, SHA-512/256 (w==64) */ + + SIGMA_0 : [w] -> [w] + SIGMA_1 : [w] -> [w] + sigma_0 : [w] -> [w] + sigma_1 : [w] -> [w] + +// Export some of the parameters +SHAH0 = H0 +S0 = SIGMA_0 +S1 = SIGMA_1 +s0 = sigma_0 +s1 = sigma_1 + +// Export Ch, Maj and the block function to be used in SAW proofs +/** (4.1) (w==32), (4.2) (w==32), (4.8) (w==64) */ +Ch : [w] -> [w] -> [w] -> [w] +Ch x y z = (x && y) ^ (~x && z) + + +/** (4.1) (w==32), (4.3) (w==32), (4.9) (w==64) */ +Maj : [w] -> [w] -> [w] -> [w] +Maj x y z = (x && y) ^ (x && z) ^ (y && z) + +processBlock_Common : [8][w] -> [16][w] -> [8][w] +processBlock_Common H Mi = compress_Common H (messageSchedule_Common Mi) + + +private + + /** block size corresponding to word size for all SHA algorithms in + FIPS 180-4 */ + type block_size = 16 * w + + type num_blocks L = (L+1+2*w) /^ block_size + type padded_size L = num_blocks L * block_size + + + /** + 5.1 Padding the Message + 5.1.1 SHA-1, SHA-224 and SHA-256 (w==32) + 5.1.2 SHA-384, SHA-512, SHA-512/224 and SHA-512/256 (w==64) + + The constraint ensure that the message size, `L`, fits within a + (2 * w)-bit word (consistent w/ Figure 1) + */ + pad : {L} (2 * w >= width L) => [L] -> [padded_size L] + pad M = M # 0b1 # zero # (`L : [2*w]) + + /** + 5.2 Parsing the Message + 5.2.1 SHA-1, SHA-224 and SHA-256 (w==32) + 5.2.2 SHA-384, SHA-512, SHA-512/224 and SHA-512/256 (w==64) + */ + parse : {m} [m * block_size] -> [m][block_size] + parse = split + + /** + SHA-256 and SHA-512 (and their respective derivatives) use a similar + message schedule that can be expressed in the same way relative to their + respective sigma functions. + + 6.2.2 SHA-256 Hash Computation (w==32, j=64) + 6.4.2 SHA-512 Hash Computation (w==64, j=80) + */ + messageSchedule_Common : [16][w] -> [j][w] + messageSchedule_Common Mi = take W + where + W : [inf][_] + W = Mi # [ w1 + s0 w2 + w3 + s1 w4 + | w1 <- W + | w2 <- drop`{1} W + | w3 <- drop`{9} W + | w4 <- drop`{14} W + ] + + + /** + Amazon S2N's SHA-256 specification includes a compression routine intended + to reflect typical implementations. This same compression routine applies + to SHA-512, modulo respective constants, sigma functions, + and message schedules. + */ + + compress_Common : [8][w] -> [j][w] -> [8][w] + compress_Common H W = + // XXX: This whole definitions looks like it might be simplifiable. + [ (as ! 0) + (H @ 0), + (bs ! 0) + (H @ 1), + (cs ! 0) + (H @ 2), + (ds ! 0) + (H @ 3), + (es ! 0) + (H @ 4), + (fs ! 0) + (H @ 5), + (gs ! 0) + (H @ 6), + (hs ! 0) + (H @ 7) + ] + where + T1 = [h + S1 e + Ch e f g + k_t + w_t + | h <- hs | e <- es | f <- fs | g <- gs | k_t <- K | w_t <- W] + T2 = [ S0 a + Maj a b c | a <- as | b <- bs | c <- cs] + hs = take`{j + 1}([H @ 7] # gs) + gs = take`{j + 1}([H @ 6] # fs) + fs = take`{j + 1}([H @ 5] # es) + es = take`{j + 1}([H @ 4] # [d + t1 | d <- ds | t1 <- T1]) + ds = take`{j + 1}([H @ 3] # cs) + cs = take`{j + 1}([H @ 2] # bs) + bs = take`{j + 1}([H @ 1] # as) + as = take`{j + 1}([H @ 0] # [t1 + t2 | t1 <- T1 | t2 <- T2]) + + + SHA_2_Common' : {L} (fin L) => [L][16][w] -> [8][w] + SHA_2_Common' blocks = hash ! 0 + where + hash = [H0] # [ processBlock_Common h b | h <- hash | b <- blocks] + + +/////////////////////////////////////////////////////////////////////////////// +// SHA imperative specification +/////////////////////////////////////////////////////////////////////////////// + +/* + * This section contains an SHA specification that more closely matches the + * BoringSSL C implementation to simplify SAW correctness proofs of the + * implementation. + */ + +//////// Imperative top level //////// + +type SHAState = { h : [8][w] + , block : [w * 2][8] + , n : [32] + , sz : [w * 2] + } + +// Initial state for SHA +SHAInit : SHAState +SHAInit = { h = H0 + , block = zero + , n = 0 + , sz = 0 + } + +// Process message being hashed, iteratively updating the SHA state with the +// input message. +SHAUpdate : {n} (fin n) => SHAState -> [n][8] -> SHAState +SHAUpdate sinit bs = ss!0 + where ss = [sinit] # [ SHAUpdate1 s b | s <- ss | b <- bs ] + +// Add padding and size and process the final block. +SHAFinal : SHAState -> [digest_size] +SHAFinal s = take (join (processBlock_Common h b')) + // Because the message is always made up of bytes, and the size is a + // fixed number of bytes, the 1 pad will always be at least a byte. + where s' = SHAUpdate1 s 0x80 + // Don't need to add zeros. They're already there. Just update + // the count of bytes in this block. After adding the 1 pad, there + // are two possible cases: the size will fit in the current block, + // or it won't. + (h, b) = if s'.n <= (`w*2 - (`w/4)) then (s'.h, s'.block) + else (processBlock_Common s'.h (split (join s'.block)), zero) + b' = split (join b || (zero # s.sz)) + +// Imperative SHA implementation +SHAImp : {n} (fin n) => [n][8] -> [digest_size] +SHAImp msg = SHAFinal (SHAUpdate SHAInit msg) + + +private + + // SHAUpdate1 updates a single byte at position s.n in s.block and return a + // new state to pass to subsequent updates. If s.n is 128, updates position 0 + // to b and zeros the remainder of the block, setting s.n to 1 for the next + // update. + SHAUpdate1 : SHAState -> [8] -> SHAState + SHAUpdate1 s b = + if s.n == (2 * `w - 1) + then { h = processBlock_Common s.h (split (join (update s.block s.n b))) + , block = zero + , n = 0 + , sz = s.sz + 8 + } + else { h = s.h + , block = update s.block s.n b + , n = s.n + 1 + , sz = s.sz + 8 + } + diff --git a/exercises/sha512/SHA512.cry b/exercises/sha512/SHA512.cry new file mode 100644 index 0000000000..428df588a4 --- /dev/null +++ b/exercises/sha512/SHA512.cry @@ -0,0 +1,46 @@ +/* + Copyright (c) 2018, Galois Inc. + www.cryptol.net + You can freely use this source code for educational purposes. +*/ + +module SHA512 = SHA where + +type w = 64 + +type digest_size = 512 + +type j = 80 + +H0 = [ 0x6a09e667f3bcc908, 0xbb67ae8584caa73b, 0x3c6ef372fe94f82b, 0xa54ff53a5f1d36f1, + 0x510e527fade682d1, 0x9b05688c2b3e6c1f, 0x1f83d9abfb41bd6b, 0x5be0cd19137e2179] + +K = [ 0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc, + 0x3956c25bf348b538, 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118, + 0xd807aa98a3030242, 0x12835b0145706fbe, 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2, + 0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235, 0xc19bf174cf692694, + 0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65, + 0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5, + 0x983e5152ee66dfab, 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4, + 0xc6e00bf33da88fc2, 0xd5a79147930aa725, 0x06ca6351e003826f, 0x142929670a0e6e70, + 0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed, 0x53380d139d95b3df, + 0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b, + 0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30, + 0xd192e819d6ef5218, 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8, + 0x19a4c116b8d2d0c8, 0x1e376c085141ab53, 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8, + 0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373, 0x682e6ff3d6b2b8a3, + 0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec, + 0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b, + 0xca273eceea26619c, 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178, + 0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b, + 0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c, + 0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817] + +SIGMA_0 x = (x >>> 28) ^ (x >>> 34) ^ (x >>> 39) + +SIGMA_1 x = (x >>> 14) ^ (x >>> 18) ^ (x >>> 41) + +sigma_0 x = (x >>> 1) ^ (x >>> 8) ^ (x >> 7) + +sigma_1 x = (x >>> 19) ^ (x >>> 61) ^ (x >> 6) + diff --git a/exercises/sha512/exercise.saw b/exercises/sha512/exercise.saw new file mode 100644 index 0000000000..7f91a4eecc --- /dev/null +++ b/exercises/sha512/exercise.saw @@ -0,0 +1,120 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + + +import "SHA512.cry"; + +include "../common/helpers.saw"; + + +// Load LLVM bytecode +m <- llvm_load_module "sha512.bc"; + +//////////////////////////////////////////////////////////////////////////////// +// SHA-512 +//////////////////////////////////////////////////////////////////////////////// + +// To help you get to the interesting bits sooner, you're given all of the +// constants below + +/* + * SHA512 defines + */ +// Size of a block in bytes +let SHA512_CBLOCK = 128; + +// Length of message digest in bytes +let SHA512_DIGEST_LENGTH = 64; + +// Size of the SHA512 context struct +let SHA512_CTX_SIZE = llvm_sizeof m (llvm_struct "struct.sha512_state_st"); + +//////////////////////////////////////////////////////////////////////////////// +// BEGIN Part 1 +//////////////////////////////////////////////////////////////////////////////// + +// Prove the C function `sha512_block_data_order` satisfies the Cryptol +// specification `processBlock_Common`. + +// NOTE: The proof may take a few seconds to go through. The sample solution +// takes about 5 seconds on a reasonably modern laptop. If your proof has been +// running for over 30 seconds you can assume it is wrong. + +//////////////////////////////////////////////////////////////////////////////// +// END Part 1 +//////////////////////////////////////////////////////////////////////////////// + +// Helper functions to help you get to the interesting bit of part 2 + +/* + * Helpers for specifying the SHA512 structs + */ +/* + * The next functions all specify structs used in the C SHA implementation. + * Most of the statements in these are of the form: + * llvm_points_to (llvm_field ptr "name") (llvm_term {{ term }}) + * which indicates that the field `name` of the struct pointed to by `ptr` + * contains the value `term`. + * All statements that do not match these two forms are documented inline + */ + +// Specify the sha512_state_st struct from a SHAState +let points_to_sha512_state_st_common ptr (h, sz, block, n) num = do { + llvm_points_to (llvm_field ptr "h") (llvm_term h); + + // Specify `sha512_state_st.Nl` and `sha512_state_st.Nh` contain `sz` + llvm_points_to_at_type (llvm_field ptr "Nl") i128 (llvm_term sz); + + if eval_bool {{ `num == 0 }} then do { + // Do not specify anything about `sha512_state_st.p` + return (); + } else do { + // Specify that the first `num` bytes of `sha512_state_st.p` match the + // first `num` bits of `state.block`. + // Untyped check because the size of `sha512_state_st.p` does not match + // the size of (take`{num} state.block) unless `num` == `SHA512_CBLOCK` + llvm_points_to_untyped (llvm_field ptr "p") (llvm_term block); + }; + + llvm_points_to (llvm_field ptr "num") (llvm_term n); + llvm_points_to (llvm_field ptr "md_len") (llvm_term {{ `SHA512_DIGEST_LENGTH : [32] }}); +}; + +let pointer_to_fresh_sha512_state_st name n = do { + // Hash value + h <- llvm_fresh_var (str_concat name ".h") (llvm_array 8 i64); + // Message block + block <- if eval_bool {{ `n == 0 }} then do { + // Do not specify anything about `sha512_state_st.p` + return {{ [] : [0][8] }}; + } else do { + llvm_fresh_var (str_concat name ".block") (llvm_array n i8); + }; + // Size + sz <- llvm_fresh_var (str_concat name ".sz") i128; + // Build SHAState, padding `block` with zeros to fit + let state = {{ { h = h, block = (block # zero) : [SHA512_CBLOCK][8], n = `n : [32], sz = sz } }}; + + // `ptr` is a pointer to a `sha512_state_st` struct + ptr <- llvm_alloc (llvm_struct "struct.sha512_state_st"); + points_to_sha512_state_st_common ptr (h, sz, block, {{ `n : [32]}}) n; + + return (state, ptr); +}; + +// Specify the sha512_state_st struct from a SHAState +let points_to_sha512_state_st ptr state num = do { + points_to_sha512_state_st_common + ptr + ({{ state.h }}, {{ state.sz }}, {{ take`{num} state.block }}, {{ state.n }}) num; +}; + +//////////////////////////////////////////////////////////////////////////////// +// Part 2 +//////////////////////////////////////////////////////////////////////////////// + +// Prove the C function SHA512 equal to the Cryptol specification SHAImp. +// Ensure your proofs provide good code coverage by running multiple proofs with +// different sizes/lengths that cover distinct paths through the program. diff --git a/exercises/sha512/sha512.c b/exercises/sha512/sha512.c new file mode 100644 index 0000000000..6d2952071b --- /dev/null +++ b/exercises/sha512/sha512.c @@ -0,0 +1,374 @@ +/* Copyright (C) 1995-1998 Eric Young (eay@cryptsoft.com) + * All rights reserved. + * + * This package is an SSL implementation written + * by Eric Young (eay@cryptsoft.com). + * The implementation was written so as to conform with Netscapes SSL. + * + * This library is free for commercial and non-commercial use as long as + * the following conditions are aheared to. The following conditions + * apply to all code found in this distribution, be it the RC4, RSA, + * lhash, DES, etc., code; not just the SSL code. The SSL documentation + * included with this distribution is covered by the same copyright terms + * except that the holder is Tim Hudson (tjh@cryptsoft.com). + * + * Copyright remains Eric Young's, and as such any Copyright notices in + * the code are not to be removed. + * If this package is used in a product, Eric Young should be given attribution + * as the author of the parts of the library used. + * This can be in the form of a textual message at program startup or + * in documentation (online or textual) provided with the package. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * 3. All advertising materials mentioning features or use of this software + * must display the following acknowledgement: + * "This product includes cryptographic software written by + * Eric Young (eay@cryptsoft.com)" + * The word 'cryptographic' can be left out if the rouines from the library + * being used are not cryptographic related :-). + * 4. If you include any Windows specific code (or a derivative thereof) from + * the apps directory (application code) you must include an acknowledgement: + * "This product includes software written by Tim Hudson (tjh@cryptsoft.com)" + * + * THIS SOFTWARE IS PROVIDED BY ERIC YOUNG ``AS IS'' AND + * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS + * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) + * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF + * SUCH DAMAGE. + * + * The licence and distribution terms for any publically available version or + * derivative of this code cannot be changed. i.e. this code cannot simply be + * copied and put under another distribution licence + * [including the GNU Public Licence.] */ + +#include +#include +#include + +#include "sha512.h" + + +static inline uint16_t CRYPTO_bswap2(uint16_t x) { + return (x >> 8) | (x << 8); +} + +static inline uint32_t CRYPTO_bswap4(uint32_t x) { + x = (x >> 16) | (x << 16); + x = ((x & 0xff00ff00) >> 8) | ((x & 0x00ff00ff) << 8); + return x; +} + +static inline uint64_t CRYPTO_bswap8(uint64_t x) { + return CRYPTO_bswap4(x >> 32) | (((uint64_t)CRYPTO_bswap4(x)) << 32); +} + +static inline uint64_t CRYPTO_load_u64_be(const void *ptr) { + uint64_t ret; + memcpy(&ret, ptr, sizeof(ret)); + return CRYPTO_bswap8(ret); +} + +static inline void CRYPTO_store_u64_be(void *out, uint64_t v) { + v = CRYPTO_bswap8(v); + memcpy(out, &v, sizeof(v)); +} + +static inline uint64_t CRYPTO_rotr_u64(uint64_t value, int shift) { + return (value >> shift) | (value << ((-shift) & 63)); +} + + +int SHA512_Init(SHA512_CTX *sha) { + sha->h[0] = UINT64_C(0x6a09e667f3bcc908); + sha->h[1] = UINT64_C(0xbb67ae8584caa73b); + sha->h[2] = UINT64_C(0x3c6ef372fe94f82b); + sha->h[3] = UINT64_C(0xa54ff53a5f1d36f1); + sha->h[4] = UINT64_C(0x510e527fade682d1); + sha->h[5] = UINT64_C(0x9b05688c2b3e6c1f); + sha->h[6] = UINT64_C(0x1f83d9abfb41bd6b); + sha->h[7] = UINT64_C(0x5be0cd19137e2179); + + sha->Nl = 0; + sha->Nh = 0; + sha->num = 0; + sha->md_len = SHA512_DIGEST_LENGTH; + return 1; +} + +static void sha512_block_data_order(uint64_t *state, const uint8_t *in, + size_t num_blocks); + +int SHA512_Update(SHA512_CTX *c, const void *in_data, size_t len) { + uint64_t l; + uint8_t *p = c->p; + const uint8_t *data = in_data; + + if (len == 0) { + return 1; + } + + l = (c->Nl + (((uint64_t)len) << 3)) & UINT64_C(0xffffffffffffffff); + if (l < c->Nl) { + c->Nh++; + } + if (sizeof(len) >= 8) { + c->Nh += (((uint64_t)len) >> 61); + } + c->Nl = l; + + if (c->num != 0) { + size_t n = sizeof(c->p) - c->num; + + if (len < n) { + memcpy(p + c->num, data, len); + c->num += (unsigned int)len; + return 1; + } else { + memcpy(p + c->num, data, n), c->num = 0; + len -= n; + data += n; + sha512_block_data_order(c->h, p, 1); + } + } + + if (len >= sizeof(c->p)) { + sha512_block_data_order(c->h, data, len / sizeof(c->p)); + data += len; + len %= sizeof(c->p); + data -= len; + } + + if (len != 0) { + memcpy(p, data, len); + c->num = (int)len; + } + + return 1; +} + +int SHA512_Final(uint8_t out[SHA512_DIGEST_LENGTH], SHA512_CTX *sha) { + assert(sha->md_len == SHA512_DIGEST_LENGTH); + uint8_t *p = sha->p; + size_t n = sha->num; + + p[n] = 0x80; // There always is a room for one + n++; + if (n > (sizeof(sha->p) - 16)) { + memset(p + n, 0, sizeof(sha->p) - n); + n = 0; + sha512_block_data_order(sha->h, p, 1); + } + + memset(p + n, 0, sizeof(sha->p) - 16 - n); + CRYPTO_store_u64_be(p + sizeof(sha->p) - 16, sha->Nh); + CRYPTO_store_u64_be(p + sizeof(sha->p) - 8, sha->Nl); + + sha512_block_data_order(sha->h, p, 1); + + if (out == NULL) { + // TODO(davidben): This NULL check is absent in other low-level hash 'final' + // functions and is one of the few places one can fail. + return 0; + } + + assert(sha->md_len % 8 == 0); + const size_t out_words = sha->md_len / 8; + for (size_t i = 0; i < out_words; i++) { + CRYPTO_store_u64_be(out, sha->h[i]); + out += 8; + } + + return 1; +} + +uint8_t *SHA512(const uint8_t *data, size_t len, + uint8_t out[SHA512_DIGEST_LENGTH]) { + SHA512_CTX ctx; + const int ok = SHA512_Init(&ctx) && + SHA512_Update(&ctx, data, len) && + SHA512_Final(out, &ctx); + memset(&ctx, 0, sizeof(ctx)); + return out; +} + + +static const uint64_t K512[80] = { + UINT64_C(0x428a2f98d728ae22), UINT64_C(0x7137449123ef65cd), + UINT64_C(0xb5c0fbcfec4d3b2f), UINT64_C(0xe9b5dba58189dbbc), + UINT64_C(0x3956c25bf348b538), UINT64_C(0x59f111f1b605d019), + UINT64_C(0x923f82a4af194f9b), UINT64_C(0xab1c5ed5da6d8118), + UINT64_C(0xd807aa98a3030242), UINT64_C(0x12835b0145706fbe), + UINT64_C(0x243185be4ee4b28c), UINT64_C(0x550c7dc3d5ffb4e2), + UINT64_C(0x72be5d74f27b896f), UINT64_C(0x80deb1fe3b1696b1), + UINT64_C(0x9bdc06a725c71235), UINT64_C(0xc19bf174cf692694), + UINT64_C(0xe49b69c19ef14ad2), UINT64_C(0xefbe4786384f25e3), + UINT64_C(0x0fc19dc68b8cd5b5), UINT64_C(0x240ca1cc77ac9c65), + UINT64_C(0x2de92c6f592b0275), UINT64_C(0x4a7484aa6ea6e483), + UINT64_C(0x5cb0a9dcbd41fbd4), UINT64_C(0x76f988da831153b5), + UINT64_C(0x983e5152ee66dfab), UINT64_C(0xa831c66d2db43210), + UINT64_C(0xb00327c898fb213f), UINT64_C(0xbf597fc7beef0ee4), + UINT64_C(0xc6e00bf33da88fc2), UINT64_C(0xd5a79147930aa725), + UINT64_C(0x06ca6351e003826f), UINT64_C(0x142929670a0e6e70), + UINT64_C(0x27b70a8546d22ffc), UINT64_C(0x2e1b21385c26c926), + UINT64_C(0x4d2c6dfc5ac42aed), UINT64_C(0x53380d139d95b3df), + UINT64_C(0x650a73548baf63de), UINT64_C(0x766a0abb3c77b2a8), + UINT64_C(0x81c2c92e47edaee6), UINT64_C(0x92722c851482353b), + UINT64_C(0xa2bfe8a14cf10364), UINT64_C(0xa81a664bbc423001), + UINT64_C(0xc24b8b70d0f89791), UINT64_C(0xc76c51a30654be30), + UINT64_C(0xd192e819d6ef5218), UINT64_C(0xd69906245565a910), + UINT64_C(0xf40e35855771202a), UINT64_C(0x106aa07032bbd1b8), + UINT64_C(0x19a4c116b8d2d0c8), UINT64_C(0x1e376c085141ab53), + UINT64_C(0x2748774cdf8eeb99), UINT64_C(0x34b0bcb5e19b48a8), + UINT64_C(0x391c0cb3c5c95a63), UINT64_C(0x4ed8aa4ae3418acb), + UINT64_C(0x5b9cca4f7763e373), UINT64_C(0x682e6ff3d6b2b8a3), + UINT64_C(0x748f82ee5defb2fc), UINT64_C(0x78a5636f43172f60), + UINT64_C(0x84c87814a1f0ab72), UINT64_C(0x8cc702081a6439ec), + UINT64_C(0x90befffa23631e28), UINT64_C(0xa4506cebde82bde9), + UINT64_C(0xbef9a3f7b2c67915), UINT64_C(0xc67178f2e372532b), + UINT64_C(0xca273eceea26619c), UINT64_C(0xd186b8c721c0c207), + UINT64_C(0xeada7dd6cde0eb1e), UINT64_C(0xf57d4f7fee6ed178), + UINT64_C(0x06f067aa72176fba), UINT64_C(0x0a637dc5a2c898a6), + UINT64_C(0x113f9804bef90dae), UINT64_C(0x1b710b35131c471b), + UINT64_C(0x28db77f523047d84), UINT64_C(0x32caab7b40c72493), + UINT64_C(0x3c9ebe0a15c9bebc), UINT64_C(0x431d67c49c100d4c), + UINT64_C(0x4cc5d4becb3e42b6), UINT64_C(0x597f299cfc657e2a), + UINT64_C(0x5fcb6fab3ad6faec), UINT64_C(0x6c44198c4a475817), +}; + +static inline uint64_t Sigma0(uint64_t x) { + return CRYPTO_rotr_u64((x), 28) ^ CRYPTO_rotr_u64((x), 34) ^ + CRYPTO_rotr_u64((x), 39); +} + +static inline uint64_t Sigma1(uint64_t x) { + return CRYPTO_rotr_u64((x), 14) ^ CRYPTO_rotr_u64((x), 18) ^ + CRYPTO_rotr_u64((x), 41); +} + +static inline uint64_t sigma0(uint64_t x) { + return CRYPTO_rotr_u64((x), 1) ^ CRYPTO_rotr_u64((x), 8) ^ ((x) >> 7); +} + +static inline uint64_t sigma1(uint64_t x) { + return CRYPTO_rotr_u64((x), 19) ^ CRYPTO_rotr_u64((x), 61) ^ ((x) >> 6); +} + +static inline uint64_t Ch(uint64_t x, uint64_t y, uint64_t z) { + return ((x) & (y)) ^ ((~(x)) & (z)); +} + +#define Maj(x, y, z) (((x) & (y)) ^ ((x) & (z)) ^ ((y) & (z))) + +#define ROUND_00_15(i, a, b, c, d, e, f, g, h) \ + do { \ + T1 += h + Sigma1(e) + Ch(e, f, g) + K512[i]; \ + h = Sigma0(a) + Maj(a, b, c); \ + d += T1; \ + h += T1; \ + } while (0) + +#define ROUND_16_80(i, j, a, b, c, d, e, f, g, h, X) \ + do { \ + s0 = X[(j + 1) & 0x0f]; \ + s0 = sigma0(s0); \ + s1 = X[(j + 14) & 0x0f]; \ + s1 = sigma1(s1); \ + T1 = X[(j) & 0x0f] += s0 + s1 + X[(j + 9) & 0x0f]; \ + ROUND_00_15(i + j, a, b, c, d, e, f, g, h); \ + } while (0) + +static void sha512_block_data_order(uint64_t *state, const uint8_t *in, + size_t num) { + uint64_t a, b, c, d, e, f, g, h, s0, s1, T1; + uint64_t X[16]; + int i; + + while (num--) { + + a = state[0]; + b = state[1]; + c = state[2]; + d = state[3]; + e = state[4]; + f = state[5]; + g = state[6]; + h = state[7]; + + T1 = X[0] = CRYPTO_load_u64_be(in); + ROUND_00_15(0, a, b, c, d, e, f, g, h); + T1 = X[1] = CRYPTO_load_u64_be(in + 8); + ROUND_00_15(1, h, a, b, c, d, e, f, g); + T1 = X[2] = CRYPTO_load_u64_be(in + 2 * 8); + ROUND_00_15(2, g, h, a, b, c, d, e, f); + T1 = X[3] = CRYPTO_load_u64_be(in + 3 * 8); + ROUND_00_15(3, f, g, h, a, b, c, d, e); + T1 = X[4] = CRYPTO_load_u64_be(in + 4 * 8); + ROUND_00_15(4, e, f, g, h, a, b, c, d); + T1 = X[5] = CRYPTO_load_u64_be(in + 5 * 8); + ROUND_00_15(5, d, e, f, g, h, a, b, c); + T1 = X[6] = CRYPTO_load_u64_be(in + 6 * 8); + ROUND_00_15(6, c, d, e, f, g, h, a, b); + T1 = X[7] = CRYPTO_load_u64_be(in + 7 * 8); + ROUND_00_15(7, b, c, d, e, f, g, h, a); + T1 = X[8] = CRYPTO_load_u64_be(in + 8 * 8); + ROUND_00_15(8, a, b, c, d, e, f, g, h); + T1 = X[9] = CRYPTO_load_u64_be(in + 9 * 8); + ROUND_00_15(9, h, a, b, c, d, e, f, g); + T1 = X[10] = CRYPTO_load_u64_be(in + 10 * 8); + ROUND_00_15(10, g, h, a, b, c, d, e, f); + T1 = X[11] = CRYPTO_load_u64_be(in + 11 * 8); + ROUND_00_15(11, f, g, h, a, b, c, d, e); + T1 = X[12] = CRYPTO_load_u64_be(in + 12 * 8); + ROUND_00_15(12, e, f, g, h, a, b, c, d); + T1 = X[13] = CRYPTO_load_u64_be(in + 13 * 8); + ROUND_00_15(13, d, e, f, g, h, a, b, c); + T1 = X[14] = CRYPTO_load_u64_be(in + 14 * 8); + ROUND_00_15(14, c, d, e, f, g, h, a, b); + T1 = X[15] = CRYPTO_load_u64_be(in + 15 * 8); + ROUND_00_15(15, b, c, d, e, f, g, h, a); + + for (i = 16; i < 80; i += 16) { + ROUND_16_80(i, 0, a, b, c, d, e, f, g, h, X); + ROUND_16_80(i, 1, h, a, b, c, d, e, f, g, X); + ROUND_16_80(i, 2, g, h, a, b, c, d, e, f, X); + ROUND_16_80(i, 3, f, g, h, a, b, c, d, e, X); + ROUND_16_80(i, 4, e, f, g, h, a, b, c, d, X); + ROUND_16_80(i, 5, d, e, f, g, h, a, b, c, X); + ROUND_16_80(i, 6, c, d, e, f, g, h, a, b, X); + ROUND_16_80(i, 7, b, c, d, e, f, g, h, a, X); + ROUND_16_80(i, 8, a, b, c, d, e, f, g, h, X); + ROUND_16_80(i, 9, h, a, b, c, d, e, f, g, X); + ROUND_16_80(i, 10, g, h, a, b, c, d, e, f, X); + ROUND_16_80(i, 11, f, g, h, a, b, c, d, e, X); + ROUND_16_80(i, 12, e, f, g, h, a, b, c, d, X); + ROUND_16_80(i, 13, d, e, f, g, h, a, b, c, X); + ROUND_16_80(i, 14, c, d, e, f, g, h, a, b, X); + ROUND_16_80(i, 15, b, c, d, e, f, g, h, a, X); + } + + state[0] += a; + state[1] += b; + state[2] += c; + state[3] += d; + state[4] += e; + state[5] += f; + state[6] += g; + state[7] += h; + + in += 16 * 8; + } +} + diff --git a/exercises/sha512/sha512.h b/exercises/sha512/sha512.h new file mode 100644 index 0000000000..628600b9f1 --- /dev/null +++ b/exercises/sha512/sha512.h @@ -0,0 +1,95 @@ +/* Copyright (C) 1995-1998 Eric Young (eay@cryptsoft.com) + * All rights reserved. + * + * This package is an SSL implementation written + * by Eric Young (eay@cryptsoft.com). + * The implementation was written so as to conform with Netscapes SSL. + * + * This library is free for commercial and non-commercial use as long as + * the following conditions are aheared to. The following conditions + * apply to all code found in this distribution, be it the RC4, RSA, + * lhash, DES, etc., code; not just the SSL code. The SSL documentation + * included with this distribution is covered by the same copyright terms + * except that the holder is Tim Hudson (tjh@cryptsoft.com). + * + * Copyright remains Eric Young's, and as such any Copyright notices in + * the code are not to be removed. + * If this package is used in a product, Eric Young should be given attribution + * as the author of the parts of the library used. + * This can be in the form of a textual message at program startup or + * in documentation (online or textual) provided with the package. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * 1. Redistributions of source code must retain the copyright + * notice, this list of conditions and the following disclaimer. + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * 3. All advertising materials mentioning features or use of this software + * must display the following acknowledgement: + * "This product includes cryptographic software written by + * Eric Young (eay@cryptsoft.com)" + * The word 'cryptographic' can be left out if the rouines from the library + * being used are not cryptographic related :-). + * 4. If you include any Windows specific code (or a derivative thereof) from + * the apps directory (application code) you must include an acknowledgement: + * "This product includes software written by Tim Hudson (tjh@cryptsoft.com)" + * + * THIS SOFTWARE IS PROVIDED BY ERIC YOUNG ``AS IS'' AND + * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS + * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) + * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF + * SUCH DAMAGE. + * + * The licence and distribution terms for any publically available version or + * derivative of this code cannot be changed. i.e. this code cannot simply be + * copied and put under another distribution licence + * [including the GNU Public Licence.] */ + +#ifndef HEADER_SHA512_H +#define HEADER_SHA512_H + +// SHA-512. + +// SHA512_CBLOCK is the block size of SHA-512. +#define SHA512_CBLOCK 128 + +// SHA512_DIGEST_LENGTH is the length of a SHA-512 digest. +#define SHA512_DIGEST_LENGTH 64 + +struct sha512_state_st { + uint64_t h[8]; + uint64_t Nl, Nh; + uint8_t p[128]; + unsigned num, md_len; +}; + +typedef struct sha512_state_st SHA512_CTX; + +// SHA512_Init initialises |sha| and returns 1. +int SHA512_Init(SHA512_CTX *sha); + +// SHA512_Update adds |len| bytes from |data| to |sha| and returns 1. +int SHA512_Update(SHA512_CTX *sha, const void *data, size_t len); + +// SHA512_Final adds the final padding to |sha| and writes the resulting digest +// to |out|, which must have at least |SHA512_DIGEST_LENGTH| bytes of space. It +// returns one on success and zero on programmer error. +int SHA512_Final(uint8_t out[SHA512_DIGEST_LENGTH], SHA512_CTX *sha); + +// SHA512 writes the digest of |len| bytes from |data| to |out| and returns +// |out|. There must be at least |SHA512_DIGEST_LENGTH| bytes of space in +// |out|. +uint8_t *SHA512(const uint8_t *data, size_t len, + uint8_t out[SHA512_DIGEST_LENGTH]); + +#endif // HEADER_SHA512_H + diff --git a/exercises/sha512/solution.saw b/exercises/sha512/solution.saw new file mode 100644 index 0000000000..b6ea572826 --- /dev/null +++ b/exercises/sha512/solution.saw @@ -0,0 +1,463 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 +*/ + + +import "SHA512.cry"; + +include "../common/helpers.saw"; + + +// Load LLVM bytecode +m <- llvm_load_module "sha512.bc"; + + +/* + * SHA512 defines + */ +// Size of a block in bytes +let SHA512_CBLOCK = 128; + +// Length of message digest in bytes +let SHA512_DIGEST_LENGTH = 64; + +// Size of the SHA512 context struct +let SHA512_CTX_SIZE = llvm_sizeof m (llvm_struct "struct.sha512_state_st"); + + +//////////////////////////////////////////////////////////////////////////////// +// Specifications + +/* + * This section of the SAW script contains specifications of the functions that + * SAW will verify. Each specification can be broken down into 3 components: + * preconditions, a function call description, and postconditions. + * + * A precondition is a predicate that must be true prior to the application of + * a function for the specification's postcondition to hold. Preconditions are + * typically restrictions on function inputs or global state. For example, a + * function that returns the first element of an array might have a + * precondition that the array is not empty. A specification makes no + * guarantees about how the function acts when the precondition is violated. + * In a SAW specification, preconditions are the statements that come before a + * function call description. If a function has no preconditions we say that + * the precondition is "true", meaning that the postcondition holds for all + * possible inputs and program states. + * + * A function call description tells SAW how to call the function being + * specified. It has the form: + * llvm_execute_func [] + * These arguments are typically from the preconditions, specification inputs, + * global variables, and literals. SAW does not actually execute the function, + * but rather uses symbolic execution to examine all possible executions + * through the function, subject to precondition constraints. For example, + * if a precondition states that a variable `sha_ptr` is a pointer to an + * `sha512_state_st` struct: + * ctx_ptr <- llvm_alloc (llvm_struct "struct.sha512_state_st"); + * And the function call description takes `sha_ptr` as an input: + * llvm_execute_func [sha_ptr]; + * Then SAW will reason about the function over all possible `sha512_state_st` + * structs. We call `sha_ptr` a symbol because SAW does not evaluate it, but + * rather treats it as the set of all possible `sha512_state_st` structs. + * + * A postcondition is a predicate that must be true following the application + * of a function, assuming the function's precondition held. From a logic + * perspective, you can think of this as: + * ( /\ ) -> + * + * where "/\" is logical AND and "->" is logical implication. If a SAW proof + * succeeds, then SAW guarantees that the postconditions hold following function + * application, so long as the function's preconditions held just prior to the + * function's application. In a SAW specification, postconditions are the + * statements that come after a function call description. If a function has + * no postconditions, then we say that the postcondition is "true", meaning + * that the specification makes no guarantees about the function's behavior. + */ + +/* + * Specifications of functions Sigma0, Sigma1, sigma0, sigma1, and Ch + */ +let Sigma0_spec = do { + x <- llvm_fresh_var "x" i64; + llvm_execute_func [llvm_term x]; + llvm_return (llvm_term {{ S0 x }}); +}; + +let Sigma1_spec = do { + x <- llvm_fresh_var "x" i64; + llvm_execute_func [llvm_term x]; + llvm_return (llvm_term {{ S1 x }}); +}; + +let sigma0_spec = do { + x <- llvm_fresh_var "x" i64; + llvm_execute_func [llvm_term x]; + llvm_return (llvm_term {{ s0 x }}); +}; + +let sigma1_spec = do { + x <- llvm_fresh_var "x" i64; + llvm_execute_func [llvm_term x]; + llvm_return (llvm_term {{ s1 x }}); +}; + +let Ch_spec = do { + x <- llvm_fresh_var "x" i64; + y <- llvm_fresh_var "y" i64; + z <- llvm_fresh_var "z" i64; + llvm_execute_func [llvm_term x, llvm_term y, llvm_term z]; + llvm_return (llvm_term {{ Ch x y z }}); +}; + +/* + * Specification of block function for SHA512 + */ +let sha512_block_data_order_spec = do { + // Precondition: `state_ptr` points to an array of 8 64 bit integers + (state, state_ptr) <- ptr_to_fresh "state" (llvm_array 8 i64); + + // Precondition: `data_ptr` points to a const message block + (data, data_ptr) <- ptr_to_fresh_readonly "data" (llvm_array SHA512_CBLOCK i8); + + // Call function with `state_ptr`, `data_ptr`, and the value `1` + llvm_execute_func [state_ptr, data_ptr, llvm_term {{ 1 : [64] }}]; + + // Postcondition: The data pointed to by `state_ptr` is equivalent to the + // return value of the processBlock_Common Cryptol spec function applied to `state` + // and `data`. + llvm_points_to state_ptr (llvm_term {{ processBlock_Common state (split (join data)) }}); +}; + + +/* + * Helpers for specifying the SHA512 structs + */ +/* + * The next functions all specify structs used in the C SHA implementation. + * Most of the statements in these are of the form: + * llvm_points_to (llvm_field ptr "name") (llvm_term {{ term }}) + * which indicates that the field `name` of the struct pointed to by `ptr` + * contains the value `term`. + * All statements that do not match these two forms are documented inline + */ + +// Specify the sha512_state_st struct from a SHAState +let points_to_sha512_state_st_common ptr (h, sz, block, n) num = do { + llvm_points_to (llvm_field ptr "h") (llvm_term h); + + // Specify `sha512_state_st.Nl` and `sha512_state_st.Nh` contain `sz` + llvm_points_to_at_type (llvm_field ptr "Nl") i128 (llvm_term sz); + + if eval_bool {{ `num == 0 }} then do { + // Do not specify anything about `sha512_state_st.p` + return (); + } else do { + // Specify that the first `num` bytes of `sha512_state_st.p` match the + // first `num` bits of `state.block`. + // Untyped check because the size of `sha512_state_st.p` does not match + // the size of (take`{num} state.block) unless `num` == `SHA512_CBLOCK` + llvm_points_to_untyped (llvm_field ptr "p") (llvm_term block); + }; + + llvm_points_to (llvm_field ptr "num") (llvm_term n); + llvm_points_to (llvm_field ptr "md_len") (llvm_term {{ `SHA512_DIGEST_LENGTH : [32] }}); +}; + +let pointer_to_fresh_sha512_state_st name n = do { + // Hash value + h <- llvm_fresh_var (str_concat name ".h") (llvm_array 8 i64); + // Message block + block <- if eval_bool {{ `n == 0 }} then do { + // Do not specify anything about `sha512_state_st.p` + return {{ [] : [0][8] }}; + } else do { + llvm_fresh_var (str_concat name ".block") (llvm_array n i8); + }; + // Size + sz <- llvm_fresh_var (str_concat name ".sz") i128; + // Build SHAState, padding `block` with zeros to fit + let state = {{ { h = h, block = (block # zero) : [SHA512_CBLOCK][8], n = `n : [32], sz = sz } }}; + + // `ptr` is a pointer to a `sha512_state_st` struct + ptr <- llvm_alloc (llvm_struct "struct.sha512_state_st"); + points_to_sha512_state_st_common ptr (h, sz, block, {{ `n : [32]}}) n; + + return (state, ptr); +}; + +// Specify the sha512_state_st struct from a SHAState +let points_to_sha512_state_st ptr state num = do { + points_to_sha512_state_st_common + ptr + ({{ state.h }}, {{ state.sz }}, {{ take`{num} state.block }}, {{ state.n }}) num; +}; + + +/* + * Specifications of SHA512_Init, SHA512_Update, SHA512_Final, + * and SHA512. + */ +let SHA512_Init_spec = do { + // Precondition: `sha_ptr` is a pointer to a `sha512_state_st` struct + sha_ptr <- llvm_alloc (llvm_struct "struct.sha512_state_st"); + + // Call function with `sha_ptr` + llvm_execute_func [sha_ptr]; + + // Postcondition: `sha_ptr` holds an initialized SHA512 context + points_to_sha512_state_st + sha_ptr + {{ { h = SHAH0, block = zero : [SHA512_CBLOCK][8], n = 0 : [32], sz = 0 : [128] } }} + 0; + + // Postcondition: The function returns 1 + llvm_return (llvm_term {{ 1 : [32] }}); +}; + +let SHA512_Update_spec num len = do { + // Precondition: `sha_ptr` is a pointer to a `sha512_state_st` struct + // Precondition: `sha512_ctx` is a fresh Cryptol SHAState + // Precondition: `sha_ptr` matches `sha512_ctx`. The message blocks + // of the two must only match up to the first `num` bits. + (sha512_ctx, sha_ptr) <- pointer_to_fresh_sha512_state_st "sha512_ctx" num; + + // Precondition: `data` is a fresh array of `len` bytes, and `data_ptr` + // points to `data`. + (data, data_ptr) <- ptr_to_fresh_readonly "data" (llvm_array len i8); + + // Call function with `sha_ptr`, `data_ptr`, and `len` as arguments. + llvm_execute_func [sha_ptr, data_ptr, llvm_term {{ `len : [64] }}]; + + // Postcondition: The context `sha_ptr` points to matches the result + // of executing the cryptol function `SHAUpdate` on `sha512_ctx` and + // `data`, with the exception of the message block, which must only match up + // to the first `(num + len) % SHA512_CBLOCK` bytes. This is because the + // C implementation does not clear the unused bytes of message block, and + // therefore the tail end of the block contains garbage. + points_to_sha512_state_st + sha_ptr + {{ SHAUpdate sha512_ctx data }} (eval_size {| (num + len) % SHA512_CBLOCK |}); + + // Postcondition: The function returns 1 + llvm_return (llvm_term {{ 1 : [32] }}); +}; + +let SHA512_Final_spec num = do { + // Precondition: `out_ptr` is allocated and points to an array + // of `SHA512_DIGEST_LENGTH` bytes. + out_ptr <- llvm_alloc (llvm_array SHA512_DIGEST_LENGTH i8); + + // Precondition: `sha_ptr` is a pointer to a `sha512_state_st` struct + // Precondition: `sha512_ctx` is a fresh Cryptol SHAState + // Precondition: `sha_ptr` matches `sha512_ctx`. The message blocks + // of the two must only match up to the first `num` bits. + (sha512_ctx, sha_ptr) <- pointer_to_fresh_sha512_state_st "sha512_ctx" num; + + // Call function with `out_ptr`, and `sha_ptr`. + llvm_execute_func [out_ptr, sha_ptr]; + + // Postcondition: The data pointed to by `out_ptr` matches the message + // digest returned by the Cryptol function `SHAFinal`. The reverses, + // splits, and joins transform the Cryptol function's big endian output to + // little endian. + llvm_points_to out_ptr (llvm_term {{ split`{SHA512_DIGEST_LENGTH} (SHAFinal sha512_ctx) }}); + + // Postcondition: The function returns 1 + llvm_return (llvm_term {{ 1 : [32] }}); +}; + +let SHA512_spec len = do { + // Precondition: `data` is a fresh const array of `len` bytes, and `data_ptr` + // points to `data`. + (data, data_ptr) <- ptr_to_fresh_readonly "data" (llvm_array len i8); + + // Precondition: `out_ptr` is allocated and points to an array + // of `SHA512_DIGEST_LENGTH` bytes. + out_ptr <- llvm_alloc (llvm_array SHA512_DIGEST_LENGTH i8); + + // Call function with arguments data_ptr, len, and out_ptr. + llvm_execute_func + [ data_ptr + , llvm_term {{ `len : [64] }} + , out_ptr + ]; + + // Postcondition: The data pointed to by `out_ptr` matches the message + // digest returned by the Cryptol function `SHAImp`. The reverses, + // splits, and joins transform the Cryptol function's big endian output to + // little endian. + llvm_points_to out_ptr (llvm_term {{ split`{SHA512_DIGEST_LENGTH} (SHAImp data) }}); + + // Postcondition: The function returns the pointer `out_ptr`. + llvm_return out_ptr; +}; + + +//////////////////////////////////////////////////////////////////////////////// +// Proof commands + +// Verify functions Sigma0, Sigma1, sigma0, sigma1, and Ch +// satisfy their specifications + +Sigma0_ov <- llvm_verify m "Sigma0" + [] + true + Sigma0_spec + (w4_unint_z3 []); + +Sigma1_ov <- llvm_verify m "Sigma1" + [] + true + Sigma1_spec + (w4_unint_z3 []); + +sigma0_ov <- llvm_verify m "sigma0" + [] + true + sigma0_spec + (w4_unint_z3 []); + +sigma1_ov <- llvm_verify m "sigma1" + [] + true + sigma1_spec + (w4_unint_z3 []); + +Ch_ov <- llvm_verify m "Ch" + [] + true + Ch_spec + (w4_unint_z3 []); + +// Verify the block data function satisfies the bounded +// `sha512_block_data_order_spec` specification + +sha512_block_data_order_ov <- llvm_verify m "sha512_block_data_order" + [Sigma0_ov, Sigma1_ov, sigma0_ov, sigma1_ov, Ch_ov] + true + sha512_block_data_order_spec + (w4_unint_z3 ["S0", "S1", "s0", "s1", "Ch"]); + + +// Verify the `SHA512_Init` C function satisfies the `SHA512_Init_spec` +// specification +SHA512_Init_ov <- llvm_verify m "SHA512_Init" + [] + true + SHA512_Init_spec + (w4_unint_z3 []); + + +// Verify the `SHA512_Update` C function satisfies the +// `SHA512_Update_spec` specification. +// There are 3 cases to consider to ensure the proof covers all possible code +// paths through the update function + +SHA512_Update_0_240_ov <- llvm_verify m "SHA512_Update" + [sha512_block_data_order_ov] + true + // num=0, len=240 covers the case with one call to the block function, + // on one block from data, and the rest of data copied in c->data + (SHA512_Update_spec 0 240) + (w4_unint_z3 ["processBlock_Common"]); +SHA512_Update_0_127_ov <- llvm_verify m "SHA512_Update" + [sha512_block_data_order_ov] + true + // num=0, len=127 covers the case without any calls to the block function, + // and data copied in c->data + (SHA512_Update_spec 0 127) + (w4_unint_z3 ["processBlock_Common"]); +SHA512_Update_127_241_ov <- llvm_verify m "SHA512_Update" + [sha512_block_data_order_ov] + true + // num=127, len=241 covers the case with two calls to the block function, + // the first one on c->data, the second one on one block from data, + // and the rest of data copied in c->data + (SHA512_Update_spec 127 241) + (w4_unint_z3 ["processBlock_Common"]); + + +// Verify the `SHA512_Final` C function satisfies the +// `SHA512_Final_spec` specification. +// There are 2 cases to consider to ensure the proof covers all possible code +// paths through the update function + +SHA512_Final_111_ov <- llvm_verify m "SHA512_Final" + [sha512_block_data_order_ov] + true + // num=111 covers the case with one call to the block function + (SHA512_Final_spec 111) + (w4_unint_z3 ["processBlock_Common"]); +SHA512_Final_112_ov <- llvm_verify m "SHA512_Final" + [sha512_block_data_order_ov] + true + // num=112 covers the case with two calls to the block function + (SHA512_Final_spec 112) + (w4_unint_z3 ["processBlock_Common"]); + + +// Verify the `SHA512` C function satisfies the `SHA512_spec` +// specification +llvm_verify m "SHA512" + [SHA512_Init_ov, SHA512_Update_0_240_ov, SHA512_Final_112_ov] + true + (SHA512_spec 240) + (w4_unint_z3 ["processBlock_Common"]); + + +let quick_check = true; +let target_num = 128; + +if quick_check then do { + return (); +} else do { + // this covers the case with all lengths given a target_num. + print (str_concat "Verifying SHA512_Update at target_num=" (show target_num)); + let verify_update_at_len len = do { + print (str_concat "Verifying SHA512_Update at len=" (show len)); + llvm_verify m "SHA512_Update" + [sha512_block_data_order_ov] + true + (SHA512_Update_spec target_num len) + (w4_unint_z3 ["processBlock_Common"]); + }; + // Given a fixed `num`, the `lens` cover all possible parameters especially below cases: + // When len = (SHA512_CBLOCK - 1), this covers the case without any calls to the block function, + // and data copied in c->data. + // When len = (SHA512_CBLOCK + 1), this covers the case with one call to the block function, + // on one block from data, and the rest of data copied in c->data. + // When len = (SHA512_CBLOCK + 1), this covers the case with two calls to the block function, + // the first one on c->data, the second one on one block from data, and the rest of data copied in c->data. + // Note: when num = 0, 'len = 256' check fails due to 'sha512_block_data_order' limit. + if eval_bool {{ `target_num == 0 }} then do { + lens <- for (eval_list {{ [0 .. (2 * SHA512_CBLOCK - 1)] : [2 * SHA512_CBLOCK][64] }}) + (\x -> (return (eval_int x)) : (TopLevel Int)); + for lens verify_update_at_len; + } else do { + lens <- for (eval_list {{ [0 .. (2 * SHA512_CBLOCK + 1 - target_num)] : [2 * SHA512_CBLOCK + 2 - target_num][64] }}) + (\x -> (return (eval_int x)) : (TopLevel Int)); + for lens verify_update_at_len; + }; + return (); +}; + +// range of valid indices in the internal block ([0 .. (SHA512_CBLOCK - 1)]) +nums <- for (eval_list {{ [0 .. (SHA512_CBLOCK - 1)] : [SHA512_CBLOCK][64] }}) + (\x -> (return (eval_int x)) : (TopLevel Int)); + +if quick_check then do { + return (); +} else do { + let verify_final_at_num num = do { + print (str_concat "Verifying SHA512_Final at num=" (show num)); + llvm_verify m "SHA512_Final" + [sha512_block_data_order_ov] + true + (SHA512_Final_spec num) + (w4_unint_z3 ["processBlock_Common"]); + }; + for nums verify_final_at_num; + return (); +}; +