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
- Initial review
- Issue classification
- Developer remediation
- Final verification
- 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
immutablevariables 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.