Saw python api

.github/workflows/python-saw.yml

@@ -46,3 +46,22 @@ jobs:
           python3 labs/Demos/SAW/xxHash/xxhash32-ref.py
           python3 labs/Demos/SAW/xxHash/xxhash64-ref.py
           python3 labs/Demos/SAW/Salsa20/proof/salsa20.py
+
+  saw-tutorial:
+    runs-on: ubuntu-latest
+    container:
+      image: ghcr.io/weaversa/cryptol-course:2.12
+      options: --user root
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v2
+      # Start saw-remote-api server
+      - run: start-saw-remote-api-read-only
+      # Run final rotl SAW Script
+      - run: cd labs/SAW/proof && clang ../src/rotl3.c -o ../src/rotl.bc -c -emit-llvm && python3 rotl.py
+      # Run addRow SAW Script
+      - run: cd labs/SAW/proof && clang ../src/addRow.c -o ../src/addRow.bc -c -emit-llvm && python3 addRow.py
+      # Run null SAW Script
+      - run: cd labs/SAW/proof && clang ../src/null.c -o ../src/null.bc -c -emit-llvm && python3 null.py
+      # Run Game SAW Script
+      - run: cd labs/SAW/Game/DLC && mkdir artifacts && clang -c -g -emit-llvm -o artifacts/Game.bc src/Game.c && python3 proof/Game.py

.gitignore

@@ -1 +1,3 @@
 **/.DS_Store
+**/*.bc
+**/*~

README.md

@@ -123,6 +123,9 @@ first lab walks you through [installing and running Cryptol](INSTALL.md).
       enjoyed the last lab, go ahead and try your hand at using
       Cryptol's connection to automated provers (SMT solvers) to solve
       some classic computational puzzles.
+    * [Continuous Reasoning with SAW](./labs/SAW/SAW.md): Learn how to
+      use Python to drive SAW and enforce formal invariants on
+      cryptographic implementations at every check-in to a repository.
 8. [Methods for Key Wrapping](./labs/KeyWrapping/KeyWrapping.md):
    Create a Cryptol specification of NIST's [SP800-38F key wrap
    standard](https://csrc.nist.gov/publications/detail/sp/800-38f/final).

labs/CryptoProofs/CryptoProofs.md

@@ -339,7 +339,7 @@ plaintext inputs.
 
 **EXERCISE**: 2.5.2 DES Parity Bits
 
-Having equivalent keys is often considered a weakness in an a
+Having equivalent keys is often considered a weakness in a
 cipher. However, in the case of DES, it turns out that this is a
 result of a design choice. The lowest bit of each byte of a DES key is
 actually a [parity bit](https://en.wikipedia.org/wiki/Parity_bit) that
@@ -383,3 +383,4 @@ https://github.com/weaversa/cryptol-course/issues
 || [+ Salsa20 Properties](../Salsa20/Salsa20Props.md) ||
 || [+ Transposition Ciphers](../Transposition/Contents.md) ||
 || [+ Project Euler](../ProjectEuler/ProjectEuler.md) ||
+|| [+ Continuous Reasoning with SAW](../SAW/SAW.md) ||

labs/CryptoProofs/CryptoProofsAnswers.md

@@ -228,9 +228,6 @@ matched_pt = join "tootough"
 matched_ct = 0x95d07f8a72707733
 ```
 
-To make this solvable, try it again with the first six bytes of key
-provided: `0x1234567890ab`.
-
 ```Xcryptol-session-ci-none
 labs::CryptoProofs::CryptoProofsAnswers> :sat \key -> DES.encrypt key matched_pt == matched_ct
 ```
@@ -242,6 +239,9 @@ DES keys have been broken using specialized algorithms
 and large amounts of compute power, but not by a single computer
 running a SAT solver.
 
+To make this solvable, try it again with the first six bytes of key
+provided: `0x1234567890ab`.
+
 ```Xcryptol-session
 labs::CryptoProofs::CryptoProofsAnswers> :sat \key -> DES.encrypt key matched_pt == matched_ct /\ take key == 0x1234567890ab
 Satisfiable
@@ -419,7 +419,7 @@ Q.E.D.
 
 **EXERCISE**: 2.5.2 DES Parity Bits
 
-Having equivalent keys is often considered a weakness in an a
+Having equivalent keys is often considered a weakness in a
 cipher. However, in the case of DES, it turns out that this is a
 result of a design choice. The lowest bit of each byte of a DES key is
 actually a [parity bit](https://en.wikipedia.org/wiki/Parity_bit) that
@@ -477,3 +477,4 @@ https://github.com/weaversa/cryptol-course/issues
 || [+ Salsa20 Properties](../Salsa20/Salsa20Props.md) ||
 || [+ Transposition Ciphers](../Transposition/Contents.md) ||
 || [+ Project Euler](../ProjectEuler/ProjectEuler.md) ||
+|| [+ Continuous Reasoning with SAW](../SAW/SAW.md) ||

labs/SAW/Game/DLC/GameDLC.md

@@ -0,0 +1,117 @@
+# Game DLC
+
+This directory contains additional Game functions and SAW contracts for you to reference. You will notice:
+- `Makefile`: Provides the necessary steps to generate our bitcode and run our SAW Python scripts.
+- `src/`: Contains the source code we'll be analyzing
+- `proof/`: Contains our Python scripts to run our SAW contracts.
+- `specs/`: Contains our Cryptol specs that our SAW contracts can call.
+
+# DLC Functions
+
+Below is a list of functions included in Game/.
+
+## levelUp(uint32_t level)
+**Goal:** Determine how to set up and verify a very simple function in a SAW contract.
+
+**Lessons Learned**
+- How to declare a fresh variable in SAW
+- How to call a Cryptol function
+- How to pass SAW types to Cryptol function (curly braces)
+
+
+## getDefaultLevel()
+**Goal:** Determine how to handle global variables in a SAW contract.
+
+**Lessons Learned:**
+- How and when to use `global_initializer`
+  - When the source code already initializes the value and SAW should just use that value
+- How to declare a global variable in SAW (`global_var`)
+- How to set a global variable to an initialized value in a SAW contract (`points_to`)
+- When to pass no inputs to `execute_func`
+
+
+## initDefaultPlayer(player_t* player)
+**Goal:** Determine how to setup a struct variable in a SAW contract.
+
+**Lessons Learned:**
+- How and when to use `alias_ty`
+- How and when to use `alloc`
+  - Use `alloc` when you only consider the pointer
+  - Use `ptr_to_fresh` when you care about the values being referenced (i.e. for pre/postconditions) and the pointer
+- SAW only recognizes the base struct name (`player_t` vs `character_t`)
+- Passing global variables/parameters/defines defined in SAW to contracts
+  - Values copied from the source code's defines
+  - Examples: `MAX_NAME_LENGTH`, `SUCCESS`
+- How to assert postconditions using `points_to`
+- Compiling clang with the `-g` flag provides debug symbols, so you can reference fields names rather than just indices
+
+
+## checkStats(character_t* character)
+**Goal:** Determine how to use parameterized contracts to set preconditions and postconditions.
+
+**Lessons Learned:**
+- Understand that when a function's behavior depends on specific input value ranges, it may be necessary to define multiple cases for a given SAW contract
+  - Determine how to break a function into its fundamental case behaviors (i.e. `SUCCESS` and `FAILURE`)
+- How to parameterize a SAW contract
+  - Understand which parameter type is best for the job (i.e. `int`, `bool`, `string`, etc)
+- How to pass and use parameters within a SAW contract
+  - Note that SAW's Python API takes advantage of if-statements, which reduces the number of SAW contracts/specs that we need to write
+- Understand that `ptr_to_fresh` is useful for setting preconditions for a struct's fields
+- How to use contract parameters to assert two possible postconditions
+- How to represent multiple Unit Tests on the same contract with different input parameters
+
+**Additional Notes:**
+- Note that the `checkStats` function would be used in the Game library to check character stats every instance before such stats would be referenced/used for gameplay.
+- In terms of the example, `checkStats` provides gameplay balancing by limiting how well characters can perform.
+- Given this policy, all other functions included in the library assume that `checkStats` is called before them.
+  - This means we will use the preconditions from `checkStats_Contract` in their contracts
+  - We will show an example in `resolveAttack` about what happens when the preconditions aren't used
+- Discuss the coding & security tradeoffs between checks made in callers vs callees
+
+
+## resolveAttack(character_t* target, uint32_t atk)
+**Goal:** Expand upon the lessons learned with `checkStats` to get a contract ready for overrides/lemmas.
+
+**Lessons Learned:**
+- All of the points referenced in `checkStats` **Lessons Learned**
+- Understand how to write cases for a function with more than 2 possible behaviors
+- Understand when it is appropriate to include preconditions for functions that lack input checks
+  - Goes back to the caller vs callee tradeoffs mentioned in `checkStats` **Additional Notes**
+
+
+## selfDamage(player_t* player)
+**Goal:** To provide a case study where SAW should have complained about its memory disjoint assertion being violated. Note that SAW's Python API silently resolves this issue.
+
+
+## resetInventoryItems(inventory_t* inventory)
+**Goal:** To show the problems SAW faces when verifying structs with pointer fields.
+
+**Lessons Learned:**
+- Consider rewriting the source code to avoid unallocated pointers as it makes SAW happy and reduces assumptions code makes (improves security)
+
+
+## initScreen(screen_t* screen, uint8_t assetID)
+**Goal:** To provide a case study where SAW should have complained about not knowing what nested defines resolve to. Note that SAW's Python API silently resolves this issue.
+
+
+## setScreenTile(screen_t* screen, uint32_t screenIdx, uint32_t tableIdx)
+**Goal:** Demonstrate how to initialize an extern global array.
+
+**Lessons Learned:**
+- How to handle extern global variables when they aren't linked into the generated bitcode
+  - Copy extern definition to Cryptol spec file
+  - Could be possible to ignore the initialization if the bitcode links the file that implements the extern global (testing required)
+- Understand when `ptr_to_fresh` vs `self.alloc` is needed
+- Repointing a pointer to a SAW variable (`screen_post`) in order to use that variable for postconditions
+
+
+## quickBattle(player_t* player, character_t* opponent)
+**Goal:** To show how to pass overrides (lemmas) to a Unit test.
+
+**Lessons Learned:**
+- Must pass preconditions that match the preconditions included in the passed overrides
+
+**Additional Notes:**
+- The function assumes that both the player and opponent have non-zero HP values, otherwise there wouldn't be a battle!
+  - Explains why the `> 0` preconditions exist
+

labs/SAW/Game/DLC/Makefile

@@ -0,0 +1,20 @@
+# Note: Makefile assumes user already started the SAW remote API
+# $ start-saw-remote-api
+
+# Variables to hold relative file paths
+SRC=src
+PROOF=proof
+SPECS=specs
+ARTIFACTS=artifacts
+
+# Note: -g flag compiles the code with debug symbols enabled.
+#       The flag lets us pass field names in addition to indices for structs.
+all: artifacts
+	clang -c -g -emit-llvm -o $(ARTIFACTS)/Game.bc $(SRC)/Game.c
+	python3 $(PROOF)/Game.py
+
+artifacts:
+	mkdir $(ARTIFACTS)
+
+clean:
+	rm -r $(ARTIFACTS)