diff --git a/.github/workflows/python-saw.yml b/.github/workflows/python-saw.yml index eb60c594..369128f3 100644 --- a/.github/workflows/python-saw.yml +++ b/.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 diff --git a/.gitignore b/.gitignore index 79b5594d..09a0cf6b 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,3 @@ **/.DS_Store +**/*.bc +**/*~ diff --git a/README.md b/README.md index c5e02c09..ed029fe5 100644 --- a/README.md +++ b/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). diff --git a/labs/CryptoProofs/CryptoProofs.md b/labs/CryptoProofs/CryptoProofs.md index 699294a7..4d34cd31 100644 --- a/labs/CryptoProofs/CryptoProofs.md +++ b/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) || diff --git a/labs/CryptoProofs/CryptoProofsAnswers.md b/labs/CryptoProofs/CryptoProofsAnswers.md index cf5290e7..2b8ed9bc 100644 --- a/labs/CryptoProofs/CryptoProofsAnswers.md +++ b/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) || diff --git a/labs/SAW/Game/DLC/GameDLC.md b/labs/SAW/Game/DLC/GameDLC.md new file mode 100644 index 00000000..0783f5a7 --- /dev/null +++ b/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 + diff --git a/labs/SAW/Game/DLC/Makefile b/labs/SAW/Game/DLC/Makefile new file mode 100644 index 00000000..de95f0c7 --- /dev/null +++ b/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) \ No newline at end of file diff --git a/labs/SAW/Game/DLC/proof/Game.py b/labs/SAW/Game/DLC/proof/Game.py new file mode 100644 index 00000000..bd5cf71b --- /dev/null +++ b/labs/SAW/Game/DLC/proof/Game.py @@ -0,0 +1,570 @@ +####################################### +# Imporant Imports +####################################### + +import os +import unittest +from saw_client import * +from saw_client.crucible import * +from saw_client.llvm import * +from saw_client.proofscript import * +from saw_client.llvm_type import * + + +####################################### +# Defines and Constants +####################################### + +MAX_NAME_LENGTH = 12 +SUCCESS = 170 +FAILURE = 85 +MAX_STAT = 100 +SCREEN_ROWS = 15 +SCREEN_COLS = 10 +SCREEN_TILES = SCREEN_ROWS * SCREEN_COLS +NEUTRAL = 0 +DEFEAT_PLAYER = 1 +DEFEAT_OPPONENT = 2 +ASSET_TABLE_SIZE = 16 +GAITS = 2 +DIRECTIONS = 4 +ANIMATION_STEPS = 3 + +####################################### +# SAW Helper Functions +####################################### + +def ptr_to_fresh(spec: Contract, ty: LLVMType, + name: str) -> Tuple[FreshVar, SetupVal]: + var = spec.fresh_var(ty, name) + ptr = spec.alloc(ty, points_to = var) + return (var, ptr) + + +####################################### +# SAW Contracts +####################################### + +# levelUp Contract +# uint32_t levelUp(uint32_t level) +class levelUp_Contract(Contract): + def specification (self): + # Declare level variable + level = self.fresh_var(i32, "level") + + # Symbolically execute the function + self.execute_func(level) + + # Assert the function's return behavior + self.returns_f("levelUp {level}") + + +# initDefaultPlayer Contract +# uint32_t initDefaultPlayer(player_t* player) +class initDefaultPlayer_Contract(Contract): + def specification (self): + # Pull the struct from the bitcode + # Although the function uses player_t, pass character_t to SAW since + # player_t is an alternative typedef name for character_t. + player = self.alloc(alias_ty("struct.character_t")) + + # Symbolically execute the function + self.execute_func(player) + + # Assert the postcondition behaviors + + # Option 1: Assert one field at a time via points_to + self.points_to(player['name'], cry_f("repeat 0x41 : [{MAX_NAME_LENGTH}][8]")) + self.points_to(player['level'], cry_f("1 : [32]")) + self.points_to(player['hp'], cry_f("10 : [32]")) + self.points_to(player['atk'], cry_f("5 : [32]")) + self.points_to(player['def'], cry_f("4 : [32]")) + self.points_to(player['spd'], cry_f("3 : [32]")) + # Note: If bitcode isn't compiled with debug symbols enabled (no "-g" flag) + # then use the field indices instead. + # self.points_to(player[0], cry_f("repeat 0x41 : [{MAX_NAME_LENGTH}][8]")) + # self.points_to(player[1], cry_f("1 : [32]")) + # self.points_to(player[2], cry_f("10 : [32]")) + # self.points_to(player[3], cry_f("5 : [32]")) + # self.points_to(player[4], cry_f("4 : [32]")) + # self.points_to(player[5], cry_f("3 : [32]")) + + # Option 2: Assert all of the fields to a tuple + # self.points_to(player, cry_f("( repeat 0x41 : [{MAX_NAME_LENGTH}][8], 1 : [32], 10 : [32], 5 : [32], 4 : [32], 3 : [32] )")) + + # Pop Quiz: Why doesn't this work? + # self.points_to(player, cry_f("""{{ name = repeat 0x41 : [{MAX_NAME_LENGTH}][8], + # level = 1 : [32], + # hp = 10 : [32], + # atk = 5 : [32], + # def = 4 : [32], + # spd = 3 : [32] }}""")) + + self.returns(cry_f("`({SUCCESS}) : [32]")) + + +# initDefaultSprite Contract +# uint32_t initDefaultSprite(character_t* character, sprite_t* sprite) +class initDefaultSprite_Contract(Contract): + def specification (self): + # Declare variables + character = self.alloc(alias_ty("struct.character_t")) # For Option 1 + #character = self.fresh_var(ptr_ty(alias_ty("struct.character_t"))) # For Option 2 + tempCharacter_p = self.alloc(alias_ty("struct.character_t")) + ty = array_ty(GAITS, array_ty(DIRECTIONS, array_ty(ANIMATION_STEPS, i8))) + frames = self.fresh_var(ty, "sprite.frames") + xPos = self.fresh_var(i32, "sprite.xPos") + yPos = self.fresh_var(i32, "sprite.yPos") + sprite_p = self.alloc(alias_ty("struct.sprite_t"), points_to = struct(tempCharacter_p, frames, xPos, yPos)) + + # Symbolically execute the function + self.execute_func(character, sprite_p) + + # Assert postconditions + # Option 1: Struct Strategy + self.points_to(sprite_p, struct( character, + cry_f("zero : [{GAITS}][{DIRECTIONS}][{ANIMATION_STEPS}][8]"), + cry_f("1 : [32]"), + cry_f("2 : [32]") )) + # Option 2: Full Tuple Strategy + #self.points_to(sprite_p, cry_f("""( {character}, + # zero : [{GAITS}][{DIRECTIONS}][{ANIMATION_STEPS}][8], + # 1 : [32], + # 2 : [32]) """)) + + self.returns_f("`({SUCCESS}) : [32]") + + +# checkStats Contract +# uint32_t checkStats(character_t* character) +class checkStats_Contract(Contract): + def __init__(self, shouldPass : bool): + super().__init__() + self.shouldPass = shouldPass + # There are 2 possible cases for checkStats + # Case 1 (shouldPass == True): All of the stats are below the MAX_STAT cap + # Case 2 (shouldPass == False): At least one stat exceeds the MAX_STAT cap + + def specification (self): + # Declare variables + (character, character_p) = ptr_to_fresh(self, alias_ty("struct.character_t"), name="character") + + # Assert preconditions + if (self.shouldPass): + # Set up the preconditions to assure all stats are below the MAX_STAT cap + self.precondition_f("{character}.2 <= `{MAX_STAT}") + self.precondition_f("{character}.3 <= `{MAX_STAT}") + self.precondition_f("{character}.4 <= `{MAX_STAT}") + self.precondition_f("{character}.5 <= `{MAX_STAT}") + else: + # Note: Must meet at least one of the following preconditions to result + # in a failure (feel free to comment out as many as you want) + self.precondition_f("{character}.2 > `{MAX_STAT}") + self.precondition_f("{character}.3 > `{MAX_STAT}") + self.precondition_f("{character}.4 > `{MAX_STAT}") + self.precondition_f("{character}.5 > `{MAX_STAT}") + + # Symbolically execute the function + self.execute_func(character_p) + + # Assert the postcondition behavior + if (self.shouldPass): + self.returns(cry_f("`({SUCCESS}) : [32]")) + else: + self.returns(cry_f("`({FAILURE}) : [32]")) + + +# resolveAttack Contract +# void resolveAttack(character_t* target, uint32_t atk) +class resolveAttack_Contract(Contract): + def __init__(self, case : int): + super().__init__() + self.case = case + # There are 3 possible cases for resolveAttack + # Case 1: Attack mitigated + # Case 2: Immediate KO + # Case 3: Regular attack + # Each case results in a different function behavior for calculating the + # target's remaining HP. While we could make 3 separate contracts to handle + # all of the possible cases, we can pass a parameter to the contract, which + # identifies what preconditions and postconditions to set. + + def specification (self): + # Declare variables + (target, target_p) = ptr_to_fresh(self, alias_ty("struct.character_t"), name="target") + atk = self.fresh_var(i32, "atk") + + # Assert the precondition that the stats are below the max stat cap + # Pop Quiz: Why do we need these preconditions? + self.precondition_f("{atk} <= `{MAX_STAT}") + self.precondition_f("{target}.2 <= `{MAX_STAT}") + self.precondition_f("{target}.4 <= `{MAX_STAT}") + + # Determine the preconditions based on the case parameter + if (self.case == 1): + # target->def >= atk + self.precondition_f("{target}.4 >= {atk}") + elif (self.case == 2): + # target->hp <= (atk - target->def) + self.precondition_f("({target}.2 + {target}.4) <= {atk}") + # Pop Quiz: Are the following preconditions better for case 2? + # self.precondition_f("{target}.4 < {atk}") + # self.precondition_f("{target}.2 <= ({atk} - {target}.4)") + else: + # Assume any other case follows the formal attack calculation + self.precondition_f("{target}.4 < {atk}") + self.precondition_f("({target}.2 + {target}.4) > {atk}") + + # Symbolically execute the function + self.execute_func(target_p, atk) + + # Determine the postcondition based on the case parameter + if (self.case == 1): + self.points_to(target_p['hp'], cry_f("{target}.2 : [32]")) + # If bitcode is compiled without debug symbols enabled (no "-g" flag), use: + # self.points_to(target_p[2], cry_f("{target}.2 : [32]")) + elif (self.case == 2): + self.points_to(target_p['hp'], cry_f("0 : [32]")) + # If bitcode is compiled without debug symbols enabled (no "-g" flag), use: + # self.points_to(target_p[2], cry_f("0 : [32]")) + else: + self.points_to(target_p['hp'], cry_f("resolveAttack ({target}.2) ({target}.4) {atk}")) + # If bitcode is compiled without debug symbols enabled (no "-g" flag), use: + # self.points_to(target_p[2], cry_f("resolveAttack ({target}.2) ({target}.4) {atk}")) + + self.returns(void) + + +# selfDamage Contract +# uint32_t selfDamage(player_t* player) +class selfDamage_Contract(Contract): + def __init__(self, case : int): + super().__init__() + self.case = case + # There are 3 possible cases for resolveAttack + # Case 1: Attack mitigated + # Case 2: Immediate KO + # Case 3: Regular attack + # Each case results in a different function behavior for calculating the + # player's remaining HP. While we could make 3 separate contracts to handle + # all of the possible cases, we can pass a parameter to the contract, which + # identifies what preconditions and postconditions to set. + + def specification (self): + # Declare variables + (player, player_p) = ptr_to_fresh(self, alias_ty("struct.character_t"), name="player") + + # Assert the precondition that the player's HP is positive + # Why? Game logic assumes you can't damage yourself if you're already KO'd! + self.precondition_f("{player}.2 > 0") + + # Assert the precondition that character stats are below the max stat cap + # Pop Quiz: Explain why the proof fails when the following preconditions + # are commented out. + self.precondition_f("{player}.2 <= `{MAX_STAT}") + self.precondition_f("{player}.3 <= `{MAX_STAT}") + self.precondition_f("{player}.4 <= `{MAX_STAT}") + self.precondition_f("{player}.5 <= `{MAX_STAT}") + + # Determine the preconditions based on the case parameter + if (self.case == 1): + # player->def >= player->atk + self.precondition_f("{player}.4 >= {player}.3") + elif (self.case == 2): + # player->hp <= (player->atk - player->def) + self.precondition_f("({player}.2 + {player}.4) <= {player}.3") + else: + # Assume any other case follows the formal attack calculation + self.precondition_f("{player}.4 < {player}.3") + self.precondition_f("({player}.2 + {player}.4) > {player}.3") + + # Symbolically execute the function + self.execute_func(player_p, player_p) + + # Assert the postcondition + if (self.case == 1): + self.points_to(player_p['hp'], cry_f("{player}.2 : [32]")) + # If bitcode is compiled without debug symbols enabled (no "-g" flag), use: + # self.points_to(player_p[2], cry_f("{player}.2 : [32]")) + self.returns(cry_f("`({NEUTRAL}) : [32]")) + elif (self.case == 2): + self.points_to(player_p['hp'], cry_f("0 : [32]")) + # If bitcode is compiled without debug symbols enabled (no "-g" flag), use: + # self.points_to(player_p[2], cry_f("0 : [32]")) + self.returns(cry_f("`({DEFEAT_PLAYER}) : [32]")) + else: + self.points_to(player_p['hp'], cry_f("resolveAttack ({player}.2) ({player}.4) {player}.3")) + # If bitcode is compiled without debug symbols enabled (no "-g" flag), use: + # self.points_to(player_p[2], cry_f("resolveAttack ({player}.2) ({player}.4) {player}.3")) + self.returns(cry_f("`({NEUTRAL}) : [32]")) + + +# quickBattle Contract +# void quickBattle(player_t* player, character_t* opponent) +class quickBattle_Contract(Contract): + def specification (self): + # Declare variables + (player, player_p) = ptr_to_fresh(self, alias_ty("struct.character_t"), name="player") + (opponent, opponent_p) = ptr_to_fresh(self, alias_ty("struct.character_t"), name="opponent") + # Pop Quiz: Why does allocating the pointers in the following way yield an + # error? + #player = self.alloc(alias_ty("struct.character_t")) + #opponent = self.alloc(alias_ty("struct.character_t")) + + # Assert the precondition that both HPs are greater than 0 + # Why? Game logic assumes you can't attack if you're already KO'd! + self.precondition_f("{player}.2 > 0") + self.precondition_f("{opponent}.2 > 0") + + # Assert the precondition that character stats are below the max stat cap + # Pop Quiz: Explain why the proof fails when the following preconditions + # are commented out. + self.precondition_f("{player}.2 <= `{MAX_STAT}") + self.precondition_f("{player}.3 <= `{MAX_STAT}") + self.precondition_f("{player}.4 <= `{MAX_STAT}") + self.precondition_f("{player}.5 <= `{MAX_STAT}") + self.precondition_f("{opponent}.2 <= `{MAX_STAT}") + self.precondition_f("{opponent}.3 <= `{MAX_STAT}") + self.precondition_f("{opponent}.4 <= `{MAX_STAT}") + self.precondition_f("{opponent}.5 <= `{MAX_STAT}") + + # Symbolically execute the function + self.execute_func(player_p, opponent_p) + + # Assert the postcondition + self.returns(void) + + +# getDefaultLevel Contract +# uint32_t getDefaultLevel() +class getDefaultLevel_Contract(Contract): + def specification (self): + # Initialize the defaultLevel global variable + defaultLevel_init = global_initializer("defaultLevel") + self.points_to(global_var("defaultLevel"), defaultLevel_init) + + # Symbolically execute the function + self.execute_func() + + # Assert the function's return behavior + self.returns(defaultLevel_init) + + +# initScreen Contract +# uint32_t initScreen(screen_t* screen, uint8_t assetID) +class initScreen_Contract(Contract): + def specification (self): + # Declare variables + screen = self.alloc(alias_ty("struct.screen_t")) + assetID = self.fresh_var(i8, "assetID") + + # Symbolically execute the function + self.execute_func(screen, assetID) + + # Assert the postcondition + self.points_to(screen['tiles'], cry_f("repeat {assetID} : [{SCREEN_TILES}][8]")) + # If bitcode is compiled without debug symbols enabled (no "-g" flag), use: + # self.points_to(screen[0], cry_f("repeat {assetID} : [{SCREEN_TILES}][8]")) + + self.returns(cry_f("`({SUCCESS}) : [32]")) + + +# setScreenTile +# uint32_t setScreenTile(screen_t* screen, uint32_t screenIdx, uint32_t tableIdx) +class setScreenTile_Contract(Contract): + def __init__(self, shouldPass : bool): + super().__init__() + self.shouldPass = shouldPass + # There are 2 possible cases for setScreenTile + # Case 1 (shouldPass == True): Both screenIdx and tableIdx are below their + # limits, SCREEN_TILES and ASSET_TABLE_SIZE, + # respectively. + # Case 2 (shouldPass == False): At least one index exceeds its limits. + + def specification (self): + # Declare variables + (screen, screen_p) = ptr_to_fresh(self, alias_ty("struct.screen_t"), name="screen") + screenIdx = self.fresh_var(i32, "screenIdx") + tableIdx = self.fresh_var(i32, "tableIdx") + # Pop Quiz: Why can't we just declare and pass the screen pointer? + # screen_p = self.alloc(alias_ty("struct.screen_t")) + + # Initialize Game.h's assetTable according to Assets.c + # Note: The contents of assetTable from Assets.c was copied into Game.cry + # Required because the global variable in Game.h is declared as an extern, + # and the current way Game.bc is compiled does not include Assets.c in the + # Makefile. + self.points_to(global_var("assetTable"), cry_f("assetTable")) + + # Assert preconditions depending on the Contract parameter + if (self.shouldPass): + self.precondition_f("{screenIdx} < {SCREEN_TILES}") + self.precondition_f("{tableIdx} < {ASSET_TABLE_SIZE}") + else: + # Note: Only one of the following preconditions is needed + self.precondition_f("{screenIdx} >= {SCREEN_TILES}") + self.precondition_f("{tableIdx} >= {ASSET_TABLE_SIZE}") + + # Symbolically execute the function + self.execute_func(screen_p, screenIdx, tableIdx) + + # Since we just want to check one index, let's have our screen pointer + # point to a new screen_t variable. + screen_post = self.fresh_var(alias_ty("struct.screen_t"), "screen_post") + + # Assert that the original screen pointer now points to the new screen_t + # variable. This will allow us to reference screen_post in Cryptol for our + # later postconditions. + self.points_to(screen_p, screen_post) + + # Assert postconditions depending on the Contract parameter + if (self.shouldPass): + self.postcondition_f("({screen_post}@{screenIdx}) == assetTable@{tableIdx}") + #self.points_to(screen['tiles'][cry_f("{screenIdx}")], cry_f("assetTable@{tableIdx}")) + self.returns_f("`({SUCCESS}) : [32]") + else: + self.returns_f("`({FAILURE}) : [32]") + + +# resetInventoryItems Contract +# void resetInventoryItems(inventory_t* inventory) +class resetInventoryItems_Contract(Contract): + def __init__(self, numItems : int): + super().__init__() + self.numItems = numItems + # Note: The inventory_t struct defines its item field as a item_t pointer. + # Instead of declaring a fixed array size, the pointer enables for a + # variable size depending on the memory allocation configured by its + # caller. + # While this is valid C syntax, SAW and Cryptol require the known + # size ahead of time. Here, our contract takes the numItems parameter + # to declare a fixed array size. + + def specification (self): + # Declare variables + # Note: The setup here does not use item_p for the proof. However, item_p + # is included to show errors that can be encountered with the + # inventory_t struct. + (item, item_p) = ptr_to_fresh(self, array_ty(self.numItems, alias_ty("struct.item_t")), name="item") + inventory_p = self.alloc(alias_ty("struct.inventory_t"), points_to = struct(item, cry_f("{self.numItems} : [32]"))) + """ + If inventory_t is defined as: + typedef struct { + item_t* item; + uint32_t numItems; + } inventory_t; + + Attempt 1: + ========== + Passing item as so: + inventory_p = self.alloc(alias_ty("struct.inventory_t"), points_to = struct(item, cry_f("{self.numItems} : [32]"))) + + yields the following error: + ⚠️ Failed to verify: lemma_resetInventoryItems_Contract (defined at proof/Game.py:190): + error: types not memory-compatible: + { %struct.item_t*, i32 } + { [5 x { i32, i32 }], i32 } + + + stdout: + + Attempt 2: + ========== + Passing item_p as so: + inventory_p = self.alloc(alias_ty("struct.inventory_t"), points_to = struct(item_p, cry_f("{self.numItems} : [32]"))) + + yields the following error: + ⚠️ Failed to verify: lemma_resetInventoryItems_Contract (defined at proof/Game.py:190): + error: typeOfSetupValue: llvm_elem requires pointer to struct or array, found %struct.item_t** + stdout: + + Considering both of these verification setup attempts, we can see that + defining inventory_t with an item_t pointer is tough for SAW to setup and. + prove. Consequently, it is better to use fixed array lengths for structs! + """ + + # Symbolically execute the function + self.execute_func(inventory_p) + + # Assert the postconditions + for i in range(self.numItems): + self.points_to(inventory_p['item'][i][1], cry_f("0 : [32]")) + # If bitcode is compiled without debug symbols enabled (no "-g" flag), use: + # self.points_to(inventory_p[0][i][1], cry_f("0 : [32]")) + # Note: Even though debug symbols is enabled, SAW cannot resolve the + # "quantity" field, which is why we still use a 1 above. + + self.returns(void) + + +####################################### + + +####################################### +# Unit Tests +####################################### + +class GameTests(unittest.TestCase): + def test_Game(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults(verbose_failure=True)) + + pwd = os.getcwd() + bitcode_name = pwd + "/artifacts/Game.bc" + cryptol_name = pwd + "/specs/Game.cry" + + cryptol_load_file(cryptol_name) + module = llvm_load_module(bitcode_name) + + # Override(s) associated with basic SAW setup + levelUp_result = llvm_verify(module, 'levelUp', levelUp_Contract()) + + # Override(s) associated with basic struct initialization + initDefaultPlayer_result = llvm_verify(module, 'initDefaultPlayer', initDefaultPlayer_Contract()) + initDefaultSprite_result = llvm_verify(module, 'initDefaultSprite', initDefaultSprite_Contract()) + + # Overrides(s) associated with preconditions and postconditions that must + # be considered in SAW contracts & unit test overrides + checkStats_pass_result = llvm_verify(module, 'checkStats', checkStats_Contract(True)) + checkStats_fail_result = llvm_verify(module, 'checkStats', checkStats_Contract(False)) + resolveAttack_case1_result = llvm_verify(module, 'resolveAttack', resolveAttack_Contract(1)) + resolveAttack_case2_result = llvm_verify(module, 'resolveAttack', resolveAttack_Contract(2)) + resolveAttack_case3_result = llvm_verify(module, 'resolveAttack', resolveAttack_Contract(3)) + selfDamage_case1_result = llvm_verify(module, 'selfDamage', selfDamage_Contract(1), lemmas=[resolveAttack_case1_result, resolveAttack_case2_result, resolveAttack_case3_result]) + selfDamage_case2_result = llvm_verify(module, 'selfDamage', selfDamage_Contract(2), lemmas=[resolveAttack_case1_result, resolveAttack_case2_result, resolveAttack_case3_result]) + selfDamage_case3_result = llvm_verify(module, 'selfDamage', selfDamage_Contract(3), lemmas=[resolveAttack_case1_result, resolveAttack_case2_result, resolveAttack_case3_result]) + quickBattle_result = llvm_verify(module, 'quickBattle', quickBattle_Contract(), lemmas=[resolveAttack_case1_result, resolveAttack_case2_result, resolveAttack_case3_result]) + + # Override(s) associated with global variable handling + getDefaultLevel_result = llvm_verify(module, 'getDefaultLevel', getDefaultLevel_Contract()) + initScreen_result = llvm_verify(module, 'initScreen', initScreen_Contract()) + setScreenTile_pass_result = llvm_verify(module, 'setScreenTile', setScreenTile_Contract(True)) + setScreenTile_fail_result = llvm_verify(module, 'setScreenTile', setScreenTile_Contract(False)) + + # Override(s) showing limitations with struct pointer fields + resetInventoryItems_result = llvm_verify(module, 'resetInventoryItems', resetInventoryItems_Contract(5)) + + # Assert the overrides are successful + self.assertIs(levelUp_result.is_success(), True) + self.assertIs(initDefaultPlayer_result.is_success(), True) + self.assertIs(initDefaultSprite_result.is_success(), True) + self.assertIs(checkStats_pass_result.is_success(), True) + self.assertIs(checkStats_fail_result.is_success(), True) + self.assertIs(resolveAttack_case1_result.is_success(), True) + self.assertIs(resolveAttack_case2_result.is_success(), True) + self.assertIs(resolveAttack_case3_result.is_success(), True) + self.assertIs(selfDamage_case1_result.is_success(), True) + self.assertIs(selfDamage_case2_result.is_success(), True) + self.assertIs(selfDamage_case3_result.is_success(), True) + self.assertIs(quickBattle_result.is_success(), True) + self.assertIs(getDefaultLevel_result.is_success(), True) + self.assertIs(initScreen_result.is_success(), True) + self.assertIs(setScreenTile_pass_result.is_success(), True) + self.assertIs(setScreenTile_fail_result.is_success(), True) + self.assertIs(resetInventoryItems_result.is_success(), True) + + +if __name__ == "__main__": + unittest.main() + +####################################### diff --git a/labs/SAW/Game/DLC/specs/Game.cry b/labs/SAW/Game/DLC/specs/Game.cry new file mode 100644 index 00000000..559a14d4 --- /dev/null +++ b/labs/SAW/Game/DLC/specs/Game.cry @@ -0,0 +1,15 @@ +module Game where + + +assetTable = [0x01, 0x12, 0x23, 0x34, + 0x45, 0x56, 0x67, 0x78, + 0x89, 0x9A, 0xAB, 0xBC, + 0xCD, 0xDE, 0xEF, 0xF0] : [16][8] + +levelUp : [32] -> [32] +levelUp level = level + 1 + +resolveAttack : [32] -> [32] -> [32] -> [32] +resolveAttack hp def atk = hp' + where + hp' = hp - (atk - def) diff --git a/labs/SAW/Game/DLC/src/Assets.c b/labs/SAW/Game/DLC/src/Assets.c new file mode 100644 index 00000000..def3e4de --- /dev/null +++ b/labs/SAW/Game/DLC/src/Assets.c @@ -0,0 +1,6 @@ +#include "Game.h" + +const uint8_t assetTable[ASSET_TABLE_SIZE] = {0x01, 0x12, 0x23, 0x34, + 0x45, 0x56, 0x67, 0x78, + 0x89, 0x9A, 0xAB, 0xBC, + 0xCD, 0xDE, 0xEF, 0xF0}; \ No newline at end of file diff --git a/labs/SAW/Game/DLC/src/Game.c b/labs/SAW/Game/DLC/src/Game.c new file mode 100644 index 00000000..8dcc9fda --- /dev/null +++ b/labs/SAW/Game/DLC/src/Game.c @@ -0,0 +1,208 @@ +#include "Game.h" + + +/////////////////////////////////////// +// Function(s) with basic SAW setup +/////////////////////////////////////// + +uint32_t levelUp(uint32_t level) +{ + return (level + 1); +} + + +/////////////////////////////////////// +// Function(s) with basic struct initialization +/////////////////////////////////////// + +uint32_t initDefaultPlayer(player_t* player) +{ + // Variables + uint8_t i = 0; + uint32_t hp_default = 10; + uint32_t atk_default = 5; + uint32_t def_default = 4; + uint32_t spd_default = 3; + + // Initialize player according to some defaults + for (i = 0; i < MAX_NAME_LENGTH; i++) + { + // For simplicity, let's use A very cool name + // Assume ignoring the null terminator is fine too + // Remember, this is a dummy example ;) + player->name[i] = 'A'; + } + player->level = 1; + player->hp = hp_default; + player->atk = atk_default; + player->def = def_default; + player->spd = spd_default; + + return SUCCESS; +} + + +uint32_t initDefaultSprite(character_t* character, sprite_t* sprite) +{ + // Initialize the character to the passed pointer + sprite->character = character; + + // Initialize the sprite frames to the default asset + for (uint8_t i = 0; i < GAITS; i++) + { + for (uint8_t j = 0; j < DIRECTIONS; j++) + { + for (uint8_t k = 0; k < ANIMATION_STEPS; k++) + { + sprite->frames[i][j][k] = 0x00; + } + } + } + + // Initialize sprite's default position + sprite->xPos = 1; + sprite->yPos = 2; + + return SUCCESS; +} + + +/////////////////////////////////////// +// Function(s) with preconditions and postconditions that must +// be considered in SAW contracts & unit test overrides +/////////////////////////////////////// + +// Checks that the character stats are below MAX_STAT +// Note: MUST be called before running any function that uses character stats! +uint32_t checkStats(character_t* character) +{ + // Assume failure by default + uint32_t result = FAILURE; + + // Check the stats + if (character->hp <= MAX_STAT && + character->atk <= MAX_STAT && + character->def <= MAX_STAT && + character->spd <= MAX_STAT ) + { + result = SUCCESS; + } + + return result; +} + + +void resolveAttack(character_t* target, uint32_t atk) +{ + if ( target->def >= atk) + { + // The target's defense mitigates the attack + target->hp = target->hp; + } + else if ( target->hp <= (atk - target->def) ) + { + // The attack will knock out the target + target->hp = 0; + } + else + { + // Calculate damage as normal + target->hp = target->hp - (atk - target->def); + } +} + + +uint32_t selfDamage(player_t* player) +{ + enum battleResult result = NEUTRAL; + + // Player attacks itself (perhaps due to status condition) + resolveAttack(player, player->atk); + // Note: If SAW ever gives a "Memory not disjoint" error, then what SAW + // actually means is that inputs to an overridden function cannot + // overlap in memory. Given that player->atk is a field within player, + // the inputs overlap. + // Also consider the following way to have the player damage itself: + // quickBattle(player, player); + // This also contains inputs that overlap in memory (i.e. not disjoint). + // Bear in mind that both function calls in this example will not result in + // the Memory Disjoint error for the Python API. However, they will likely + // yield the same error if not using the Python API (i.e. llvm.saw). + + if (player->hp <= 0) + { + // Player's self damage results in a knockout + result = DEFEAT_PLAYER; + } + + return result; +} + + +// Simulates a simple battle where only the faster character attacks. +void quickBattle(player_t* player, character_t* opponent) +{ + if (player->spd >= opponent->spd) + { + resolveAttack(opponent, player->atk); + } + else + { + resolveAttack(player, opponent->atk); + } +} + + +/////////////////////////////////////// +// Function(s) with global variable handling +/////////////////////////////////////// + +uint32_t getDefaultLevel() +{ + return defaultLevel; +} + + +uint32_t initScreen(screen_t* screen, uint8_t assetID) +{ + // Iterate through the screen tiles and set their asset ID + for (int i = 0; i < SCREEN_TILES; i++) + { + screen->tiles[i] = assetID; + } + + return SUCCESS; +} + + +// Sets a tile displayed on the screen to an particular assetID held in the +// global assetTable +uint32_t setScreenTile(screen_t* screen, uint32_t screenIdx, uint32_t tableIdx) +{ + // Initialize return status to FAILURE + uint32_t result = FAILURE; + + // Check for valid bounds + if (screenIdx < SCREEN_TILES && tableIdx < ASSET_TABLE_SIZE) + { + screen->tiles[screenIdx] = assetTable[tableIdx]; + result = SUCCESS; + } + + return result; +} + + + +/////////////////////////////////////// +// Function(s) showing limitations with struct pointer fields +/////////////////////////////////////// + +void resetInventoryItems(inventory_t* inventory) +{ + // Iterate through the inventory and set the quantity field to 0 + for (int i = 0; i < inventory->numItems; i++) + { + inventory->item[i].quantity = 0; + } +} diff --git a/labs/SAW/Game/DLC/src/Game.h b/labs/SAW/Game/DLC/src/Game.h new file mode 100644 index 00000000..e646b22c --- /dev/null +++ b/labs/SAW/Game/DLC/src/Game.h @@ -0,0 +1,109 @@ +#ifndef GAME_H +#define GAME_H + +#include + +#define MAX_NAME_LENGTH 12 +#define SUCCESS 170 // 170 = 0xAA = 10101010 +#define FAILURE 85 // 85 = 0x55 = 01010101 +#define MAX_STAT 100 +#define SCREEN_ROWS 15 +#define SCREEN_COLS 10 +#define SCREEN_TILES SCREEN_ROWS*SCREEN_COLS +#define ASSET_TABLE_SIZE 16 +#define GAITS 2 // Possible gaits to animate: walk and run +#define DIRECTIONS 4 // 2D game, 4 directions (up, down, left, right) +#define ANIMATION_STEPS 3 // 3 frames per direction (stand, left leg forward, right leg forward) + + +/////////////////////////////////////// +// Globals +/////////////////////////////////////// + +const uint32_t defaultLevel = 1; +extern const uint8_t assetTable[ASSET_TABLE_SIZE]; + + +/////////////////////////////////////// +// Enums +/////////////////////////////////////// + +// Enum containing possible battle outcomes +enum battleResult{ + NEUTRAL = 0, + DEFEAT_PLAYER = 1, + DEFEAT_OPPONENT = 2 +}; + + +/////////////////////////////////////// +// Structs +/////////////////////////////////////// + +// Struct containing character information +typedef struct { + uint8_t name[MAX_NAME_LENGTH]; + uint32_t level; + uint32_t hp; + uint32_t atk; + uint32_t def; + uint32_t spd; +} character_t; + +typedef character_t player_t; + +// Struct containing item information +typedef struct { + uint32_t id; + uint32_t quantity; +} item_t; + +// Struct containing inventory information +typedef struct { + //item_t* item; // Assume this points to an item_t array of unknown length + item_t item[5]; + uint32_t numItems; +} inventory_t; + +// Struct containing screen information +typedef struct { + uint8_t tiles[SCREEN_TILES]; // Holds asset ID for each screen tile +} screen_t; + +// Struct containing information on a character sprite +typedef struct { + character_t* character; + uint8_t frames[GAITS][DIRECTIONS][ANIMATION_STEPS]; + uint32_t xPos; // x position relative to the screen + uint32_t yPos; // y position relative to the screen +} sprite_t; + + +/////////////////////////////////////// +// Function prototypes +/////////////////////////////////////// + +// Function(s) with basic SAW setup +uint32_t levelUp(uint32_t level); + +// Function(s) with basic struct initialization +uint32_t initDefaultPlayer(player_t* player); +uint32_t initDefaultSprite(character_t* character, sprite_t* sprite); + +// Function(s) with preconditions and postconditions that must +// be considered in SAW contracts & unit test overrides +uint32_t checkStats(character_t* character); +void resolveAttack(character_t* target, uint32_t atk); +uint32_t selfDamage(player_t* player); +void quickBattle(player_t* player, character_t* opponent); + +// Function(s) with global variable handling +uint32_t getDefaultLevel(); +uint32_t initScreen(screen_t* screen, uint8_t assetID); +uint32_t setScreenTile(screen_t* screen, uint32_t screenIdx, uint32_t tableIdx); + +// Function(s) showing limitations with struct pointer fields +void resetInventoryItems(inventory_t* inventory); + + +#endif \ No newline at end of file diff --git a/labs/SAW/Game/Makefile b/labs/SAW/Game/Makefile new file mode 100644 index 00000000..de95f0c7 --- /dev/null +++ b/labs/SAW/Game/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) \ No newline at end of file diff --git a/labs/SAW/Game/proof/Game.py b/labs/SAW/Game/proof/Game.py new file mode 100644 index 00000000..8c56ebc8 --- /dev/null +++ b/labs/SAW/Game/proof/Game.py @@ -0,0 +1,145 @@ +####################################### +# Imporant Imports +####################################### + +import os +import unittest +from saw_client import * +from saw_client.crucible import * +from saw_client.llvm import * +from saw_client.proofscript import * +from saw_client.llvm_type import * + + +####################################### +# Defines and Constants +####################################### + +MAX_NAME_LENGTH = 12 +SUCCESS = 170 +FAILURE = 85 +MAX_STAT = 100 +GAITS = 2 +DIRECTIONS = 4 +ANIMATION_STEPS = 3 + + +####################################### +# SAW Helper Functions +####################################### + +def ptr_to_fresh(spec: Contract, ty: LLVMType, + name: str) -> Tuple[FreshVar, SetupVal]: + var = spec.fresh_var(ty, name) + ptr = spec.alloc(ty, points_to = var) + return (var, ptr) + + +####################################### +# SAW Contracts +####################################### + +# initDefaultPlayer Contract +# uint32_t initDefaultPlayer(player_t* player) +class initDefaultPlayer_Contract(Contract): + def specification (self): + # TODO: Declare variables + + + # TODO: Assert preconditions + + + # TODO: Symbolically execute the function + + + # TODO: Assert postconditions + + + # TODO: Remove the following line when you have something! + pass + + +# initDefaultSprite Contract +# uint32_t initDefaultSprite(character_t* character, sprite_t* sprite) +class initDefaultSprite_Contract(Contract): + def specification (self): + # TODO: Declare variables + + + # TODO: Assert preconditions + + + # TODO: Symbolically execute the function + + + # TODO: Assert postconditions + + + # TODO: Remove the following line when you have something! + pass + + +# resolveAttack Contract +# void resolveAttack(character_t* target, uint32_t atk) +class resolveAttack_Contract(Contract): + def specification (self): + # TODO: Declare variables + + + # TODO: Assert preconditions + + + # TODO: Symbolically execute the function + + + # TODO: Assert postconditions + + + # TODO: Remove the following line when you have something! + pass + + +# checkStats Contract +# uint32_t checkStats(character_t* character) +class checkStats_Contract(Contract): + def specification (self): + # TODO: Declare variables + + + # TODO: Assert preconditions + + + # TODO: Symbolically execute the function + + + # TODO: Assert postconditions + + + # TODO: Remove the following line when you have something! + pass + + +####################################### +# Unit Tests +####################################### + +class GameTests(unittest.TestCase): + def test_Game(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults(verbose_failure=True)) + + pwd = os.getcwd() + bitcode_name = pwd + "/artifacts/Game.bc" + cryptol_name = pwd + "/specs/Game.cry" + + cryptol_load_file(cryptol_name) + module = llvm_load_module(bitcode_name) + + # TODO: Set up verification overrides + + + # TODO: Assert the overrides are successful + + +if __name__ == "__main__": + unittest.main() diff --git a/labs/SAW/Game/proof/Game_answers.py b/labs/SAW/Game/proof/Game_answers.py new file mode 100644 index 00000000..1f83c855 --- /dev/null +++ b/labs/SAW/Game/proof/Game_answers.py @@ -0,0 +1,215 @@ +####################################### +# Imporant Imports +####################################### + +import os +import unittest +from saw_client import * +from saw_client.crucible import * +from saw_client.llvm import * +from saw_client.proofscript import * +from saw_client.llvm_type import * + + +####################################### +# Defines and Constants +####################################### + +MAX_NAME_LENGTH = 12 +SUCCESS = 170 +FAILURE = 85 +MAX_STAT = 100 +GAITS = 2 +DIRECTIONS = 4 +ANIMATION_STEPS = 3 + + +####################################### +# SAW Helper Functions +####################################### + +def ptr_to_fresh(spec: Contract, ty: LLVMType, + name: str) -> Tuple[FreshVar, SetupVal]: + var = spec.fresh_var(ty, name) + ptr = spec.alloc(ty, points_to = var) + return (var, ptr) + + +####################################### +# SAW Contracts +####################################### + +# initDefaultPlayer Contract +# uint32_t initDefaultPlayer(player_t* player) +class initDefaultPlayer_Contract(Contract): + def specification (self): + # Pull the struct from the bitcode + # Although the function uses player_t, pass character_t to SAW since + # player_t is an alternative typedef name for character_t. + player = self.alloc(alias_ty("struct.character_t")) + + # Symbolically execute the function + self.execute_func(player) + + # Assert the postcondition behaviors + self.points_to(player['name'], cry_f("repeat 0x41 : [{MAX_NAME_LENGTH}][8]")) + self.points_to(player['level'], cry_f("1 : [32]")) + self.points_to(player['hp'], cry_f("10 : [32]")) + self.points_to(player['atk'], cry_f("5 : [32]")) + self.points_to(player['def'], cry_f("4 : [32]")) + self.points_to(player['spd'], cry_f("3 : [32]")) + + self.returns(cry_f("`({SUCCESS}) : [32]")) + + +# initDefaultSprite Contract +# uint32_t initDefaultSprite(character_t* character, sprite_t* sprite) +class initDefaultSprite_Contract(Contract): + def specification (self): + # Declare variables + character = self.alloc(alias_ty("struct.character_t")) + tempCharacter_p = self.alloc(alias_ty("struct.character_t")) + ty = array_ty(GAITS, array_ty(DIRECTIONS, array_ty(ANIMATION_STEPS, i8))) + frames = self.fresh_var(ty, "sprite.frames") + xPos = self.fresh_var(i32, "sprite.xPos") + yPos = self.fresh_var(i32, "sprite.yPos") + sprite_p = self.alloc(alias_ty("struct.sprite_t"), points_to = struct(tempCharacter_p, frames, xPos, yPos)) + + # Symbolically execute the function + self.execute_func(character, sprite_p) + + # Assert postconditions + self.points_to(sprite_p, struct( character, + cry_f("zero : [{GAITS}][{DIRECTIONS}][{ANIMATION_STEPS}][8]"), + cry_f("1 : [32]"), + cry_f("2 : [32]") )) + + self.returns_f("`({SUCCESS}) : [32]") + + +# resolveAttack Contract +# void resolveAttack(character_t* target, uint32_t atk) +class resolveAttack_Contract(Contract): + def __init__(self, case : int): + super().__init__() + self.case = case + # There are 3 possible cases for resolveAttack + # Case 1: Attack mitigated + # Case 2: Immediate KO + # Case 3: Regular attack + # Each case results in a different function behavior for calculating the + # target's remaining HP. While we could make 3 separate contracts to handle + # all of the possible cases, we can pass a parameter to the contract, which + # identifies what preconditions and postconditions to set. + + def specification (self): + # Declare variables + (target, target_p) = ptr_to_fresh(self, alias_ty("struct.character_t"), name="target") + atk = self.fresh_var(i32, "atk") + + # Assert the precondition that the stats are below the max stat cap + self.precondition_f("{atk} <= `{MAX_STAT}") + self.precondition_f("{target}.2 <= `{MAX_STAT}") + self.precondition_f("{target}.4 <= `{MAX_STAT}") + + # Determine the preconditions based on the case parameter + if (self.case == 1): + # target->def >= atk + self.precondition_f("{target}.4 >= {atk}") + elif (self.case == 2): + # target->hp <= (atk - target->def) + self.precondition_f("({target}.2 + {target}.4) <= {atk}") + else: + # Assume any other case follows the formal attack calculation + self.precondition_f("{target}.4 < {atk}") + self.precondition_f("({target}.2 + {target}.4) > {atk}") + + # Symbolically execute the function + self.execute_func(target_p, atk) + + # Determine the postcondition based on the case parameter + if (self.case == 1): + self.points_to(target_p['hp'], cry_f("{target}.2 : [32]")) + elif (self.case == 2): + self.points_to(target_p['hp'], cry_f("0 : [32]")) + else: + self.points_to(target_p['hp'], cry_f("resolveAttack ({target}.2) ({target}.4) {atk}")) + + self.returns(void) + + +# checkStats Contract +# uint32_t checkStats(character_t* character) +class checkStats_Contract(Contract): + def __init__(self, shouldPass : bool): + super().__init__() + self.shouldPass = shouldPass + # There are 2 possible cases for checkStats + # Case 1 (shouldPass == True): All of the stats are below the MAX_STAT cap + # Case 2 (shouldPass == False): At least one stat exceeds the MAX_STAT cap + + def specification (self): + # Declare variables + (character, character_p) = ptr_to_fresh(self, alias_ty("struct.character_t"), name="character") + + # Assert preconditions + if (self.shouldPass): + # Set up the preconditions to assure all stats are below the MAX_STAT cap + self.precondition_f("{character}.2 <= `{MAX_STAT}") + self.precondition_f("{character}.3 <= `{MAX_STAT}") + self.precondition_f("{character}.4 <= `{MAX_STAT}") + self.precondition_f("{character}.5 <= `{MAX_STAT}") + else: + # Note: Must meet at least one of the following preconditions to result + # in a failure (feel free to comment out as many as you want) + self.precondition_f("{character}.2 > `{MAX_STAT}") + self.precondition_f("{character}.3 > `{MAX_STAT}") + self.precondition_f("{character}.4 > `{MAX_STAT}") + self.precondition_f("{character}.5 > `{MAX_STAT}") + + # Symbolically execute the function + self.execute_func(character_p) + + # Assert the postcondition behavior + if (self.shouldPass): + self.returns(cry_f("`({SUCCESS}) : [32]")) + else: + self.returns(cry_f("`({FAILURE}) : [32]")) + + +####################################### +# Unit Tests +####################################### + +class GameTests(unittest.TestCase): + def test_Game(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults(verbose_failure=True)) + + pwd = os.getcwd() + bitcode_name = pwd + "/artifacts/Game.bc" + cryptol_name = pwd + "/specs/Game.cry" + + cryptol_load_file(cryptol_name) + module = llvm_load_module(bitcode_name) + + # Set up verification overrides + initDefaultPlayer_result = llvm_verify(module, 'initDefaultPlayer', initDefaultPlayer_Contract()) + initDefaultSprite_result = llvm_verify(module, 'initDefaultSprite', initDefaultSprite_Contract()) + resolveAttack_case1_result = llvm_verify(module, 'resolveAttack' , resolveAttack_Contract(1) ) + resolveAttack_case2_result = llvm_verify(module, 'resolveAttack' , resolveAttack_Contract(2) ) + resolveAttack_case3_result = llvm_verify(module, 'resolveAttack' , resolveAttack_Contract(3) ) + checkStats_pass_result = llvm_verify(module, 'checkStats' , checkStats_Contract(True) ) + checkStats_fail_result = llvm_verify(module, 'checkStats' , checkStats_Contract(False) ) + + # Assert the overrides are successful + self.assertIs(initDefaultPlayer_result.is_success() , True) + self.assertIs(initDefaultSprite_result.is_success() , True) + self.assertIs(resolveAttack_case1_result.is_success(), True) + self.assertIs(resolveAttack_case2_result.is_success(), True) + self.assertIs(resolveAttack_case3_result.is_success(), True) + self.assertIs(checkStats_pass_result.is_success() , True) + self.assertIs(checkStats_fail_result.is_success() , True) + +if __name__ == "__main__": + unittest.main() diff --git a/labs/SAW/Game/specs/Game.cry b/labs/SAW/Game/specs/Game.cry new file mode 100644 index 00000000..951162c5 --- /dev/null +++ b/labs/SAW/Game/specs/Game.cry @@ -0,0 +1,7 @@ +module Game where + + +resolveAttack : [32] -> [32] -> [32] -> [32] +resolveAttack hp def atk = hp' + where + hp' = hp - (atk - def) diff --git a/labs/SAW/Game/src/Game.c b/labs/SAW/Game/src/Game.c new file mode 100644 index 00000000..ea1f4d52 --- /dev/null +++ b/labs/SAW/Game/src/Game.c @@ -0,0 +1,91 @@ +#include "Game.h" + + +uint32_t initDefaultPlayer(player_t* player) +{ + // Variables + uint8_t i = 0; + uint32_t hp_default = 10; + uint32_t atk_default = 5; + uint32_t def_default = 4; + uint32_t spd_default = 3; + + // Initialize player according to some defaults + for (i = 0; i < MAX_NAME_LENGTH; i++) + { + // For simplicity, let's use A very cool name + // Assume ignoring the null terminator is fine too + // Remember, this is a dummy example ;) + player->name[i] = 'A'; + } + player->level = 1; + player->hp = hp_default; + player->atk = atk_default; + player->def = def_default; + player->spd = spd_default; + + return SUCCESS; +} + + +uint32_t initDefaultSprite(character_t* character, sprite_t* sprite) +{ + // Initialize the character to the passed pointer + sprite->character = character; + + // Initialize the sprite frames to the default asset + for (uint8_t i = 0; i < GAITS; i++) + { + for (uint8_t j = 0; j < DIRECTIONS; j++) + { + for (uint8_t k = 0; k < ANIMATION_STEPS; k++) + { + sprite->frames[i][j][k] = 0x00; + } + } + } + + // Initialize sprite's default position + sprite->xPos = 1; + sprite->yPos = 2; + + return SUCCESS; +} + + +void resolveAttack(character_t* target, uint32_t atk) +{ + if ( target->def >= atk) + { + // The target's defense mitigates the attack + target->hp = target->hp; + } + else if ( target->hp <= (atk - target->def) ) + { + // The attack will knock out the target + target->hp = 0; + } + else + { + // Calculate damage as normal + target->hp = target->hp - (atk - target->def); + } +} + + +uint32_t checkStats(character_t* character) +{ + // Assume failure by default + uint32_t result = FAILURE; + + // Check the stats + if (character->hp <= MAX_STAT && + character->atk <= MAX_STAT && + character->def <= MAX_STAT && + character->spd <= MAX_STAT ) + { + result = SUCCESS; + } + + return result; +} \ No newline at end of file diff --git a/labs/SAW/Game/src/Game.h b/labs/SAW/Game/src/Game.h new file mode 100644 index 00000000..7f118bd3 --- /dev/null +++ b/labs/SAW/Game/src/Game.h @@ -0,0 +1,81 @@ +#ifndef GAME_H +#define GAME_H + +#include + + +// Status values that provide a hamming distance of 5 +#define SUCCESS 170 // 170 = 0xAA = 10101010 +#define FAILURE 85 // 85 = 0x55 = 01010101 + +#define MAX_NAME_LENGTH 12 // Maximum number of bytes in a character name +#define MAX_STAT 100 // Inclusive upper bound limit on character stats + +#define GAITS 2 // Possible gaits to animate: walk and run +#define DIRECTIONS 4 // 2D game, 4 directions (up, down, left, right) +#define ANIMATION_STEPS 3 // 3 frames per direction (stand, left leg forward, right leg forward) + + +/////////////////////////////////////// +// Structs +/////////////////////////////////////// + +// Contains information about in-game characters +typedef struct { + uint8_t name[MAX_NAME_LENGTH]; + uint32_t level; + uint32_t hp; + uint32_t atk; + uint32_t def; + uint32_t spd; +} character_t; + +typedef character_t player_t; + +// Contains information related to character sprites +typedef struct { + character_t* character; + uint8_t frames[GAITS][DIRECTIONS][ANIMATION_STEPS]; + uint32_t xPos; // x position relative to the screen + uint32_t yPos; // y position relative to the screen +} sprite_t; + + +/////////////////////////////////////// +// Function prototypes +/////////////////////////////////////// + +/** + Initializes a player variable based on default parameters. + \param player_t* player - Pointer to an allocated player variable. + \return SUCCESS. +**/ +uint32_t initDefaultPlayer(player_t* player); + +/** + Initializes a sprite variable based on default parameters and ties the sprite + to the passed character reference. + \param character_t* character - Pointer to a character variable that the + the sprite should be tied to. + \param sprite_t* sprite - Pointer to an allocated sprite variable. + \return SUCCESS. +**/ +uint32_t initDefaultSprite(character_t* character, sprite_t* sprite); + +/** + Resolves a target's hp stat after an attack. + \param character_t* target - Defender during the attack. + \param uint32_t atk - Attacker's atk stat. + \return None. +**/ +void resolveAttack(character_t* target, uint32_t atk); + +/** + Checks whether the referenced character's stats are at or below the MAX_STAT. + \param character_t* character - Pointer to the character in question. + \return SUCCESS when all stats are <= MAX_STAT, or FAILURE otherwise. +**/ +uint32_t checkStats(character_t* character); + + +#endif diff --git a/labs/SAW/SAW.md b/labs/SAW/SAW.md new file mode 100644 index 00000000..922bfafe --- /dev/null +++ b/labs/SAW/SAW.md @@ -0,0 +1,2057 @@ +# Introduction + +This is a tutorial aimed at training developers how to leverage the +[Software Analysis Workbench (SAW)](https://saw.galois.com) and +Cryptol to develop and verify cryptographic implementations in a +[Continuous Reasoning](https://dl.acm.org/doi/abs/10.1145/3209108.3209109) +paradigm. Continuous Reasoning is, roughly, + +> formal reasoning about a (changing) codebase ... done in a fashion +> which mirrors the iterative, continuous model of software +> development that is increasingly practiced in industry. + +SAW and Cryptol can be used by a Continuous Integration (CI) system to +enforce invariants (safety, security, and functional) that software +must have at certain stages in a software development pipeline. Some +industrial examples include [AWS's s2n](https://link.springer.com/chapter/10.1007/978-3-319-96142-2_26) +and [Supranational's BLST](https://github.com/GaloisInc/BLST-Verification). + +## Prerequisites + +Before working through this lab, you'll need + * A recent version of Python, Cryptol, SAW, saw-remote-api, SAW's Python client package, and the clang C compiler to be installed and + * an editor for completing the exercises in this file. + +You'll also need experience with the following languages + * Python + * Cryptol + * SAW + * C + +## Skills You'll Learn + +By the end of this lab you will be comfortable using SAW's remote API +to formally verify cryptographic implementations. Since the bulk of +work with SAW lies in crafting linkages between the source language +and spec, this lab is filled with examples of different types of data +structures and how to represent them in SAW. Hence, this lab also +exists as a kind of reference that you may return to when using these +tools. As well, there are some examples +[here](https://github.com/GaloisInc/saw-script/tree/master/saw-remote-api/python/tests) +and a full-featured tutorial on SAW +[here](https://saw.galois.com/intro/). + +# Setting Everything Up + +To run any of the examples in this lab, you need to first start the +Software Analysis Workbench (SAW) remote API (`saw-remote-api`). If +you are using the development container that comes with this course +(`ghcr.io/weaversa/cryptol-course`), you can enter the following +command in your terminal: + +```sh +$ start-saw-remote-api +``` + +Otherwise, this tool can be installed by following the instructions +for SAW found in the [Installation lab](../../INSTALL.md). Once +installed, to run `saw-remote-api`, enter the following commands into +your terminal: + +```sh +$ export SAW_SERVER_URL=http://0.0.0.0:36691 +$ saw-remote-api http --host 0.0.0.0 --port 36691 & +``` + +Congrats! You now have a server version of SAW running in the +background ready to accept commands on port `36691`. + +# SAW and Python + +If you followed the instructions above, you now have SAW running in +the background, waiting for a connection on port `36691`. Galois +provides a [Python client package](https://pypi.org/project/saw-client/) +that allows you to write formal/logical contracts to enforce +invariants on some given software. + +# Python Contracts Introduction + +Here's the general layout for SAW in Python: + +```python +# Import SAW's Python modules + +class contractName(Contract): + def specification(self): + # Initialization and Preconditions + # Execute Function + # Initialization for output variables (optional) + # Postconditions and Return + +class testName(unittest.TestCase): + def specificTestName(self): + # Verify contracts + +if __name__ == "__main__": + unittest.main() +``` + +## Imports + +To start making Python contracts first import the necessary files: + +```python +import unittest +from saw_client import * +from saw_client.crucible import * +from saw_client.llvm import * +from saw_client.proofscript import * +from saw_client.llvm_type import * +``` + +We put `*` for simplicity, but if one only wanted certain functions, +they could refer to this table for some common imports: + +|Package | Values | +|---------------------|--------| +|`saw_client.crucible`| `cry`, `cry_f`| +|`saw_client.llvm` | `Contract`, `CryptolTerm`, `SetupVal`, `FreshVar`, `i8`, `i32`, `i64`, `void`, `null`, `array_ty`, `field`, `struct`, `alias_ty` | +|`saw_client.llvm_type` | `LLVMType`, `LLVMArrayType` | + +## Left Circular Shift Example + +To see contracts in action we need an example. Here's some C code for +left circular shift we want to verify: + +```C +uint32_t rotl(uint32_t bits, uint32_t shift) { + return (bits << shift) | (bits >> (sizeof(bits) * 8 - shift)); +} +``` + +In this example, SAW won't actually verify C source, but rather C +compiled down to LLVM intermediate representation (IR), or +bitcode. This can be accomplished via the `clang` compiler. In this +instance, we can create the bitcode by entering the following command +in a terminal. + +```sh +$ clang -emit-llvm labs/SAW/src/rotl.c -c -o labs/SAW/src/rotl.bc +``` + +We can inspect the bitcode using SAW by loading the module and +printing some meta-data. + +```Xsaw-session +$ saw + ┏━━━┓━━━┓━┓━┓━┓ + ┃ ━━┓ ╻ ┃ ┃ ┃ ┃ + ┣━━ ┃ ╻ ┃┓ ╻ ┏┛ + ┗━━━┛━┛━┛┗━┛━┛ version 0.9.0.99 () + +sawscript> r <- llvm_load_module "labs/SAW/src/rotl.bc" +sawscript> print r +Module: rotl.bc +Types: + +Globals: + +External references: + +Definitions: + i32 @rotl(i32 %0, i32 %1) + +``` + +The corresponding Cryptol specification for left circular shift is: + +```cryptol +rotl : [32] -> [32] -> [32] +rotl xs shift = xs <<< shift +``` + +For the SAW Python API we make a `Contract` object with the required +`specification` function: + +```python +class rotl_Contract(Contract): + def specification(self): + bits = self.fresh_var(i32, "bits") + shift = self.fresh_var(i32, "shift") + + self.execute_func(bits, shift) + + self.returns_f("rotl {bits} {shift}") +``` + +Let's break down `specification` piece by piece. + +### Fresh Symbolic Variables + +The command `self.fresh_var(type, name)` creates a new symbolic +variable of type `type` and name `name`, where `name` is a +string. Names for fresh symbolic variables are not optional inputs, +though they mostly serve displaying names in counter-examples and +error messages. The string can be anything, but it makes sense to give +it the name of the variable being defined. + +### Execute Functions + +The command `self.execute_func(input1, input2, ...)` will symbolically +execute the function we're writing a contract for. There should be +exactly as many comma separated inputs as there are in the C +function. One can only place preconditions before this command and +postconditions after this command. + +### Return Statements + +The command `self.returns_f(string)` is a postcondition that asserts +the function returns a given Cryptol term (parsed from a Python +string). To use Python variables in scope within the string use +`{variable_name}`. For example, + +|`self.`|`returns_f(`|`"rotl {bits} {shift}"`|)| +|-------|-----------|---------------------|----| +|In this contract| assert the current function returns the Cryptol term | left circular shift `bits` by `shift` |.| + +Sometimes we don't want to return a Cryptol term. In those cases we +can just use `returns(someSetupValue)`. The specification function of +a Contract must **always** have a `self.returns(someSetupValue)` or +`self.returns_f(string)` statement. If the function returns `void`, one +can use `self.returns(void)`. + +### Terms from Cryptol + +The command `cry(string)` converts a Python string into a +`CryptolTerm` that can be used in SAW. The `cry_f(string)` command is +similar to `cry`, but the `_f` indicates one can pass Python local +variables into the strings. To do this, surround the variable with +braces as we did in `returns_f("{bits} >>> {shift}")`. In fact, +`returns_f` is just syntactic sugar for `returns(cry_f(string))`. In +general, `cry_f` and friends are mostly a wrapper around [formatted string literals](https://docs.python.org/3/tutorial/inputoutput.html#formatted-string-literals) +called "f-strings". + +The `CryptolTerm` class is a subclass of `SetupVal`. This allows using +`CryptolTerm` as a `SetupVal`. + +Braces are sometimes used in Cryptol to assign type parameters or +declare records. The symbols `{{` and `}}` are used to denote literal +braces for these cases when parsing Python strings. For example, +let's think about how to parse the following line: + +```python + self.returns_f("{{a = take`{{5}} {var}, b = take`{{{N}}} {var} }} == foo `eel") +``` + +If `var` is a local Python variable equal to `23` and `N` is a +local Python variable equal to `2`, then the string parses in Cryptol as + +```cryptol +{a = take`{5} 23, b = take`{2} 23} == foo `eel +``` + +where `foo` is some Cryptol function returning a record and `eel` is +some Cryptol type in the currently loaded specification. + +## Unit Testing + +```python +class rotlTest(unittest.TestCase): + def test_rotl(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults(verbose_failure=True)) + + bcname = "/some/path/to/your/file.bc" + mod = llvm_load_module(bcname) + + cryname = "/some/path/to/your/file.cry" + cryptol_load_file(cryname) + + rotl_result = llvm_verify(mod, 'rotl', rotl_Contract()) + self.assertIs(rotl_result.is_success(), True) +``` + +For a contract, the specification function should be called +`specification`. For tests, it doesn't matter what you name your +tests. Here we named it `test_rotl`. These tests will be run when you +run the Python program. + +Let's break down the first few lines of this function: + +- The command `connect(reset_server=True)` connects to the server so + we can use the SAW Python API. +- The line `if __name__ == "__main__": + view(LogResults(verbose_failure=True))` allows us to view the output + with verbose error messages. If you don't want verbose error + messages, then just use `if __name__ == "__main__": + view(LogResults())`. +- The line `bcname = "/some/path/to/your/file.bc"` declares the + bitcode file to analyze. If there are multiple bitcode files, + make a variable for each file. +- The line `mod = llvm_load_module(bcname)` creates the object to + pass to verification that represents the bitcode. +- The line `cryname = "/some/path/to/your/file.cry"` specifies the + path to a Cryptol specification. +- The line `cryptol_load_file(cryname)` loads a Cryptol specification. + +Now that the environment is set up, let's actually verify our +contract! This is done at the line + +|`rotl_result =` | `llvm_verify(` | `mod,` | `'rotl',` | `rotl_Contract()`| `)`| +|----------|-----------|----|------|---------------|----| +|Assign this variable| to the result of trying to verify| the bitcode| function with this name| using this contract|.| + +Now that we have the result, we want to assert this result succeeded +using `self.assertIs(rotl_result.is_success(), True)`. + +## Debugging C with SAW + +
+ Click here for the full code + +```python +import os +import unittest +from saw_client import * +from saw_client.crucible import * +from saw_client.llvm import * +from saw_client.proofscript import * +from saw_client.llvm_type import * + +class rotl_Contract(Contract): + def specification(self): + xs = self.fresh_var(i32, "xs") + shift = self.fresh_var(i32, "shift") + + self.execute_func(xs, shift) + + self.returns_f("rotl {xs} {shift}") + +class rotlTest(unittest.TestCase): + def test_rotl(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults(verbose_failure=True)) + + pwd = os.getcwd() + bcname = pwd + "/../src/rotl.bc" + cryname = pwd + "/spec/rotl.cry" + + cryptol_load_file(cryname) + mod = llvm_load_module(bcname) + + rotl_result = llvm_verify(mod, 'rotl', rotl_Contract()) + self.assertIs(rotl_result.is_success(), True) + +if __name__ == "__main__": + unittest.main() +``` + +Remember to always include + +```python +if __name__ == "__main__": + unittest.main() +``` + +or else the python script won't do anything! + +
+ +We can now run the proof script. + +```sh +$ cd labs/SAW/proof +$ python3 rotl.py +[03:08:29.986] Verifying rotl ... +[03:08:29.987] Simulating rotl ... +[03:08:29.988] Checking proof obligations rotl ... +[03:08:30.007] Subgoal failed: rotl safety assertion: +internal: error: in rotl +Undefined behavior encountered +Details: + Poison value created + The second operand of `shl` was equal to or greater than the number of bits in the first operand + +[03:08:30.007] SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 382} +[03:08:30.007] ----------Counterexample---------- +[03:08:30.007] shift0: 2147483648 +[03:08:30.007] ---------------------------------- + +F +====================================================================== +FAIL: test_rotl (__main__.rotlTest) +---------------------------------------------------------------------- +Traceback (most recent call last): + File "cryptol-course/labs/SAW/proof/rotl.py", line 31, in test_rotl + self.assertIs(rotl_result.is_success(), True) + AssertionError: False is not True + + ---------------------------------------------------------------------- + Ran 1 test in 0.750s + + FAILED (failures=1) + 🛑 The goal failed to verify. +``` + +SAW alerted us about potentially undefined behavior; the [C99 standard](https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf) +specifies the following about bit shifts: + +> If the value of the right operand is negative or is greater than or +> equal to the width of the promoted left operand, the behavior is +> undefined. + +As expected, this alerts us to a bug: + +``` + The second operand of `shl` was equal to or greater than the number of bits in the first operand + +[03:08:30.007] SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 382} +[03:08:30.007] ----------Counterexample---------- +[03:08:30.007] shift0: 2147483648 +[03:08:30.007] ---------------------------------- +``` + +SAW also provides a handy counterexample, namely, when `shift = +2147483648` (clearly larger than 31), we encounter undefined behavior. + +One remedy to this is the following: + +```C +uint32_t rotl(uint32_t bits, uint32_t shift) { + shift %= sizeof(bits) * 8; + return (bits << shift) | (bits >> (sizeof(bits) * 8 - shift)); +} +``` + +Recompiling and running SAW gives: + +```sh +$ clang ../src/rotl2.c -o ../src/rotl.bc -c -emit-llvm && python3 rotl.py +[03:11:54.334] Verifying rotl ... +[03:11:54.334] Simulating rotl ... +[03:11:54.335] Checking proof obligations rotl ... +[03:11:54.351] Subgoal failed: rotl safety assertion: +internal: error: in rotl +Undefined behavior encountered +Details: + Poison value created + The second operand of `shl` was equal to or greater than the number of bits in the first operand + +[03:11:54.351] SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 388} +[03:11:54.351] ----------Counterexample---------- +[03:11:54.351] shift0: 0 +[03:11:54.351] ---------------------------------- + +F +====================================================================== +FAIL: test_rotl (__main__.rotlTest) +---------------------------------------------------------------------- +Traceback (most recent call last): + File "cryptol-course/labs/SAW/proof/rotl.py", line 31, in test_rotl + self.assertIs(rotl_result.is_success(), True) + AssertionError: False is not True + + ---------------------------------------------------------------------- + Ran 1 test in 0.723s + + FAILED (failures=1) + 🛑 The goal failed to verify.~ +``` + +Aha! The counter example shows that we forgot about the case when +`shift = 0`! This causes `(sizeof(bits) * 8 - 0)` to be `32`, +which is equal to the word-size of `bits`, and hence causes `<<` to +exhibit undefined behavior. + +Let's try again with + +```C +uint32_t rotl(uint32_t bits, uint32_t shift) { + shift %= sizeof(bits)*8; + if(shift == 0) return bits; + return (bits << shift) | (bits >> (sizeof(bits) * 8 - shift)); +} +``` + +```sh +$ clang ../src/rotl3.c -o ../src/rotl.bc -c -emit-llvm && python3 rotl.py +[03:14:09.561] Verifying rotl ... +[03:14:09.562] Simulating rotl ... +[03:14:09.563] Checking proof obligations rotl ... +[03:14:09.614] Proof succeeded! rotl +✅ Verified: lemma_rotl_Contract (defined at cryptol-course/labs/SAW/proof/rotl.py:30) +. +---------------------------------------------------------------------- +Ran 1 test in 0.780s + +OK +✅ The goal was verified! +``` + +Finally, SAW is happy. More importantly, the C is correct and free of +undefined behavior. + +# Pointers and Arrays + +We'll begin by writing a function that given two arrays of a common +fixed size, say five, adds the second to the first. One way to +accomplish this is to pass in the two arrays, mutate the first and +return nothing: + +```C +void addRow5Mutate(uint32_t a[5], uint32_t b[5]) { + for(int i = 0 ; i < 5; i++) { + a[i] += b[i]; + } + return; +} +``` + +The corresponding Cryptol specification is: + +```cryptol +addRow5 : [5][32] -> [5][32] -> [5][32] +addRow5 a b = a + b +``` + +## Initializing Arrays and Pointers + +To initialize the arrays and pointers we'll use the `alloc` command +and `array_ty` type constructor: + +```python +def addRow5Mutate_Contract(Contract): + def specification(self): + a = self.fresh_var(array_ty(5, i32), "a") + a_p = self.alloc(array_ty(5, i32), points_to=a) + b = self.fresh_var(array_ty(5, i32), "b") + b_p = self.alloc(array_ty(5, i32), points_to=b, read_only=True) + + self.execute_func(a_p, b_p) + + self.points_to(a_p, cry_f("rowAdd {a} {b}")) + + self.returns(void) +``` + +- The `array_ty(type, length)` command creates a type representing an + array with entries of type `type` and length `length`. +- The `alloc` command will initialize a symbolic pointer. Let's break + down the initialization of `b_p`: + +| `b_p` | `self.alloc(` | `array_ty(5, i32)`|`,`|`points_to=b`|`,`|`read_only=True`|`)`| +|-------|---------------|-------------------|---|-------------|---|----------------|---| +| Assign this variable to | a symbolic pointer in the current contract | that has the following type | and | points to this object | with | read only permissions| . | + +Since arrays are passed as pointers in C, when we call `execute_func` +we supply `a_p` and `b_p` rather than `a` and `b`. + +To verify correctness, we assert after execution `a_p` +points to what the Cryptol specification claims it should: + +| `self.points_to(` | `a_p,` | `cry_f( "rowAdd {a} {b}"` | `))` | +|-------------------|--------|---------------------------|------| +| Assert in the current contract that the pointer | with this name | points to this Cryptol term | . | + +Finally, `specification` must contain `self.returns` or `self.returns_f`, so we use `self.returns(void)`. + +### Python Helper Functions + +To limit code reuse we can define helper functions in Python. Code *reuse* +is good. Code *repetition* is bad! For example, the following construct +is often used: + +```python +def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None, read_only : Optional[bool] = False) -> Tuple[FreshVar, SetupVal]: + var = c.fresh_var(ty, name) + ptr = c.alloc(ty, points_to = var, read_only=read_only) + return (var, ptr) +``` + +Given a contract and a type this function outputs a tuple `(var, ptr)` +where `var` is a fresh symbolic variable of the given type and `ptr` +is a pointer pointing to this variable. We give optional arguments to +name the fresh symbolic variable and to assert read-only pointer +constraints. + +To see this in action, let's rewrite our previous contract: + +```python +def addRow5Mutate_Contract(Contract): + def specification(self): + (a, a_p) = ptr_to_fresh(self, array_ty(5, i32), name="a") + (b, b_p) = ptr_to_fresh(self, array_ty(5, i32), name="b", read_only=True) + + self.execute_func(a_p, b_p) + + self.points_to(a_p, cry_f("rowAdd {a} {b}")) + + self.returns(void) +``` + +## Auxiliary Variables + +In this section we discuss an alternative way add two rows by using an auxillary variable. For example, consider the function + +```C +uint32_t* addRow5NewVar(uint32_t a[5], uint32_t b[5]) { + uint32_t* c = (uint32_t*) malloc(5*sizeof(uint32_t)); + for(int i = 0 ; i < 5; i++) { + c[i] = a[i] + b[i]; + } + return c; +} +``` + +Recall that a SAW contract is strictly divided into three parts: +1. Preconditions +2. Execution +3. Postconditions + +SAW complains if you place a precondition after `execute_func` and +similarly for postcondition. If a function returns a value that was +not passed through `execute_func`, then you will have to initialize +new fresh symbolic variables. For example, consider the proposed +contract for `addRow5NewVar`: + +```python +def addRow5NewVar_Contract(Contract): + def specification(self): + (a, a_p) = ptr_to_fresh(self, array_ty(5, i32), name="a") + (b, b_p) = ptr_to_fresh(self, array_ty(5, i32), name="b", read_only=True) + (c, c_p) = ptr_to_fresh(self, array_ty(5, i32), name="c") + + self.execute_func(a_p, b_p) + + self.points_to(c_p, cry_f("rowAdd {a} {b}")) + + self.returns(c_p) +``` + +Running a unit test yields the following error message: + +```sh +[16:42:51.066] Subgoal failed: addRow5NewVar safety assertion: +internal: error: in _SAW_verify_prestate SAWServer +The following pointers had to alias, but they didn't: + (12, 0x0:[64]) + (7, 0x0:[64]) + + +[16:42:51.067] SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 29} +[16:42:51.067] ----------Counterexample---------- +[16:42:51.067] <> +[16:42:51.067] ---------------------------------- +``` + +Think about the precondition block, the part before `execute_func`, as +setting up the symbolic variables **before** they enter the +function. With this in mind, it doesn't make sense to declare `c_p` in +this block because `c_p` is defined **within** the C function. The fix +to the previous contract is moving the declaration of `c_p` to the +postcondition block: + +```python +def addRow5NewVar_Contract(Contract): + def specification(self): + (a, a_p) = ptr_to_fresh(self, array_ty(5, i32), name="a") + (b, b_p) = ptr_to_fresh(self, array_ty(5, i32), name="b", read_only=True) + + self.execute_func(a_p, b_p) + + (c, c_p) = ptr_to_fresh(self, array_ty(5, i32), name="c") + self.points_to(c_p, cry_f("rowAdd {a} {b}")) + + self.returns(c_p) +``` + +Python supports wildcards, denoted by `_`, like Cryptol. Wildcards are placeholders for values we don't use. For example, we could rewrite the `addRow5NewVar_Contract` as follows: + +```python +def addRow5NewVar_Contract(Contract): + def specification(self): + (a, a_p) = ptr_to_fresh(self, array_ty(5, i32), name="a") + (b, b_p) = ptr_to_fresh(self, array_ty(5, i32), name="b", read_only=True) + + self.execute_func(a_p, b_p) + + (_, c_p) = ptr_to_fresh(self, array_ty(5, i32), name="c") + self.points_to(c_p, cry_f("rowAdd {a} {b}")) + + self.returns(c_p) +``` + +### Postconditions and `points_to` + +One could replace the `points_to` line with a `postcondition_f` line to get an equivalent contract: + +```python +def addRow5NewVar_Contract(Contract): + def specification(self): + (a, a_p) = ptr_to_fresh(self, array_ty(5, i32), name="a", read_only=True) + (b, b_p) = ptr_to_fresh(self, array_ty(5, i32), name="b", read_only=True) + + self.execute_func(a_p, b_p) + + (c, c_p) = ptr_to_fresh(self, array_ty(5, i32), name="c") + self.postcondition_f("{c} == rowAdd {a} {b}") + + self.returns(c_p) +``` + +While Cryptol has arrays, it doesn't have a notion of pointer, so we can't pass a symbolic pointer into `cry_f`. For example, if we wanted to assert `a_p` points to `b_p` then we can use `self.points_to(a_p, b_p)` but **NOT** `self.postcondition_f("{a_p} == {b_p}")`. + +## Parameterized Contracts + +Now let's consider a third possible way to write the same function. Here we are given two arrays of arbitrary size and a length. + +```C +uint32_t* addRowAlias(uint32_t* a, uint32_t* b, uint8_t length) { + for(int i = 0 ; i < length; i++) { + a[i] += b[i]; + } + return a; +} +``` + +A corresponding Cryptol specification might is + +```cryptol +addRow : {length} (fin length) => [length][32] -> [length][32] -> [length][32] +addRow a b = a + b +``` + +SAW currently does not have inductive reasoning capabilities and so +can only reason about concrete types. However, SAWCore terms can be +[formalized in Coq](https://github.com/GaloisInc/saw-script/tree/master/saw-core-coq), +a much more powerful theorem prover that has inductive reasoning (and +many more) capabilities. This is obviously well beyond the scope of +the course, but worth mentioning. + +We could make a new contract for each value of `length` used in the C code. Instead we make a single contract with a `length` +parameter: + +```python +def addRowAlias_Contract(Contract): + def __init__(self, length : int): + super().__init__() + self.length = length + + def specification(self): + (a, a_p) = ptr_to_fresh(self, array_ty(self.length, i32), name="a") + (b, b_p) = ptr_to_fresh(self, array_ty(self.length, i32), name="b", read_only=True) + length = fresh_var(i8, "length") + + self.execute_func(a_p, b_p, length) + + self.points_to(a_p, cry_f("rowAdd`{{{self.length}}} {a} {b}")) + + self.returns(a_p) +``` + +However, we still need to make a test for each length encountered: + +```python +class ArrayTests(unittest.TestCase): + def test_rowAdds(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults(verbose_failure=True)) + + bcname = "/some/path/to/your/file.bc" + cryname = "/some/path/to/your/file.cry" + + cryptol_load_file(cryname) + mod = llvm_load_module(bcname) + + arrayAddNewVar05_result = llvm_verify(mod, 'addRowAlias', addRowAlias_Contract(5)) + arrayAddNewVar10_result = llvm_verify(mod, 'addRowAlias', addRowAlias_Contract(10)) + self.assertIs(addRowAlias05_result.is_success(), True) + self.assertIs(addRowAlias10_result.is_success(), True) +``` + +## Full Code Example and Debugging SAW + +```python +import unittest +from saw_client import * +from saw_client.crucible import * +from saw_client.llvm import * +from saw_client.proofscript import * +from saw_client.llvm_type import * + +def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None, read_only : Optional[bool] = False) -> Tuple[FreshVar, SetupVal]: + var = c.fresh_var(ty, name) + ptr = c.alloc(ty, points_to = var, read_only=read_only) + return (var, ptr) + +def addRow5Mutate_Contract(Contract): + def specification(self): + (a, a_p) = ptr_to_fresh(self, array_ty(5, i32), name="a") + (b, b_p) = ptr_to_fresh(self, array_ty(5, i32), name="b", read_only=True) + + self.execute_func(a_p, b_p) + + self.points_to(a_p, cry_f("rowAdd {a} {b}")) + + self.returns(void) + +def addRow5NewVar_Contract(Contract): + def specification(self): + (a, a_p) = ptr_to_fresh(self, array_ty(5, i32), name="a") + (b, b_p) = ptr_to_fresh(self, array_ty(5, i32), name="b", read_only=True) + + self.execute_func(a_p, b_p) + + (c, c_p) = ptr_to_fresh(self, array_ty(5, i32), name="c") + self.points_to(c_p, cry_f("rowAdd {a} {b}")) + + self.returns(c_p) + +def addRowAlias_Contract(Contract): + def __init__(self, length : int): + super().__init__() + self.length = length + + def specification(self): + (a, a_p) = ptr_to_fresh(self, array_ty(self.length, i32), name="a") + (b, b_p) = ptr_to_fresh(self, array_ty(self.length, i32), name="b", read_only=True) + length = fresh_var(i8, "length") + + self.execute_func(a_p, b_p, length) + + self.points_to(a_p, cry_f("rowAdd`{{{length}}} {a} {b}")) + + self.returns(a_p) + +class ArrayTests(unittest.TestCase): + def test_rowAdds(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults(verbose_failure=True)) + + bcname = "../src/addRow.bc" + cryname = "spec/addRow.cry" + + cryptol_load_file(cryname) + mod = llvm_load_module(bcname) + + addRow5Mutate_result = llvm_verify(mod, 'addRowMutate', addRowMutate_Contract()) + self.assertIs(addRow5Mutate_result.is_success(), True) + + addRow5NewVar_result = llvm_verify(mod, 'addRowNewVar', addRowNewVar_Contract()) + self.assertIs(addRow5NewVar_result.is_success(), True) + + addRowAlias05_result = llvm_verify(mod, 'addRowAlias', addRowAlias_Contract(5)) + addAddAlias10_result = llvm_verify(mod, 'addRowAlias', addRowAlias_Contract(10)) + self.assertIs(addRowAlias05_result.is_success(), True) + self.assertIs(addRowAlias10_result.is_success(), True) +``` + +What do you think will happen if we run this code? + +
+ Click here to find out! + Running the code, SAW verifies the first two contracts + + ```sh + $ clang ../src/addRow.c -o ../src/addRow.bc -c -emit-llvm && python3 addRow.py + [15:40:51.330] Verifying addRow5Mutate ... + [15:40:51.330] Simulating addRow5Mutate ... + [15:40:51.335] Checking proof obligations addRow5Mutate ... + [15:40:51.362] Proof succeeded! addRow5Mutate + ✅ Verified: lemma_addRow5Mutate_Contract (defined at /home/cryptol/cryptol-course/labs/SAW/proof/addRow.py:64) + [15:40:51.430] Verifying addRow5NewVar ... + [15:40:51.430] Simulating addRow5NewVar ... + [15:40:51.435] Checking proof obligations addRow5NewVar ... + [15:40:51.462] Proof succeeded! addRow5NewVar + ✅ Verified: lemma_addRow5NewVar_Contract (defined at /home/cryptol/cryptol-course/labs/SAW/proof/addRow.py:67) + ``` + + ...but fails to verify the third contract. It alerts us there is a memory error + + ```sh + [15:40:51.527] Verifying addRowAlias ... + [15:40:51.528] Simulating addRowAlias ... + [15:40:51.532] Symbolic simulation completed with side conditions. + [15:40:51.535] Checking proof obligations addRowAlias ... + [15:40:51.575] Subgoal failed: addRowAlias safety assertion: + internal: error: in addRowAlias + Error during memory load + ``` + + and even produces the following counterexample: + + ```sh + [15:40:51.575] SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 331} + [15:40:51.575] ----------Counterexample---------- + [15:40:51.575] length0: 6 + [15:40:51.575] : False + [15:40:51.575] ---------------------------------- + ⚠️ Failed to verify: lemma_addRowAlias_Contract (defined at /home/cryptol/cryptol-course/labs/SAW/proof/addRow.py:37): + error: Proof failed. + stdout: + [15:40:51.527] Verifying addRowAlias ... + [15:40:51.528] Simulating addRowAlias ... + [15:40:51.532] Symbolic simulation completed with side conditions. + [15:40:51.535] Checking proof obligations addRowAlias ... + [15:40:51.575] Subgoal failed: addRowAlias safety assertion: + internal: error: in addRowAlias + Error during memory load + + [15:40:51.575] SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 331} + [15:40:51.575] ----------Counterexample---------- + [15:40:51.575] length0: 6 + [15:40:51.575] : False + [15:40:51.575] ---------------------------------- + F + ====================================================================== + FAIL: test_rowAdds (__main__.ArrayTests) + ---------------------------------------------------------------------- + Traceback (most recent call last): + File "/home/cryptol/cryptol-course/labs/SAW/proof/addRow.py", line 71, in test_rowAdds + self.assertIs(addRowAlias05_result.is_success(), True) + AssertionError: False is not True + + ---------------------------------------------------------------------- + Ran 1 test in 1.735s + + FAILED (failures=1) + 🛑 1 out of 3 goals failed to verify. + ``` + + SAW is telling us we forgot to add a precondition to assert our symbolic `length` agrees with our Python parameter `self.length`. This is an easy fix: + + ```sh + def addRowAlias_Contract(Contract): + def __init__(self, length : int): + super().__init__() + self.length = length + + def specification(self): + (a, a_p) = ptr_to_fresh(self, array_ty(self.length, i32), name="a") + (b, b_p) = ptr_to_fresh(self, array_ty(self.length, i32), name="b", read_only=True) + + self.execute_func(a_p, b_p, cry(self.length)) + + self.points_to(a_p, cry_f("rowAdd`{{{self.length}}} {a} {b}")) + + self.returns(a_p) + ``` + +And now SAW happily verifies the third contract! + + ```sh + $ python3 addRow.py + ✅ Verified: lemma_addRow5Mutate_Contract (defined at /home/cryptol/cryptol-course/labs/SAW/proof/addRow.py:64) + ✅ Verified: lemma_addRow5NewVar_Contract (defined at /home/cryptol/cryptol-course/labs/SAW/proof/addRow.py:67) + ✅ Verified: lemma_addRowAlias_Contract (defined at /home/cryptol/cryptol-course/labs/SAW/proof/addRow.py:37) + . + ---------------------------------------------------------------------- + Ran 1 test in 1.985s + + OK + ✅ All 3 goals verified! + ``` + +
+ +## Explicit Arrays + +Another way to initialize arrays is through the `array` command. For +example, suppose I have the following C function (taken from +[here](https://github.com/GaloisInc/saw-script/blob/337ca6c9edff3bcbcd6924289471abd5ee714c82/saw-remote-api/python/tests/saw/test-files/llvm_array_swap.c)): + +```C +#include + +void array_swap(uint32_t a[2]) { + uint32_t tmp = a[0]; + a[0] = a[1]; + a[1] = tmp; +} +``` + +Here's a contract that doesn't even require Cryptol (taken from +[here](https://github.com/GaloisInc/saw-script/blob/337ca6c9edff3bcbcd6924289471abd5ee714c82/saw-remote-api/python/tests/saw/test_llvm_array_swap.py)): + +```python +class ArraySwapContract(Contract): + def specification(self): + a0 = self.fresh_var(i32, "a0") + a1 = self.fresh_var(i32, "a1") + a = self.alloc(array_ty(2, i32), points_to=array(a0, a1)) + + self.execute_func(a) + + self.points_to(a[0], a1) + self.points_to(a[1], a0) + self.returns(void) +``` + +Explicit arrays can be useful when you want to assert a condition on a +particular element of the array. Of course, a drawback is you have to +initialize every member of the array. This can be problematic +for large arrays. Ideally, one would just have to declare the array +implicitly as before and then pass this array to a Cryptol +specification for postconditions as was done in the previous examples. + +## Null Pointers + +Consider the following C code to check if a pointer is null: + +```C +int f(int *x) { + return (x == (int*)0); +} +``` + +The following contract has possibly unexpected behavior (in C booleans are encoded as `0` for false and `1` for true). + +```python +import unittest +from saw_client import * +from saw_client.crucible import * +from saw_client.llvm import * + + +class FContract(Contract): + def specification(self): + p = self.alloc(i32) + + self.execute_func(p) + + self.returns(cry("1 : [32]")) + +class LLVMAssertNullTest(unittest.TestCase): + def test_llvm_assert_null(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults(verbose_failure=True)) + bcname = '../src/null.bc' + mod = llvm_load_module(bcname) + + result = llvm_verify(mod, 'f', FContract()) + self.assertIs(result.is_success(), True) + + +if __name__ == "__main__": + unittest.main() +``` + +
+ Click here to see if your guess is correct! + + It turns out the contract above will fail! + + ```sh + $ clang ../src/null.c -o ../src/null.bc -c -emit-llvm && python3 null.py + [17:21:44.701] Verifying isNull ... + [17:21:44.701] Simulating isNull ... + [17:21:44.703] Checking proof obligations isNull ... + [17:21:44.724] Subgoal failed: isNull safety assertion: + internal: error: in _SAW_verify_prestate SAWServer + Literal equality postcondition + [more error message] + FAILED (failures=1) + 🛑 The goal failed to verify. + ``` + + The counterexample produced may seem mystical. + ```sh + [17:21:44.725] ----------Counterexample---------- + [17:21:44.725] <> + [17:21:44.725] ---------------------------------- + ``` + + However, if **every** setting is a counterexample, then this is telling us the pointer must have been the null pointer! An initialized symbolic pointer that hasn't been assigned a symbolic variable to point to is **NOT** equivalent to a null pointer in SAW. We can use `null()` in situations where we want a null pointer. For example, if we change the contract above to + + ```python + class FContract(Contract): + def specification(self): + self.execute_func(null()) + + self.returns(cry("1 : [32]")) + ``` + + then SAW is a happy. + + ```sh + $ python3 null.py + [17:33:50.802] Verifying isNull ... + [17:33:50.802] Simulating isNull ... + [17:33:50.804] Checking proof obligations isNull ... + [17:33:50.804] Proof succeeded! isNull + ✅ Verified: lemma_isNull_Contract (defined at /home/cryptol/cryptol-course/labs/SAW/proof/null.py:22) + . + ---------------------------------------------------------------------- + Ran 1 test in 1.301s + + OK + ✅ The goal was verified! + ``` +
+ +This example is from the [GaloisInc/saw-script repo](https://github.com/GaloisInc/saw-script/blob/master/saw-remote-api/python/tests/saw/test_llvm_assert_null.py). + + +# Structs + +In this section we will learn how to verify code involving structs by analyzing a game. The code for the game can be found [here](./Game/src/). + +To complete this lab, navigate to the [Game directory](./Game). In there, you'll notice the following: +- `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. Your job will be to complete the `TODO` sections marked throughout [Game.cry](./Game/proof/Game.py). If you get stuck, you can refer to [Game_answers.cry](./Game/proof/Game_answers.py) or look at the discussions mentioned later in this markdown file! +- `specs/`: Contains our Cryptol specs that our SAW contracts can call. Feel free to add your own Cryptol functions to help you complete this lab! +- `DLC/`: Contains an extended version of this lab (think Downloadable Content) with even more Game functions for you to play with! While there aren't any lab worksheets configured for you in there, you can reference the contents for how to tackle additional functions. For more information regarding to what each function intends to teach, refer to [GameOutline.md](./Game/DLC/GameOutline.md). + +With that knowledge, make sure you have `start-saw-remote-api` running, open up Game.cry, fill out your answers, and test your work by running `make`. Game on! + + +## Struct Initialization + +The game defines the following player type. + +```C +typedef struct { + uint8_t name[MAX_NAME_LENGTH]; + uint32_t level; + uint32_t hp; + uint32_t atk; + uint32_t def; + uint32_t spd; +} character_t; + +typedef character_t player_t; +``` + +A player is initialized with some default values + +```C +uint32_t initDefaultPlayer(player_t* player) +{ + uint8_t i = 0; + uint32_t hp_default = 10; + uint32_t atk_default = 5; + uint32_t def_default = 4; + uint32_t spd_default = 3; + + for (i = 0; i < MAX_NAME_LENGTH; i++) + { + player->name[i] = 'A'; + } + player->level = 1; + player->hp = hp_default; + player->atk = atk_default; + player->def = def_default; + player->spd = spd_default; + + return SUCCESS; +} +``` + +where `SUCCESS` and `MAX_NAME_LENGTH` are C constants: + +```C +#define MAX_NAME_LENGTH 12 +#define SUCCESS 170 +#define FAILURE 85 +``` + +We use the following contract to verify this initialization function: + +```python +MAX_NAME_LENGTH = 12 +SUCCESS = 170 +FAILURE = 85 + +class initDefaultPlayer_Contract(Contract): + def specification (self): + player = self.alloc(alias_ty("struct.player_t")) + + self.execute_func(player) + + self.points_to(player['name'], cry_f("repeat 0x41 : [{MAX_NAME_LENGTH}][8]")) + self.points_to(player['level'], cry_f("1 : [32]")) + self.points_to(player['hp'], cry_f("10 : [32]")) + self.points_to(player['atk'], cry_f("5 : [32]")) + self.points_to(player['def'], cry_f("4 : [32]")) + self.points_to(player['spd'], cry_f("3 : [32]")) + + self.returns(cry_f("`({SUCCESS}) : [32]")) +``` + +For every C symbol defined using `#define` we make a corresponding Python global variable. + +```python +MAX_NAME_LENGTH = 12 +SUCCESS = 170 +FAILURE = 85 +``` + +The command `alias_ty("struct.")` creates a type corresponding to the structure, e.g., + +```python +player = self.alloc(alias_ty("struct.player_t")) +``` +creates a symbolic pointer variable `player` pointing to a structure of type `player_t`. + +Let's breakdown a `points_to` command seen above: + + +| `self.points_to(` | `player` | `['name']` | `,` | `cry_f("repeat 0x41 : [{MAX_NAME_LENGTH}][8]")` | `)` | +|-------------------|-----------|----------|------|-------------------------------------------------|-----| +| Assert in the current contract that the following pointer | with this name | points to a struct with this named field | and the value of that field is | this expression | . | + + +Above we use strings to reference fields of structures. However, we can only do this when strings are present in the bitcode, e.g., when debug symbols are included in the generated bitcode. The `-g` clang flag tells the compiler to include the field names of the structs in the bitcode. For the full compilation details, check out the [Makefile](./Game/Makefile) associated with the `Game` directory. + +If we didn't have the debug symbols in the bitcode, SAW would produce an error: + +```sh +$ cd labs/SAW/Game +$ mkdir artifacts +$ clang -c -emit-llvm -o artifacts/Game.bc src/Game.c +$ python3 proof/Game.py +⚠️ Failed to verify: lemma_initDefaultPlayer_Contract (defined at proof/Game.py:513): +error: Unable to resolve struct field name: '"name"' +Could not resolve setup value debug information into a struct type. +Perhaps you need to compile with debug symbols enabled. +``` + +If we didn't want to include debug symbols in the bitcode, then we can reference the struct fields by using their corresponding indices: + +```python +class initDefaultPlayer_Contract(Contract): + def specification (self): + player = self.alloc(alias_ty("struct.character_t")) + + self.execute_func(player) + + self.points_to(player[0], cry_f("repeat 0x41 : [{MAX_NAME_LENGTH}][8]")) + self.points_to(player[1], cry_f("1 : [32]")) + self.points_to(player[2], cry_f("10 : [32]")) + self.points_to(player[3], cry_f("5 : [32]")) + self.points_to(player[4], cry_f("4 : [32]")) + self.points_to(player[5], cry_f("3 : [32]")) + + self.returns(cry_f("`({SUCCESS}) : [32]")) +``` + + +### Structs as Cryptol Tuples and Records + +We can replace all of the `points_to` postconditions in the previous contract since Cryptol interprets symbolic structs as tuples. + +```python +self.points_to(player, cry_f("""( repeat 0x41 : [{MAX_NAME_LENGTH}][8], + 1 : [32], + 10 : [32], + 5 : [32], + 4 : [32], + 3 : [32] )""")) +``` + +We use 3 double quotes `"""` in our `cry_f` call. This technique is useful when we want to separate our expected Cryptol-defined behaviors over multiple lines to improve code readability. Python considers the 3 double quotes as a multiline string. Multiline strings may also be used as block comments in Python. + +Note that the setup we see above results in wide open spaces, which will be noticable when debugging strings passed to the family of `cry` functions. These spaces can be mitigated using `dedent` from the `textwrap` package that comes with Python. For example: + +```python +from textwrap import dedent +# ... + + self.returns(cry(dedent(""" + (y, z) + where + y = "foo" + z = "bar" + """).strip())) +``` + +This renders (without leading/trailing whitespace) as: + +```python +(y, z) + where + y = "foo" + z = "bar" +``` + +While Cryptol's record types could also represent structs, SAW does not currently support translating Cryptol's record types into crucible-llvm's type system. If we tried to represent the struct as a Cryptol record like so: + +```python +self.points_to(player, cry_f("""{{ name = repeat 0x41 : [{MAX_NAME_LENGTH}][8], + level = 1 : [32], + hp = 10 : [32], + atk = 5 : [32], + def = 4 : [32], + spd = 3 : [32] }}""")) +``` + +SAW would return this error: + +```sh +$ clang -c -g -emit-llvm -o artifacts/Game.bc src/Game.c +$ python3 proof/Game.py +⚠️ Failed to verify: lemma_initDefaultPlayer_Contract (defined at proof/Game.py:537): +error: SAW doesn't yet support translating Cryptol's record type(s) into crucible-llvm's type system. + stdout: + +F +====================================================================== +FAIL: test_Game (__main__.GameTests) +---------------------------------------------------------------------- +Traceback (most recent call last): + File "proof/Game.py", line 563, in test_Game + self.assertIs(initDefaultPlayer_result.is_success(), True) +AssertionError: False is not True + +---------------------------------------------------------------------- +Ran 1 test in 0.752s + +FAILED (failures=1) +🛑 The goal failed to verify. +make: *** [Makefile:14: all] Error 1 +``` + +If a Cryptol specification uses a record type to represent structs, then we can define a Python helper function for wrapping. + + +## Explicit Structs + +We can also explicitly define a struct in SAW. Let's consider another struct: + +```C +#define GAITS 2 +#define DIRECTIONS 4 +#define ANIMATION_STEPS 3 + +typedef struct { + character_t* character; + uint8_t frames[GAITS][DIRECTIONS][ANIMATION_STEPS]; + uint32_t xPos; + uint32_t yPos; +} sprite_t; +``` + +The idea behind the `sprite_t` struct is to hold all of the sprites associated with a character that we will present in our game. `character` is a pointer to a `character_t` type that the sprite is tied to. `frames` is a 3D uint8_t array where each element represents an asset identifier from our art collection. Why a 3D array? Well, we want to provide animations for our characters that way it looks like they are moving on the screen (and it's a great excuse to discuss multi-dimensional arrays in SAW). The first dimension refers to the number of gaits we want to represent, that being walking and running. The second dimension refers to the number of directions a character can face. Imagine that we are working with a 2D top down game, so we have 4 directions: up, down, left, and right. The third dimension refers to the number of frames per movement. + +Let's think about how we walk forward (feel free to try this at home). If you are walking forward, you first stand up, move one foot in front of the other, place that foot down, lift up your back foot, and move that back foot ahead of your front foot. Rinse and repeat, and you'll be walking 'cross the floor. + +Now that's a lot of steps! We can simplify this process by only considering 3 frames: standing up, left foot in front, and right foot in front. We can then reuse the standing up frame as a transition between the left foot forward and the right foot forward frames. + +Alright, that's enough of a crash course in animation. Let's get back to our struct. We have two more fields: xPos and yPos. These are simply positional references for where a character is located relative to the screen. + +With that understanding, let's consider a function that uses the `sprite_t` struct: + +```C +uint32_t initDefaultSprite(character_t* character, sprite_t* sprite) +{ + // Initialize the character to the passed pointer + sprite->character = character; + + // Initialize the sprite frames to the default asset + for (uint8_t i = 0; i < GAITS; i++) + { + for (uint8_t j = 0; j < DIRECTIONS; j++) + { + for (uint8_t k = 0; k < ANIMATION_STEPS; k++) + { + sprite->frames[i][j][k] = 0x00; + } + } + } + + // Initialize sprite's default position + sprite->xPos = 1; + sprite->yPos = 2; + + return SUCCESS; +} +``` + +Now, let's go ahead and make a contract to represent this function: + +```python +class initDefaultSprite_Contract(Contract): + def specification (self): + # Declare variables + character = self.alloc(alias_ty("struct.character_t")) + tempCharacter_p = self.alloc(alias_ty("struct.character_t")) + frames = self.fresh_var(array_ty(GAITS, array_ty(DIRECTIONS, array_ty(ANIMATION_STEPS, i8))), "sprite.frames") + xPos = self.fresh_var(i32, "sprite.xPos") + yPos = self.fresh_var(i32, "sprite.yPos") + sprite = struct(tempCharacter_p, frames, xPos, yPos) + sprite_p = self.alloc(alias_ty("struct.sprite_t")) + self.points_to(sprite_p, sprite) + + # Symbolically execute the function + self.execute_func(character, sprite_p) + + # Assert postconditions + self.points_to(sprite_p, struct( character, + cry_f("zero : [{GAITS}][{DIRECTIONS}][{ANIMATION_STEPS}][8]"), + cry_f("1 : [32]"), + cry_f("2 : [32]") )) + + self.returns_f("`({SUCCESS}) : [32]") +``` + +Like `array`, the `struct` keyword declares a symbolic struct given a variable for each struct field. We assert the precondition that our pointer points to this symbolic struct. Alternatively, we could replace + +```python + sprite = struct(tempCharacter_p, frames, xPos, yPos) + sprite_p = self.alloc(alias_ty("struct.sprite_t")) + self.points_to(sprite_p, sprite) +``` + with +```python +sprite_p = self.alloc(alias_ty("struct.sprite_t"), points_to = struct(tempCharacter_p, frames, xPos, yPos)) +``` +since we don't use `sprite` later in the code. If we wanted, we could assert other preconditions on `tempCharacter_p`, `frames`, `xPos`, and `yPos``. We don't in this example, but it's still a feature to consider! + +In the postcondition, we assert `sprite_p` points to some concrete structure. The benefit of using explicit structs is that it allows us to represent pointer fields that may be present in a struct. + +However, explicit structs isn't the only way to represent pointer fields. We could also use a tuple to assert our postcondition. However, we will need to change our definition for `character`. + +```python +class initDefaultSprite_Contract(Contract): + def specification (self): + # Declare variables + character = self.fresh_var(ptr_ty(alias_ty("struct.character_t"))) + tempCharacter_p = self.alloc(alias_ty("struct.character_t")) + ty = array_ty(GAITS, array_ty(DIRECTIONS, array_ty(ANIMATION_STEPS, i8))) + frames = self.fresh_var(ty, "sprite.frames") + xPos = self.fresh_var(i32, "sprite.xPos") + yPos = self.fresh_var(i32, "sprite.yPos") + sprite_p = self.alloc(alias_ty("struct.sprite_t"), points_to = struct(tempCharacter_p, frames, xPos, yPos)) + + # Symbolically execute the function + self.execute_func(character, sprite_p) + + # Assert postconditions + self.points_to(sprite_p, cry_f("""( {character}, + zero : [{GAITS}][{DIRECTIONS}][{ANIMATION_STEPS}][8], + 1 : [32], + 2 : [32]) """)) + + self.returns_f("`({SUCCESS}) : [32]") +``` + + +## Exercise: Resolving an Attack! + +Feeling pretty confident with our little `player_t` and `character_t` structs? How about we go for a full on attack then? Well, in our game of course ;) + +Consider the following function: + +```C +void resolveAttack(character_t* target, uint32_t atk) +{ + if ( target->def >= atk) + { + // The target's defense mitigates the attack + target->hp = target->hp; + } + else if ( target->hp <= (atk - target->def) ) + { + // The attack will knock out the target + target->hp = 0; + } + else + { + // Calculate damage as normal + target->hp = target->hp - (atk - target->def); + } +} +``` + +Our function, `resolveAttack`, takes two inputs: +- `character_t* target`: Our defending character +- `uint32_t atk`: The attack stat of our attacker + +Think about how to make a SAW contract for this function. Go ahead and try it if you'd like! We'll wait for you :) + +Got an idea, great! Let's go over the steps we need to go through... + +First, let's set up our basic format for the contract: + +```python +class resolveAttack_Contract(Contract): + def specification (self): + # Declare variables + (target, target_p) = ptr_to_fresh(self, alias_ty("struct.character_t"), name="target") + atk = self.fresh_var(i32, "atk") + + # Assert preconditions + + # Symbolically execute the function + self.execute_func(target_p, atk) + + # Assert postconditions + + self.returns(void) +``` + +Alright, we got our basic setup! But wait a second, there are 3 possible assignments for the target's hp... Each of these behaviors are determined by the stat ranges for the defender and attacker. How are we going to represent these different behaviors? + +First, let's consider the 3 possible cases for `resolveAttack`: +- Case 1: Attack mitigated + - Precondition: `target->def >= atk` + - Postcondition: `target->hp = target->hp` +- Case 2: Immediate KO + - Precondition: `target->hp <= (atk - target-> def)` + - Postcondition: `target->hp = 0` +- Case 3: Regular attack calculation + - Precondition: Anything other than Cases 1 and 2 + - Postcondition: `target->hp = target->hp - (atk - target->def)` + +With those 3 cases laid out, we now have a battle plan to represent the preconditions and postconditions needed for our proof. Now one option to account for all of these cases is to create 3 different contracts where each one specifies the appropriate precondition and postcondition pair for our case. Do we really want to copy and paste the bulk of our proof across 3 contracts though? Probably not. How about we bring our knowledge of parameterized contracts to battle! Tactics! + +```python +class resolveAttack_Contract(Contract): + def __init__(self, case : int): + super().__init__() + self.case = case + # There are 3 possible cases for resolveAttack + # Case 1: Attack mitigated + # Case 2: Immediate KO + # Case 3: Regular attack + + def specification (self): + # Declare variables + (target, target_p) = ptr_to_fresh(self, alias_ty("struct.character_t"), name="target") + atk = self.fresh_var(i32, "atk") + + # Assert preconditions + # Determine the preconditions based on the case parameter + if (self.case == 1): + # target->def >= atk + self.precondition_f("{target}.4 >= {atk}") + elif (self.case == 2): + # target->hp <= (atk - target->def) + self.precondition_f("({target}.2 + {target}.4) <= {atk}") + else: + # Assume any other case follows the formal attack calculation + self.precondition_f("{target}.4 < {atk}") + self.precondition_f("({target}.2 + {target}.4) > {atk}") + + # Symbolically execute the function + self.execute_func(target_p, atk) + + # Assert postconditions + # Determine the postcondition based on the case parameter + if (self.case == 1): + self.points_to(target_p['hp'], cry_f("{target}.2 : [32]")) + elif (self.case == 2): + self.points_to(target_p['hp'], cry_f("0 : [32]")) + else: + self.points_to(target_p['hp'], cry_f("resolveAttack ({target}.2) ({target}.4) {atk}")) + + self.returns(void) +``` + +Our contract is looking pretty good now! Notice that we use `{target}.2` and `{target}.4`for our postconditions. This notation lets us access fields within our target type. Specifically, `{target}.2` refers to the `hp` field, and `{target}.4` refers to the `def` field. + +It should be noted that using these cases in a parameterized contract is not the only way to set up our contract. We could have designed some fancy Cryptol that considers all of the different stat ranges for our preconditions and postconditions. However, we wanted to show this method of using cases since we can leverage Python's if statements in our proofs. + +Let's set up our unit test: + +```python +class GameTests(unittest.TestCase): + def test_Game(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults(verbose_failure=True)) + + pwd = os.getcwd() + bitcode_name = pwd + "/artifacts/Game.bc" + cryptol_name = pwd + "/specs/Game.cry" + + cryptol_load_file(cryptol_name) + module = llvm_load_module(bitcode_name) + + resolveAttack_case1_result = llvm_verify(module, 'resolveAttack', resolveAttack_Contract(1)) + resolveAttack_case2_result = llvm_verify(module, 'resolveAttack', resolveAttack_Contract(2)) + resolveAttack_case3_result = llvm_verify(module, 'resolveAttack', resolveAttack_Contract(3)) + + self.assertIs(resolveAttack_case1_result.is_success(), True) + self.assertIs(resolveAttack_case2_result.is_success(), True) + self.assertIs(resolveAttack_case3_result.is_success(), True) + + +if __name__ == "__main__": + unittest.main() +``` + +Excellent, now for the moment of truth! + +```sh +$ clang -c -emit-llvm -o artifacts/Game.bc src/Game.c +$ python3 proof/Game.py +[01:59:53.576] Verifying resolveAttack ... +[01:59:53.577] Simulating resolveAttack ... +[01:59:53.580] Checking proof obligations resolveAttack ... +[01:59:53.594] Proof succeeded! resolveAttack +✅ Verified: lemma_resolveAttack_Contract (defined at proof/Game.py:179) +[01:59:53.658] Verifying resolveAttack ... +[01:59:53.659] Simulating resolveAttack ... +[01:59:53.662] Checking proof obligations resolveAttack ... +[01:59:53.689] Subgoal failed: resolveAttack safety assertion: +internal: error: in llvm_points_to SAWServer +Literal equality postcondition + + +[01:59:53.689] SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 438} +[01:59:53.689] ----------Counterexample---------- +[01:59:53.689] target0: ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0, 4294967293, 0, 3, 0) +[01:59:53.689] atk0: 4294967295 +[01:59:53.689] ---------------------------------- +⚠️ Failed to verify: lemma_resolveAttack_Contract0 (defined at proof/Game.py:179): +error: Proof failed. + stdout: + [01:59:53.658] Verifying resolveAttack ... + [01:59:53.659] Simulating resolveAttack ... + [01:59:53.662] Checking proof obligations resolveAttack ... + [01:59:53.689] Subgoal failed: resolveAttack safety assertion: + internal: error: in llvm_points_to SAWServer + Literal equality postcondition + + + [01:59:53.689] SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 438} + [01:59:53.689] ----------Counterexample---------- + [01:59:53.689] target0: ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0, 4294967293, 0, 3, 0) + [01:59:53.689] atk0: 4294967295 + [01:59:53.689] ---------------------------------- + +[01:59:53.789] Verifying resolveAttack ... +[01:59:53.789] Simulating resolveAttack ... +[01:59:53.792] Checking proof obligations resolveAttack ... +[01:59:53.905] Proof succeeded! resolveAttack +✅ Verified: lemma_resolveAttack_Contract1 (defined at proof/Game.py:179) +F +====================================================================== +FAIL: test_Game (__main__.GameTests) +---------------------------------------------------------------------- +Traceback (most recent call last): + File "proof/Game.py", line 549, in test_Game + self.assertIs(resolveAttack_case2_result.is_success(), True) +AssertionError: False is not True + +---------------------------------------------------------------------- +Ran 1 test in 1.132s + +FAILED (failures=1) +🛑 1 out of 3 goals failed to verify. +make: *** [Makefile:14: all] Error 1 +``` + +A counterexample?! Let's take a closer look at what SAW provides us and reassess our strategy. + +```sh +[01:59:53.689] ----------Counterexample---------- +[01:59:53.689] target0: ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0, 4294967293, 0, 3, 0) +[01:59:53.689] atk0: 4294967295 +[01:59:53.689] ---------------------------------- +``` + +Notice that our unit case failed for case 2, but passed for cases 1 and 3. How about we look at our precondition for case 2 again: + +```python + elif (self.case == 2): + # target->hp <= (atk - target->def) + self.precondition_f("({target}.2 + {target}.4) <= {atk}") +``` + +and if we plug in the counterexample values SAW provides us... + +```sh +{target}.2 + {target}.4 <= {atk} +4294967293 + 3 <= 4294967295 + 4294967296 <= 4294967295 +``` + +Well that doesn't make sense, now does it? Well actually, it does make some sense when we recognize one BIG detail. And yes, I'm referring to the big values SAW gave us. Doesn't the atk stat look familiar? Like the upper bound for unsigned 32-bit integers? + +Taking that into consideration, then our efforts to test out the counterexample was incorrect. We forgot to account for integer overflow! + +```sh +4294967293 + 3 <= 4294967295 +4294967295 + 1 <= 4294967295 + 0 <= 4294967295 +``` + +*Audible gasp* Good thing we have SAW on our side! Now, let's determine what we can do to fix this issue. First, let's compare our precondition again to the source code's if condition: + +```python +self.precondition_f("({target}.2 + {target}.4) <= {atk}") +``` + +```C +else if ( target->hp <= (atk - target->def) ) +``` + +So maybe we tried being *too* fancy showing off our associative property knowledge. While moving the defense term to the left-hand side of the expression does not violate any mathematical rules on paper, it does violate our expectations in practice when accounting for limited bit widths. + +Fine, let's toss out our fancy math skills and write our contact's precondition for case 2 exactly as we see it in the source code: + +```python + elif (self.case == 2): + # target->hp <= (atk - target->def) + self.precondition_f("{target}.2 <= ({atk} - {target}.4)") +``` + +```sh +$ clang -c -emit-llvm -o artifacts/Game.bc src/Game.c +$ python3 proof/Game.py +[02:34:39.387] Verifying resolveAttack ... +[02:34:39.388] Simulating resolveAttack ... +[02:34:39.391] Checking proof obligations resolveAttack ... +[02:34:39.409] Proof succeeded! resolveAttack +✅ Verified: lemma_resolveAttack_Contract (defined at proof/Game.py:179) +[02:34:39.481] Verifying resolveAttack ... +[02:34:39.481] Simulating resolveAttack ... +[02:34:39.483] Checking proof obligations resolveAttack ... +[02:34:39.508] Subgoal failed: resolveAttack safety assertion: +internal: error: in llvm_points_to SAWServer +Literal equality postcondition + + +[02:34:39.508] SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 438} +[02:34:39.509] ----------Counterexample---------- +[02:34:39.509] target0: ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0, 134217728, 0, 4184634256, 0) +[02:34:39.509] atk0: 23884688 +[02:34:39.509] ---------------------------------- +⚠️ Failed to verify: lemma_resolveAttack_Contract0 (defined at proof/Game.py:179): +error: Proof failed. + stdout: + [02:34:39.481] Verifying resolveAttack ... + [02:34:39.481] Simulating resolveAttack ... + [02:34:39.483] Checking proof obligations resolveAttack ... + [02:34:39.508] Subgoal failed: resolveAttack safety assertion: + internal: error: in llvm_points_to SAWServer + Literal equality postcondition + + + [02:34:39.508] SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 438} + [02:34:39.509] ----------Counterexample---------- + [02:34:39.509] target0: ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0, 134217728, 0, 4184634256, 0) + [02:34:39.509] atk0: 23884688 + [02:34:39.509] ---------------------------------- + +[02:34:39.613] Verifying resolveAttack ... +[02:34:39.613] Simulating resolveAttack ... +[02:34:39.616] Checking proof obligations resolveAttack ... +[02:34:39.735] Proof succeeded! resolveAttack +✅ Verified: lemma_resolveAttack_Contract1 (defined at proof/Game.py:179) +F +====================================================================== +FAIL: test_Game (__main__.GameTests) +---------------------------------------------------------------------- +Traceback (most recent call last): + File "proof/Game.py", line 550, in test_Game + self.assertIs(resolveAttack_case2_result.is_success(), True) +AssertionError: False is not True + +---------------------------------------------------------------------- +Ran 1 test in 1.200s + +FAILED (failures=1) +🛑 1 out of 3 goals failed to verify. +make: *** [Makefile:14: all] Error 1 +``` + +Nope, that didn't work either. But hey, SAW gave us a different counterexample. Let's look at that one: + +```sh +[02:34:39.509] ----------Counterexample---------- +[02:34:39.509] target0: ([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 0, 134217728, 0, 4184634256, 0) +[02:34:39.509] atk0: 23884688 +[02:34:39.509] ---------------------------------- +``` + +Plugging those values into our updated case 2 precondition: + +```sh +{target}.2 <= ({atk} - {target}.4) + 134217728 <= 23884688 - 4184634256 + 134217728 <= 134217728 +``` + +Nice, we got an integer underflow counterexample. Based on these input values, the source code would actually meet the first if condition: + +```C +target->def >= atk +``` + +This means our precondition for case 2 is lacking something. Let's adjust it in this way: + +```python + elif (self.case == 2): + # target->hp <= (atk - target->def) + self.precondition_f("{target}.4 < {atk}") + self.precondition_f("{target}.2 <= ({atk} - {target}.4)") +``` + +```sh +$ clang -c -emit-llvm -o artifacts/Game.bc src/Game.c +$ python3 proof/Game.py +[02:55:30.437] Verifying resolveAttack ... +[02:55:30.437] Simulating resolveAttack ... +[02:55:30.440] Checking proof obligations resolveAttack ... +[02:55:30.455] Proof succeeded! resolveAttack +✅ Verified: lemma_resolveAttack_Contract (defined at proof/Game.py:179) +[02:55:30.551] Verifying resolveAttack ... +[02:55:30.551] Simulating resolveAttack ... +[02:55:30.554] Checking proof obligations resolveAttack ... +[02:55:30.570] Proof succeeded! resolveAttack +✅ Verified: lemma_resolveAttack_Contract0 (defined at proof/Game.py:179) +[02:55:30.672] Verifying resolveAttack ... +[02:55:30.673] Simulating resolveAttack ... +[02:55:30.675] Checking proof obligations resolveAttack ... +[02:55:30.789] Proof succeeded! resolveAttack +✅ Verified: lemma_resolveAttack_Contract1 (defined at proof/Game.py:179) +. +---------------------------------------------------------------------- +Ran 1 test in 1.140s + +OK +✅ All 3 goals verified! +``` + +Whoo hoo! We finally won the battle! From our exercise, we found that SAW provides us with some pretty useful counterexamples to consider for edge cases that may be lacking in traditional software unit testing. + +Now let's imagine that very large character stats is a concern in our game. In order to balance characters in our game and avoid problems with very large values, let's say we decided to add a function (`checkStats`) that checks character stats. Let's also assume that this function is always called before functions that use those stats like what we saw in `resolveAttack`. + +```C +uint32_t checkStats(character_t* character) +{ + // Assume failure by default + uint32_t result = FAILURE; + + // Check the stats + if (character->hp <= MAX_STAT && + character->atk <= MAX_STAT && + character->def <= MAX_STAT && + character->spd <= MAX_STAT ) + { + result = SUCCESS; + } + + return result; +} +``` + +Is this a good idea security-wise? Eh, maybe not. The assumption that `checkStats` is ALWAYS called before functions that use character stats may be missed. So what can we do? Using `resolveAttack` as an example, should we rely on its caller to also call `checkStats` and perform error handling ahead of time? An argument could be made for performance benefits, but at the cost of security. Should we call `checkStats` within `resolveAttack`? That strategy would provide more security, but the repeated `checkStats` may be redundant and could hurt performance depending on the use case. As we can see, the answer for `checkStats`'s best placement follows the classic "it depends". + +For the sake of argument, let's go with the assumption that `checkStats` is always called BEFORE the call to `resolveAttack`. While the stat checks aren't performed in `resolveAttack`, we could include them as preconditions in our contract. Let's add the stat checks to our original `resolveAttack_Contract`, problems with case 2's preconditons and all! + +```python +class resolveAttack_Contract(Contract): + def __init__(self, case : int): + super().__init__() + self.case = case + + def specification (self): + # Declare variables + (target, target_p) = ptr_to_fresh(self, alias_ty("struct.character_t"), name="target") + atk = self.fresh_var(i32, "atk") + + # Assert the precondition that the stats are below the max stat cap + # Suggests checkStats was called before resolveAttack + self.precondition_f("{atk} <= `{MAX_STAT}") + self.precondition_f("{target}.2 <= `{MAX_STAT}") + self.precondition_f("{target}.4 <= `{MAX_STAT}") + + # Determine the preconditions based on the case parameter + if (self.case == 1): + # target->def >= atk + self.precondition_f("{target}.4 >= {atk}") + elif (self.case == 2): + # target->hp <= (atk - target->def) + self.precondition_f("({target}.2 + {target}.4) <= {atk}") + else: + # Assume any other case follows the formal attack calculation + self.precondition_f("{target}.4 < {atk}") + self.precondition_f("({target}.2 + {target}.4) > {atk}") + + # Symbolically execute the function + self.execute_func(target_p, atk) + + # Determine the postcondition based on the case parameter + if (self.case == 1): + self.points_to(target_p['hp'], cry_f("{target}.2 : [32]")) + elif (self.case == 2): + self.points_to(target_p['hp'], cry_f("0 : [32]")) + else: + self.points_to(target_p['hp'], cry_f("resolveAttack ({target}.2) ({target}.4) {atk}")) + + self.returns(void) +``` + +Would this contract pass verification? Absolutely. Given that the `MAX_STAT` preconditions limits our input values, we would never see SAW's counterexample of an integer overflow/underflow from case 2. + +# Using Gained Knowledge + +## Assumptions and Lemmas + +Only functions with implementations in the bitcode can be verified. If one imports a function from a library, then that implementation will not be present in the bitcode generated as above. Instead of verifying these library functions we can use contracts to assume their behavior. + +For example, the height of +[height-balanced binary +trees](https://en.wikipedia.org/wiki/Self-balancing_binary_search_tree) +on n nodes is given by the ceiling of `log(n)`. In C we might try to implement this using + +```C +#include + +uint64_t ceilLog2(uint64_t i) { + return ceil(log2(i)); +} + +``` + +We may not care to verify this function because it's a library +function, especially if that library has already been formally +verified. Also, even if we have verified this function we would like +to speed up the verification procedure by black boxing its behavior. + +To accomplish these goals we make a contract outlining what the +behavior of this function: + +```python +class ceilLog2Contract(Contract): + def specification(self): + i = self.fresh_var(i64, "i") + + self.execute_func(i) + + self.returns_f("lg2 {i}") +``` + +We should note that `ceil(log2(i))` in C is NOT equal to Cryptol's `lg2` for values `1 << j + 1 where j > 49`. + +To illustrate this disparity, consider the following: + +```Xcryptol-session +Cryptol> let j49 = 1 << 49 + 1 : [64] +Cryptol> j49 +1125899906842624 +Cryptol> lg2 j49 +50 + +Cryptol> let j50 = 1 << 50 + 1 : [64] +Cryptol> j50 +2251799813685248 +Cryptol> lg2 j50 +51 + +Cryptol> let j50m1 = j50 - 1 +Cryptol> j50m1 +2251799813685247 +Cryptol> lg2 j50m1 +51 +``` + +```C +#include +#include +#include + +int main() +{ + uint64_t j49 = 1125899906842624; // 1 << j + 1 where j == 49 + uint64_t j50 = 2251799813685248; // 1 << j + 1 where j == 50 + uint64_t j50m1 = 2251799813685247; // j50 - 1 + + printf("ceil(log2(%ld)) = %llu\n", j49, (unsigned long long)ceil(log2(j49))); + printf("ceil(log2(%ld)) = %llu\n", j50, (unsigned long long)ceil(log2(j50))); + printf("ceil(log2(%ld)) = %llu\n", j50m1, (unsigned long long)ceil(log2(j50m1))); + + return 0; +} +``` + +```sh +$ gcc -o log2Test log2Test.c +$ ./log2Test +ceil(log2(1125899906842624)) = 50 +ceil(log2(2251799813685248)) = 52 +ceil(log2(2251799813685247)) = 52 +``` + +The lesson here, beware of `float`s claiming to mimic `int`s. To account for this disparity, we could add a precondition to our SAW contract. + +```python +class ceilLog2Contract(Contract): + def specification(self): + i = self.fresh_var(i64, "i") + + self.precondition_f("lg2 {i} <= 49") + + self.execute_func(i) + + self.returns_f("lg2 {i}") +``` + +In the unit test, we would assume the `ceilLog2Contract`: + +```python +log2i_assume = llvm_assume(mod, 'ceilLog2', ceilLog2Contract()) +``` + +If a C function ever used `ceilLog2`, then we could pass in the +assumption as an optional argument to verification: + +```python +getHeight_result = llvm_verify(mod, 'getHeight', getHeightContract(), lemmas=[ceilLog2_assume]) +``` + +The optional argument is a list because we can supply multiple +assumptions or previous verifications. For example, we might have + +```python +addNode_result = llvm_verify(mod, 'addNode', addNodeContract(), lemmas=[getHeight_result]) +removeNode_result = llvm_verify(mod, 'removeNode', removeNodeContract(), lemmas=[getHeight_result]) +addOneRemoveTwo_result = llvm_verify(mod, 'addOneRemoveTwo', addOneRemoveTwo(), lemmas=[addNode_result, removeNode_result]) +``` + +One can think of lemmas as rewrite rules under the hood. Whenever SAW +encounters ceilLog2 function in the C it will interpret its behavior as +what is specified in the `ceilLog2Contract()`. + +**Exercise**: Does the `C` function `ceilLog2` as defined above always yield the behavior outlined in `ceilLog2Contract`? That is, was our assumption a fair one to make? If not, change the `C` code (possibly using different library functions) to match `lg2` in Cryptol and verify it! + +Hint: consider [CLZ](https://en.wikipedia.org/wiki/Find_first_set#CLZ). + +```c +int __builtin_clzll (unsigned long long) +``` + +## Uninterpreting Functions + +Another way to simplify proofs is to uninterpret a function. This is +useful when you don't care about the specifics of the values produced +by a total function, but rather, the types of the value produced. For +example, hashing algorithms are often total functions. We often don't +care about the particular bits of a hash function, but rather, that +the hash function returned some 32-bit integer. + +This is also useful _in conjunction with lemmas_, reducing proof +complexity by decomposing a complex _specification_ into manageable +logical steps (constrained by the lemmas), much as verifying +function implementations and using results as lemmas does for the +corresponding _implementation_. + +See [SMT: Equality Logic With Uninterpreted Functions](https://www21.in.tum.de/teaching/sar/SS20/6.pdf), which describes +how uninterpreted functions and constraints are applied to +Satisfiability Modulo Theories. + +# Solicitation + +How was your experience with this lab? Suggestions are welcome in the +form of a ticket on the course GitHub page: +https://github.com/weaversa/cryptol-course/issues + +# From here, you can go somewhere! + +|||| +|-:|:-:|-| +|| [- Cryptographic Properties](../CryptoProofs/CryptoProofs.md) || diff --git a/labs/SAW/proof/addRow.py b/labs/SAW/proof/addRow.py new file mode 100644 index 00000000..5c9a54d1 --- /dev/null +++ b/labs/SAW/proof/addRow.py @@ -0,0 +1,76 @@ +import os +import unittest +from saw_client import * +from saw_client.crucible import * +from saw_client.llvm import * +from saw_client.proofscript import * +from saw_client.llvm_type import * + +def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None, read_only : Optional[bool] = False) -> Tuple[FreshVar, SetupVal]: + var = c.fresh_var(ty, name) + ptr = c.alloc(ty, points_to = var, read_only=read_only) + return (var, ptr) + +class addRow5Mutate_Contract(Contract): + def specification(self): + (a, a_p) = ptr_to_fresh(self, array_ty(5, i32), name="a") + (b, b_p) = ptr_to_fresh(self, array_ty(5, i32), name="b", read_only=True) + + self.execute_func(a_p, b_p) + + self.points_to(a_p, cry_f("addRow {a} {b}")) + self.returns(void) + +class addRow5NewVar_Contract(Contract): + def specification(self): + (a, a_p) = ptr_to_fresh(self, array_ty(5, i32), name="a") + (b, b_p) = ptr_to_fresh(self, array_ty(5, i32), name="b", read_only=True) + + self.execute_func(a_p, b_p) + + (c, c_p) = ptr_to_fresh(self, array_ty(5, i32), name="c") + self.points_to(c_p, cry_f("addRow {a} {b}")) + + self.returns(c_p) + +class addRowAlias_Contract(Contract): + def __init__(self, length : int): + super().__init__() + self.length = length + + def specification(self): + (a, a_p) = ptr_to_fresh(self, array_ty(self.length, i32), name="a") + (b, b_p) = ptr_to_fresh(self, array_ty(self.length, i32), name="b", read_only=True) + length = self.fresh_var(i8, "length") + + self.precondition_f("{length} == {self.length}") + + self.execute_func(a_p, b_p, length) + + self.points_to(a_p, cry_f("addRow`{{{self.length}}} {a} {b}")) + + self.returns(a_p) + +class ArrayTests(unittest.TestCase): + def test_rowAdds(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults(verbose_failure=True)) + + pwd = os.getcwd() + bcname = pwd + "/../src/addRow.bc" + cryname = pwd + "/spec/addRow.cry" + + cryptol_load_file(cryname) + mod = llvm_load_module(bcname) + + addRow5Mutate_result = llvm_verify(mod, 'addRow5Mutate', addRow5Mutate_Contract()) + self.assertIs(addRow5Mutate_result.is_success(), True) + + addRow5NewVar_result = llvm_verify(mod, 'addRow5NewVar', addRow5NewVar_Contract()) + self.assertIs(addRow5NewVar_result.is_success(), True) + + addRowAlias05_result = llvm_verify(mod, 'addRowAlias', addRowAlias_Contract(5)) + self.assertIs(addRowAlias05_result.is_success(), True) + +if __name__ == "__main__": + unittest.main() diff --git a/labs/SAW/proof/null.py b/labs/SAW/proof/null.py new file mode 100644 index 00000000..95968502 --- /dev/null +++ b/labs/SAW/proof/null.py @@ -0,0 +1,28 @@ +import os +import unittest +from saw_client import * +from saw_client.crucible import * +from saw_client.llvm import * + +class isNull_Contract(Contract): + def specification(self): + # p = self.alloc(i32) + + self.execute_func(null()) + + self.returns(cry("1 : [32]")) + +class LLVMAssertNullTest(unittest.TestCase): + def test_llvm_assert_null(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults(verbose_failure=True)) + + pwd = os.getcwd() + bcname = pwd + "/../src/null.bc" + mod = llvm_load_module(bcname) + + result = llvm_verify(mod, 'isNull', isNull_Contract()) + self.assertIs(result.is_success(), True) + +if __name__ == "__main__": + unittest.main() diff --git a/labs/SAW/proof/rotl.py b/labs/SAW/proof/rotl.py new file mode 100644 index 00000000..1af6d4df --- /dev/null +++ b/labs/SAW/proof/rotl.py @@ -0,0 +1,34 @@ +import os +import unittest +from saw_client import * +from saw_client.crucible import * +from saw_client.llvm import * +from saw_client.proofscript import * +from saw_client.llvm_type import * + +class rotl_Contract(Contract): + def specification(self): + xs = self.fresh_var(i32, "xs") + shift = self.fresh_var(i32, "shift") + + self.execute_func(xs, shift) + + self.returns_f("rotl {xs} {shift}") + +class rotlTest(unittest.TestCase): + def test_rotl(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults(verbose_failure=True)) + + pwd = os.getcwd() + bcname = pwd + "/../src/rotl.bc" + cryname = pwd + "/spec/rotl.cry" + + cryptol_load_file(cryname) + mod = llvm_load_module(bcname) + + rotl_result = llvm_verify(mod, 'rotl', rotl_Contract()) + self.assertIs(rotl_result.is_success(), True) + +if __name__ == "__main__": + unittest.main() diff --git a/labs/SAW/proof/spec/addRow.cry b/labs/SAW/proof/spec/addRow.cry new file mode 100644 index 00000000..bd7f4469 --- /dev/null +++ b/labs/SAW/proof/spec/addRow.cry @@ -0,0 +1,9 @@ +module addRow where + + +addRow5 : [5][32] -> [5][32] -> [5][32] +addRow5 a b = a + b + +addRow : {length} (fin length) => [length][32] -> [length][32] -> [length][32] +addRow a b = a + b + diff --git a/labs/SAW/proof/spec/rotl.cry b/labs/SAW/proof/spec/rotl.cry new file mode 100644 index 00000000..468664f7 --- /dev/null +++ b/labs/SAW/proof/spec/rotl.cry @@ -0,0 +1,4 @@ +module rotl where + +rotl : [32] -> [32] -> [32] +rotl xs shift = xs <<< shift diff --git a/labs/SAW/src/addRow.c b/labs/SAW/src/addRow.c new file mode 100644 index 00000000..dd9f3989 --- /dev/null +++ b/labs/SAW/src/addRow.c @@ -0,0 +1,25 @@ +#include +#include +#include + +void addRow5Mutate(uint32_t a[5], uint32_t b[5]) { + for(int i = 0; i < 5; i++) { + a[i] += b[i]; + } + return; +} + +uint32_t* addRow5NewVar(uint32_t a[5], uint32_t b[5]) { + uint32_t* c = (uint32_t*) malloc(5*sizeof(uint32_t)); + for(int i = 0; i < 5; i++) { + c[i] = a[i] + b[i]; + } + return c; +} + +uint32_t* addRowAlias(uint32_t* a, uint32_t* b, uint8_t length) { + for(int i = 0; i < length; i++) { + a[i] += b[i]; + } + return a; +} diff --git a/labs/SAW/src/null.bc b/labs/SAW/src/null.bc new file mode 100644 index 00000000..c5eaa589 Binary files /dev/null and b/labs/SAW/src/null.bc differ diff --git a/labs/SAW/src/null.c b/labs/SAW/src/null.c new file mode 100644 index 00000000..551d44fc --- /dev/null +++ b/labs/SAW/src/null.c @@ -0,0 +1,5 @@ + + +int isNull(int *x) { + return (x == (int*)0); +} diff --git a/labs/SAW/src/rotl.c b/labs/SAW/src/rotl.c new file mode 100644 index 00000000..8c119eb4 --- /dev/null +++ b/labs/SAW/src/rotl.c @@ -0,0 +1,7 @@ +#include +#include +#include + +uint32_t rotl(uint32_t bits, uint32_t shift) { + return (bits << shift) | (bits >> (sizeof(bits) * 8 - shift)); +} diff --git a/labs/SAW/src/rotl2.c b/labs/SAW/src/rotl2.c new file mode 100644 index 00000000..ac7621cf --- /dev/null +++ b/labs/SAW/src/rotl2.c @@ -0,0 +1,8 @@ +#include +#include +#include + +uint32_t rotl(uint32_t bits, uint32_t shift) { + shift %= sizeof(bits) * 8; + return (bits << shift) | (bits >> (sizeof(bits) * 8 - shift)); +} diff --git a/labs/SAW/src/rotl3.c b/labs/SAW/src/rotl3.c new file mode 100644 index 00000000..a6ee3f20 --- /dev/null +++ b/labs/SAW/src/rotl3.c @@ -0,0 +1,9 @@ +#include +#include +#include + +uint32_t rotl(uint32_t bits, uint32_t shift) { + shift %= sizeof(bits) * 8; + if(shift == 0) return bits; + return (bits << shift) | (bits >> (sizeof(bits) * 8 - shift)); +} diff --git a/misc/CryptolCourse.gv b/misc/CryptolCourse.gv index cd3d03ad..4baf51aa 100644 --- a/misc/CryptolCourse.gv +++ b/misc/CryptolCourse.gv @@ -31,6 +31,7 @@ digraph { Salsa20Properties [URL="../labs/Salsa20/Salsa20Props.html"]; TranspositionCiphers [URL="../labs/Transposition/Contents.html"]; ProjectEuler [URL="../labs/ProjectEuler/ProjectEuler.html"]; + ContinuousReasoning [URL="../labs/SAW/SAW.html"]; ParameterizedModules [URL="../labs/SimonSpeck/SimonSpeck.html"]; // newline/space labels @@ -44,6 +45,7 @@ digraph { TranspositionCiphers [label = "Transposition\nCiphers"] ParameterizedModules [label = "Parameterized\nModules"] Salsa20Properties [label = "Salsa20\nProperties"] + ContinuousReasoning [label = "SAW\nContinuous Reasoning"]; StyleGuide [label = "Style Guide"] ProjectEuler [label = "Project Euler"] @@ -69,6 +71,7 @@ digraph { CryptographicProperties -> Salsa20Properties; CryptographicProperties -> TranspositionCiphers; CryptographicProperties -> ProjectEuler; + CryptographicProperties -> ContinuousReasoning KeyWrapping -> ParameterizedModules; // ranks @@ -99,6 +102,7 @@ digraph { Salsa20Properties; TranspositionCiphers; ProjectEuler; + ContinuousReasoning; } { diff --git a/misc/CryptolCourse.gv.png b/misc/CryptolCourse.gv.png index 867231b6..5f690db0 100644 Binary files a/misc/CryptolCourse.gv.png and b/misc/CryptolCourse.gv.png differ diff --git a/misc/CryptolCourse.gv.svg b/misc/CryptolCourse.gv.svg index 9256ee97..ff8c8253 100644 --- a/misc/CryptolCourse.gv.svg +++ b/misc/CryptolCourse.gv.svg @@ -1,233 +1,281 @@ - - - - -%3 + + + -Installation + +Installation -Installation +Installation -Overview + +Overview -Overview +Overview -Installation->Overview - - + +Installation->Overview + + -Interpreter + +Interpreter -Interpreter +Interpreter -Overview->Interpreter - - + +Overview->Interpreter + + -LanguageBasics + +LanguageBasics -Language -Basics +Language +Basics -Interpreter->LanguageBasics - - + +Interpreter->LanguageBasics + + -CRC + +CRC - -CRC + +CRC -LanguageBasics->CRC - - + +LanguageBasics->CRC + + -StyleGuide + +StyleGuide - -Style Guide + +Style Guide -LanguageBasics->StyleGuide - - + +LanguageBasics->StyleGuide + + -CryptolDemos + +CryptolDemos - -Cryptol Demos + +Cryptol Demos -LanguageBasics->CryptolDemos - - + +LanguageBasics->CryptolDemos + + -SAWDemos + +SAWDemos - -SAW Demos + +SAW Demos -LanguageBasics->SAWDemos - - + +LanguageBasics->SAWDemos + + -TypeHackery + +TypeHackery - -Type Hackery + +Type Hackery -LanguageBasics->TypeHackery - - + +LanguageBasics->TypeHackery + + -Salsa20 + +Salsa20 - -Salsa20 + +Salsa20 -CRC->Salsa20 - - + +CRC->Salsa20 + + -CryptographicProperties + +CryptographicProperties - -Cryptographic -Properties + +Cryptographic +Properties -Salsa20->CryptographicProperties - - + +Salsa20->CryptographicProperties + + -KeyWrapping + +KeyWrapping - -Key Wrapping + +Key Wrapping -CryptographicProperties->KeyWrapping - - + +CryptographicProperties->KeyWrapping + + -Salsa20Properties + +Salsa20Properties - -Salsa20 -Properties + +Salsa20 +Properties -CryptographicProperties->Salsa20Properties - - + +CryptographicProperties->Salsa20Properties + + -TranspositionCiphers + +TranspositionCiphers - -Transposition -Ciphers + +Transposition +Ciphers -CryptographicProperties->TranspositionCiphers - - + +CryptographicProperties->TranspositionCiphers + + -ProjectEuler + +ProjectEuler - -Project Euler + +Project Euler -CryptographicProperties->ProjectEuler - - + +CryptographicProperties->ProjectEuler + + + + + +ContinuousReasoning + + +SAW +Continuous Reasoning + + + + + +CryptographicProperties->ContinuousReasoning + + -Capstone + +Capstone - -Capstone + +Capstone -KeyWrapping->Capstone - - + +KeyWrapping->Capstone + + -ParameterizedModules - - -Parameterized -Modules + +ParameterizedModules + + +Parameterized +Modules -KeyWrapping->ParameterizedModules - - + +KeyWrapping->ParameterizedModules + +