Frequently Asked Questions
What is the difference between security engineering and a security audit?
A security audit reviews finished code for vulnerabilities. Security engineering embeds security throughout development — designing contracts with explicit invariants, testing those invariants with fuzz testing, running static analysis on every commit, and modelling economic attacks before implementation. The output of security engineering is contracts that are hard to exploit by construction. The output of an audit is a list of vulnerabilities in existing code. Both are needed; security engineering reduces what the audit finds.
What are invariants and why do they matter?
A protocol invariant is a property that must always be true regardless of what operations have been performed — "the sum of all user balances equals the total supply," "the collateral value of every vault always exceeds its debt," "only the governance timelock can change protocol parameters." Defining invariants explicitly before implementation gives you a testable specification. Echidna and Foundry fuzz testing can then systematically try to violate them. Invariants that are not explicitly defined are invariants that get broken during development.
What is read-only reentrancy?
Standard reentrancy attacks reenter a state-modifying function to drain funds or manipulate state. Read-only reentrancy is subtler: the attacker reenters a view function — which reads state that is temporarily in an inconsistent state during a transaction. If another protocol uses that view function to calculate a price or ratio, it reads an incorrect value. This has been exploited against protocols built on top of Curve, where the virtual price was readable mid-transaction in an inconsistent state. Most automated tools miss this class.
When should we use formal verification?
Formal verification is justified when the cost of a wrong answer is catastrophic and the property to be verified is well-defined. Specifically: for protocols expecting >$50M TVL, for bridge contracts that custody assets across chains, for stablecoin peg mechanisms, and for access control properties where bypass has irreversible consequences. Certora Prover is the practical tool for most teams — it can prove properties like "only the owner can mint" and "total shares never exceed total deposits" with mathematical certainty.
How do you prevent flash loan attacks?
Flash loan attacks exploit temporary capital availability within a single block. Prevention: never use spot price from an on-chain pool for security-critical calculations, use TWAP oracles or Chainlink, take governance snapshots at past blocks rather than current balance, use re-entrancy guards to prevent mid-transaction state manipulation, and add rate limiting or volume circuit breakers. The economic design is as important as the technical implementation — if the profit from a flash loan attack exceeds the cost, someone will execute it.
What monitoring should we have post-deployment?
At minimum: alerts on anomalous contract function calls (unusual volume, calls from new addresses with large transactions), price deviation alerts (if your protocol involves pricing), governance proposal alerts (any proposal submitted), and emergency pause event monitoring. OpenZeppelin Defender Sentinel, Forta Network and Tenderly Actions all provide this. The goal is to know about a potential exploit before users do — ideally with enough time to pause the protocol before losses become catastrophic.
What is the Certora Prover?
Certora Prover is a formal verification tool for Solidity smart contracts. You write "specifications" in Certora Verification Language (CVL) that describe properties your contract must satisfy — for example, "after any call to withdraw(), the caller's balance decreases by exactly the withdrawn amount." The Prover mathematically verifies that these properties hold for all possible inputs and all possible states. It is the only tool that can provide certainty rather than confidence. Major protocols including Aave, Compound and MakerDAO use Certora Prover.
How much test coverage is enough?
100% line coverage is necessary but not sufficient. A contract with 100% line coverage can have critical vulnerabilities that are never triggered by the test inputs the developer wrote. The correct measure is: 100% line coverage + invariant testing with Echidna covering all protocol invariants + fuzz testing for all functions with numeric inputs + edge case coverage for boundary values. Coverage is a floor, not a ceiling. The goal is to test all the ways things can go wrong, not just the ways things should go right.
