Suppose DCRouter's ports belong to different tenants, and a disabled port must keep one tenant's traffic out. BUG_23 (a disabled port still accepts traffic) was, in Part 1, a configuration bug. In a security setting it is an isolation breach that an attacker would look for deliberately. And even a correct DCRouter might leak something subtler: whether another tenant is sending, visible as the delay its own packets see at a shared output.
How do you verify a security property?
The obvious approach is to add security tests to the functional plan. Functional tests check expected behaviour on expected inputs; an attacker chooses the unexpected ones, including timing and induced faults, and security failures are often about what the design reveals rather than what it computes. In Spectre and Meltdown every architectural result was correct and data still leaked (fact C3).
Kind of property | Example | How verified |
|---|---|---|
Access control | A disabled port never accepts traffic; a register is writable only in secure mode | Assertions and formal (DCRouter's R1 assertion) |
Information flow (confidentiality) | Data from tenant A never reaches tenant B's outputs or registers | Information-flow tracking (taint) in simulation or formal |
Integrity | Untrusted inputs never change trusted state | Formal and taint analysis |
Timing side channels | Observable timing does not depend on secret data | Timing analysis, formal non-interference checks, measurement |
Fault attacks | Glitches or flipped bits cannot bypass a check | Fault injection (lesson 15.1) aimed at security decisions |
Debug and test access | Scan and debug ports locked in the field | Directed tests and formal on lock logic |
Access: a disabled port's in_rdy is never high (R1); formal can prove it for every input sequence, not just tested ones.
Flow: a packet from input A appears only at its destination output, never in another tenant's registers; a taint check would tag A's data and assert it never reaches B's outputs.
Timing: input B's packets wait longer when input A is busy at the same output; that delay reveals A's activity. Whether it matters is a threat-model decision, and removing it needs a different arbitration policy (time slots), not a bug fix.
Start from a threat model: assets, attackers, what they control.
Write security properties as negatives, then prove them where possible: absence of behaviour is what formal does best.
Track information flow: taint propagation shows where secrets can travel.
Attack the design: fault injection and fuzzing at security decision points.
Review debug, test and reset paths: classic ways around protections.
Practice | Purpose |
|---|---|
Threat models and security requirements in the plan | Security features verified like any other, with negative properties |
Formal and information-flow tools on security blocks | Absence of leaks and bypasses proved |
Red-team reviews and fault-injection campaigns | Attacker thinking applied before silicon |
Spectre and Meltdown are the canonical example (lesson 16.4): processors that passed every functional check, because every architectural result was right, leaked data through cache timing after speculative execution. No functional scoreboard could have flagged it; only properties about what must not be observable could.
It becomes an isolation breach that an attacker can seek out deliberately, not just a configuration mistake.
Every output is correct; the leak is in when outputs appear, which depends on secret activity, and the scoreboard does not check timing as information.
Security verification checks what must not happen, under an adversary.
Write negative properties (access, flow, timing, faults) and prove them where possible.
Correct results are not evidence of no leaks.