Skip to content

Latest commit

 

History

History
117 lines (84 loc) · 5.78 KB

GameDLC.md

File metadata and controls

117 lines (84 loc) · 5.78 KB
Raw

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