Resources

People often ask me "How did you learn how to hack?" The answer: by reading. This page is a collection of the blog posts and other articles that I have accumulated over the years of my journey. Enjoy!

The Three Prompts of Spec Thinking: Yet Another Lens for Smart Contract Auditing- 1632

DraveePosted 11 Months Ago
  • One fantastic hacker is better than five good ones. We can make all of the checklists that we want and this will always be the case. Most bugs are not just items from a checklist - they are broken assumptions or mismatches between what the developer intended and what the code actually does. This article is about Spec Thinking - a strategy to uncover assumptions and the implicit rules of the system.
  • A smart contract is an asset management system where actors gain access to benefits through actions. Pretty simple way to break down some code! The author claims that all bugs fall into three categories: missing paths, incorrect happy paths and unexpected paths. Missing paths are just user intentions that aren't there - you can deposit money but can't withdraw.
  • Incorrect Happy Paths are features that exist but there's a fault or mistake in the state transitions. This is "wrong result but the right path". Things like rewards being miscalculated or state not being updated are good examples of this. These are often caught in testing but it becomes harder to find these with larger codebases or very complex flows.
  • Unexpected Paths are parts of a system that do more than intended. Weird edge cases, unsafe flows or badly scoped permissioned are where these bugs exist. In my experience, this is where most bugs are at and threat modeling works the best.
  • Specifications are how the system is supposed to behave. Invariants are statements that always must hold about a system. For instance, total supply must always equal the sum of all balances. Properties define what should hold true after executing a specific state transition. As an example, after withdrawing the user's balance should decrease by the withdrawn amount.
  • These matter because a bad property means something is wrong. If you understand the invariants, intents and expected properties, you can find how to break them. Understanding these parts of the system helps you get better good coverage. The idea is using this understanding of the system to create specifications at three different levels.
  • The first is the high level specification. This is in plain English how it works like "a user cannot lose funds unless they voluntarily withdraw or trade." The second is mid-level specification with state tracking. Finally, the code level specification for function-levels conditions and transitions. Drafting out the properties, invariants and flows of the protocol allow you to understand the code much better.
  • Formal methods teach you to understand the design intentions versus the implementation. You should be asking yourself three questions when working through these specs:
    1. What is expected?
    2. What is allowed?
    3. What was assumed but never enforced?
  • The specification thinking is something I do a good amount. I usually write out the entire flow from a high level step by step to understand what's going on. Over time, I get some properties and invariants for the protocol and see if I can break them. They have a good question that I should probably use more "What does the code assume, but never check?"
  • Overall, a good thought process on bug hunting. However, I felt this post was really dense and touched on a few too many things. If it just touched on the specs, it would have been better imo.