Module 5 – Smart Contract Security Engineering, Threat Modelling & Formal Verification

This final module presents an advanced security-engineering perspective on smart contracts and decentralised applications. We examine threat modelling, vulnerability classes, adversarial behaviour, formal verification, auditing methodologies, and secure development lifecycle design. The focus is to enable students to evaluate, defend, and harden blockchain systems at a professional and research-grade level.

1. Foundations of Blockchain Security Engineering

Smart contract security combines distributed-systems engineering, cryptography, economic game theory, and adversarial thinking. Unlike conventional software, smart contracts operate:

  • Publicly and transparently
  • Irreversibly
  • With immutable deployment
  • Under economic incentives
  • In adversarial environments

These properties make prevention, formal guarantees, and defence-in-depth essential.

1.1 Security Principles for Smart Contracts

  • Least privilege: minimal access and authorisation
  • Fail-safe defaults: restricted behaviour unless explicitly permitted
  • Minimised attack surface: reduce external calls, storage writes
  • Circuit breakers: pausing mechanisms under abnormal conditions
  • Economic safety: incentive-aware design

1.2 Types of Failures

Smart contract systems fail due to:

  • Logical vulnerabilities
  • Economic design flaws
  • Oracle failure
  • Governance manipulation
  • Protocol interaction vulnerabilities
  • Human error in deployment or configuration

2. Threat Modelling for Smart Contract Systems

Threat modelling identifies how an adversary can exploit a system. Effective models account for technical, economic, and behavioural threats.

2.1 Adversary Types

  • External attackers: exploit contract logic
  • Insiders: privileged actors misusing admin roles
  • Miners/validators: exploiting reordering or censorship
  • Governance attackers: capturing voting power
  • Economic adversaries: arbitrageurs manipulating price

2.2 STRIDE for Smart Contracts

The STRIDE model adapts to smart contracts:

  • S – Spoofing: impersonating privileged roles
  • T – Tampering: state manipulation via bugs
  • R – Repudiation: unverifiable off-chain behaviour
  • I – Information disclosure: leakage of sensitive state
  • D – Denial of service: gas griefing, reverts
  • E – Elevation of privilege: bypassing access control

2.3 Attack Surface Mapping

Attack surfaces include on-chain code, off-chain components, governance processes, price feeds, and user signature flows.


3. Vulnerability Classes in Smart Contracts

Smart contracts are subject to a range of well-known and emerging vulnerabilities. Below is a structured overview of critical classes.

3.1 Re-entrancy

Occurs when a contract sends ETH or calls another contract before updating state. The external call re-enters the function and manipulates state.

3.2 Integer Overflow & Underflow

Arithmetic exceeding limits results in wrap-around errors.

3.3 Access Control Misconfiguration

Missing or incorrect modifiers allow unauthorised actors to mint, burn, or change parameters.

3.4 Oracle Manipulation

  • Using illiquid DEX pools as price reference
  • Manipulating TWAP windows
  • Stale price reads

3.5 Front-Running & MEV Attacks

Miners reorder transactions for arbitrage, liquidation capture, or sandwiching.

3.6 Flash-Loan Exploits

Attackers borrow large capital to manipulate prices, collateral ratios, or protocol logic.

3.7 Signature Replay Attacks

Re-using old signatures on new chains or states.

3.8 Logic Bugs in State Machines

Incorrect state-transition rules allow illegal behaviour sequences.

3.9 Gas Griefing & Denial of Service

Attackers intentionally cause out-of-gas reverts or force expensive computation.


4. Secure Smart Contract Design Patterns

4.1 Checks–Effects–Interactions

Update state before calling external contracts.

4.2 Pull Payments

Avoid sending ETH directly; users withdraw funds themselves.

4.3 Access Control Frameworks

  • Ownable
  • Role-based access (RBAC)
  • Multi-signature roles
  • DAO-based governance

4.4 Rate Limiting

Restrict certain operations to prevent rapid manipulation (mint caps, withdrawal limits).

4.5 Emergency Pause (Circuit Breaker)

Allows disabling critical functions during suspected attacks.


5. Formal Verification

Formal verification mathematically proves that a contract satisfies certain invariants or behaviours. Unlike testing, it evaluates all possible execution paths under specified assumptions.

5.1 Specification Writing

A specification defines intended behaviour using mathematical logic. Examples:

  • Invariant: total supply never exceeds maxSupply
  • Invariant: no unauthorised minting
  • Property: transfers maintain sum(balanceOf)

5.2 Verification Tools

  • SMT solvers
  • Model checkers
  • Symbolic execution tools
  • KEVM and Isabelle/HOL for EVM semantics

5.3 Formal Verification Failure Cases

Verification can be misleading if:

  • Specifications are incomplete
  • Assumptions do not reflect real-world scenarios
  • Economic behaviours are not modelled

Despite limitations, formal verification is indispensable for mission-critical systems.


6. Static and Dynamic Security Analysis

Security engineering employs a combination of static and dynamic tools.

6.1 Static Analysis

Inspects bytecode or source code without executing it.

  • Detects overflow, unused variables, uninitialised storage
  • Finds dead code paths
  • Identifies unbounded loops

6.2 Dynamic Analysis

Executes the contract under simulated conditions.

  • Fuzzing (randomised input generation)
  • Symbolic execution
  • Transaction-level simulation

6.3 Runtime Monitoring

Monitoring contract events, gas usage, anomalies, and failed calls in production.


7. Professional Smart Contract Auditing

Audits provide an independent evaluation of security, logic correctness, risk exposure, and architecture robustness.

7.1 Audit Scope

  • Code review
  • Attack path enumeration
  • State machine correctness
  • Economic modelling
  • Gas optimisation
  • Governance review

7.2 Multi-Stage Auditing

  1. Initial review
  2. Issue classification
  3. Developer remediation
  4. Final verification
  5. On-chain monitoring after deployment

7.3 Categories of Audit Findings

  • Critical: funds at risk
  • High: major logic flaw or privilege escalation
  • Medium: potential attack vector under certain conditions
  • Low: minor issue, gas inefficiency
  • Informational: stylistic or documentation issues

8. Security in Upgradeable Contract Architectures

Proxy-based upgradeability introduces additional risk factors.

8.1 Storage Layout Safety

Storage variable order must never change between upgrades.

8.2 Admin Key Management

  • Multi-sig controlled
  • Time-locked upgrades
  • DAO governance for high-stakes protocols

8.3 Upgrade Failure Modes

Common risks include:

  • Bricking contracts through incorrect storage alignment
  • Compromised admin keys
  • Malicious upgrades by governance attackers

9. Economic, Governance & Incentive Attacks

Many high-profile DeFi failures originate from incentive misuse, not code bugs.

9.1 Governance Takeovers

  • Acquiring cheap tokens to control votes
  • Flash-loan-based voting attacks

9.2 Oracle Price Gaming

Manipulating assets used as collateral triggers forced liquidations.

9.3 Liquidity Extraction Attacks

Draining liquidity from thin AMM pools to distort prices or amplify slippage.

9.4 Incentive Collapse

Unsustainable emissions or APYs collapse when token demand decreases.


10. Defence-in-Depth Strategies for Smart Contract Systems

Combining multiple layers of protection yields better resilience.

  • Formal verification for critical modules
  • Optimised code review
  • Fail-fast logic checks
  • Pausing and kill-switch mechanisms
  • Multi-sig control over treasuries
  • Monitoring dashboards
  • Bounties and continuous audits

Each component contributes to layered risk reduction.


11. Security Checklist for Smart Contract Developers

  • Zero unbounded loops in critical functions
  • No state changes after external calls
  • Use immutable variables whenever possible
  • Verify constructor sets correct roles
  • Ensure proper error handling
  • Write comprehensive tests and invariants
  • Simulate extreme market conditions
  • Audit dependencies and oracles
  • Document all assumptions and limitations

12. Case Studies from Real DeFi Exploits

12.1 The DAO (2016)

Re-entrancy attack caused theft of millions in ETH.

12.2 bZx Exploits

Flash-loan attacks exploiting price manipulation across AMMs.

12.3 Wormhole Bridge Hack

Verification bypass led to unauthorised minting of wrapped assets.

12.4 Curve Stablecoin Exploits

Re-entrancy vulnerabilities in Vyper compiler versions.

These events illustrate how combinations of technical, oracle, and governance weaknesses create systemic failures.


13. Module Summary

This module delivered a comprehensive approach to smart contract security: threat modelling, vulnerability analysis, secure design patterns, economic attack surfaces, formal verification, auditing workflows, and defence-in-depth engineering. Together, these concepts prepare learners to evaluate, defend, and build advanced decentralised systems with high assurance.

This concludes Course 3. You are now equipped with a full-stack, engineering-level understanding of smart contract design, development, architecture, DeFi mechanics, and security engineering.

Pages: 1 2 3 4 5 6