Silicon-rooted Security experimental

Silicon-rooted Security Down from software abstraction to gates, datapaths and buses, where trust is rooted in hardware From software to silicon. Gates, datapaths and buses, and how an instruction becomes signals moving through hardware.. Explain how logic gates compose into a datapath.. Model how an instruction becomes control and data signals.. Read a datapath-and-bus animation.. Gates and logic, Datapaths, Buses, From instruction to signals From software to silicon Every abstraction you have used so far in this track (a function call, a memory safety bug, a formally verified property) ultimately runs as physical switching activity in a piece of silicon. ANVIL takes you down that ladder: from an instruction as text, to an instruction as bits, to an instruction as voltages moving through wires and transistors on a clock's schedule. Descending this ladder matters to a defender because every software guarantee is only as strong as the hardware underneath it; a root of trust that lives below software cannot be patched around by software, for better and for worse. Gates and logic A logic gate is a physical element (built from transistors) that computes a Boolean function of its inputs: AND, OR, NOT, eXclusive OR (XOR) and their combinations. Gates are composed into larger combinational circuits, whose output depends only on the current inputs, and into sequential circuits, which include memory elements (flip-flops, registers) whose output also depends on past inputs. A processor's control logic is, at bottom, a network of gates that decides which signals to assert on any given clock cycle. Nothing in a CPU is 'magic'; every decision, including a security check, reduces to gates evaluating Boolean functions of bits. Datapaths A datapath is the hardware through which data actually flows and is transformed: registers that hold values, arithmetic-logic units that compute on them, multiplexers that select among candidate values, and the wiring connecting them. Where control logic decides 'what to do this cycle', the datapath is 'the machinery that does it'. A register updates only on a clock edge, and only when its enable signal is asserted by control logic; this synchronous discipline is what makes hardware behaviour deterministic and analysable one cycle at a time. Buses A bus is a shared set of wires carrying data, addresses or control signals between components: the CPU, memory, and peripherals. Because a bus is shared, anything with electrical or logical access to it can potentially observe or inject signals onto it; this is precisely the vulnerability Module 04 exploits and defends. Buses are described by a protocol: which wires carry what, and in what order, so that senders and receivers agree on meaning. From instruction to signals When a core executes an instruction, the instruction's encoded bits are decoded into control signals; those signals steer multiplexers, enable registers and select Arithmetic Logic Unit (ALU) operations in the datapath, cycle by cycle, paced by the clock. A waveform view lets you watch this directly: a signal's value over time, revealing exactly when a register updates and why. Throughout ANVIL you will read waveforms to verify that hardware behaves as specified, and later, that a security property truly holds over the signals, not just in prose. Related CCI capabilities Computer Architecture (Course): (https://www.cambridgecyberinternational.com/en/insights/academy/computer-architecture/). CCI Lab: Run it, build with it, read the thinking, reuse the data. (https://www.cambridgecyberinternational.com/en/insights/lab/) From transistor to logic gate The transistor, invented at Bell Laboratories in 1947 by John Bardeen, Walter Brattain and William Shockley, replaced the vacuum tube as the switching element behind digital logic, and its solid-state reliability is what made a gate-level abstraction practical to build in volume rather than as a laboratory curiosity. Jack Kilby's 1958 demonstration of the integrated circuit at Texas Instruments, followed closely by Robert Noyce's 1959 planar-process patent at Fairchild Semiconductor, showed that many transistors could be fabricated together on a single piece of silicon, which is the step that turned a handful of gates into the millions-of-transistors datapaths a modern processor contains. A logic gate's behaviour is fully described by a truth table, but a datapath's behaviour depends on how gates are wired together and clocked, which is why this module treats the datapath as an animated object rather than a static diagram: a register's value only changes on a clock edge, and a multiplexer's output depends on a select signal that itself came from earlier logic in the same cycle. Reading a waveform, rather than only a schematic, is the skill that lets a defender see this timing dependency directly instead of inferring it from documentation that may be stale or wrong. Understanding this software-to-silicon descent matters to a defender because every security property a higher layer claims, an access control check, an encryption boundary, ultimately reduces to a specific arrangement of gates and registers that either enforces that property or does not; a vulnerability that looks like a software bug from above can just as easily be a hardware datapath that never implemented the check the software assumed was there. The datapath and the ISA. A RISC-V-class core: fetch, decode, execute, and the register file over the bus.. Describe fetch, decode and execute in a simple core.. Explain the register file and its role in the datapath.. Run the core step by step, single-stepping it to read its datapath signals.. Fetch, decode, execute, The register file, The datapath in motion, A RISC-V-class core The datapath and the ISA An instruction set architecture (ISA) is the contract between software and hardware: the set of instructions a core promises to execute and what each one means. A microarchitecture, the datapath and control logic you actually build, is one of many possible ways to honour that contract. This module ties the two together in a simple Reduced Instruction Set Computer (RISC)-V-class core, the shared machine model this track reuses so a new security mechanism can be studied against a machine you already understand rather than against unfamiliar plumbing each time. Fetch, decode, execute A simple instruction cycle has three visible stages. Fetch reads the instruction word located at the address held in the program counter (PC) from memory. Decode interprets that word's fields: which operation, which source and destination registers, which immediate value. Execute performs the operation, typically in the Arithmetic Logic Unit (ALU), and a write-back step commits the result to the register file or memory, after which the PC advances (sequentially, or to a branch target). Each stage's behaviour is driven by control signals produced during decode. The register file The register file is the core's small, fast array of general-purpose registers, distinct from main memory: it has few entries, low latency, and multiple read/write ports so an instruction can read two source operands and (later) write one result within a single cycle. RISC-V is a load/store architecture: arithmetic instructions operate only on registers, and explicit load and store instructions are the sole path moving data between the register file and memory, itself reached over the bus. This separation keeps the common case (register arithmetic) fast and pushes the slower memory interaction into instructions designed for it. The datapath in motion Single-stepping the core means advancing exactly one clock cycle and inspecting every signal and register before and after: which instruction was fetched, which control signals decode asserted, which multiplexer inputs were selected, and which register or memory location changed. This is how you verify, concretely, that a core behaves as its ISA specifies, rather than trusting a description of intended behaviour. A RISC-V-class core RISC-V is an open, royalty-free, reduced-instruction-set ISA with a small, regular base instruction set and fixed-width encodings, which simplifies decode logic and keeps the datapath's control simpler to build, verify and extend. Its openness and modular extension mechanism (reserved opcode space for optional extensions) are exactly why Module 02 can graft a new security opcode onto this same core without redesigning it from scratch, and why this core recurs across the track as one audited machine model rather than a new one per course. Related CCI capabilities Computer Architecture (Course): (https://www.cambridgecyberinternational.com/en/insights/academy/computer-architecture/). CCI Lab: Run it, build with it, read the thinking, reuse the data. (https://www.cambridgecyberinternational.com/en/insights/lab/) The RISC-V teaching architecture RISC-V, first published by Krste Asanovic, Yunsup Lee and Andrew Waterman at the University of Berkeley beginning in 2010, was designed from the outset as an open, royalty-free instruction set architecture suitable for both industrial silicon and classroom teaching, which is why this course, like a growing number of computer-architecture programmes worldwide, uses it as the shared core configuration across every module that needs one. Its load-store design, where only dedicated load and store instructions touch memory and all arithmetic operates on registers, keeps the fetch-decode-execute cycle this module teaches uncluttered by the addressing-mode complexity older architectures accumulated. The classic five-stage pipeline, fetch, decode, execute, memory access and writeback, traces back to instruction-set design work published by John Hennessy and David Patterson in the 1980s and later formalised in their widely used computer-architecture textbooks; RISC-V's regular, fixed-width encoding is a direct descendant of that same design philosophy, favouring instructions that are easy for hardware to decode over instructions that are easy for a human assembly programmer to read. Single-stepping the simulated core through this five-stage cycle is what turns the pipeline diagram from an abstraction into a concrete, inspectable sequence of register and control-signal changes, which is exactly the skill Module 02's opcode-extension exercise and the model-checking work in Modules 08 and 09 both build on directly. Adding a security opcode. Extending the ISA and datapath with a new instruction and observing it execute.. Describe how a new opcode extends the ISA, then extend it.. Build the datapath and control wiring for the new instruction.. Observe the security opcode execute.. Extending the ISA, Datapath and control changes, A security opcode, Observing it execute Adding a security opcode Hardware-enforced security mechanisms often begin as a new instruction: an operation the Instruction Set Architecture (ISA) did not previously offer, wired directly into the datapath so it runs with hardware speed and, crucially, cannot be bypassed purely from software the way a library routine can be. This module extends the Reduced Instruction Set Computer (RISC)-V-class core from Module 01 with exactly one new opcode and traces it all the way from encoding to execution. Extending the ISA RISC-V is designed for extension: its encoding reserves opcode space precisely so new instructions can be added without colliding with, or reinterpreting, existing ones. Extending the ISA means choosing an unused encoding, defining its fields (which bits name source/destination registers, which carry an immediate or function code), and writing down precisely what it must do to the architectural state. This specification, not the eventual gateware, is the source of truth the datapath must be built to satisfy. Datapath and control changes Giving an instruction meaning requires two coordinated changes. First, decode logic must recognise the new opcode's bit pattern and distinguish it from every existing instruction. Second, the datapath and control signals must be extended: a new multiplexer input, a new enable line to a register, or a new functional unit, so that the resource performing the security operation is wired into the existing structure of registers, Arithmetic Logic Unit (ALU) and buses rather than bolted on separately. If decode is updated but no control signals are wired to a datapath action, the opcode will decode cleanly and yet do nothing when executed, a classic integration gap. A security opcode A security opcode typically performs an operation software could not safely or atomically perform itself: a memory-tag check that gates an access, a cryptographic key operation kept out of general-purpose registers, or a measurement-register update (the mechanism Module 05's measured boot depends on). Because the operation executes inside the trusted hardware boundary, it can enforce invariants, such as 'this register can only be extended, never overwritten' that no amount of software discipline can guarantee on its own. Observing it execute Specifying an opcode is not the same as knowing it works. You single-step the modified core through a program that issues the new instruction and confirm, cycle by cycle in the waveform view, that decode asserts the expected control signals and that the correct register or datapath state changes exactly as specified, no more and no less. This observed execution, not a description of intended behaviour, is the pass condition: it is the difference between an opcode that is documented and one that is verified to exist in the hardware. Related CCI capabilities Computer Architecture (Course): (https://www.cambridgecyberinternational.com/en/insights/academy/computer-architecture/). CCI Lab: Run it, build with it, read the thinking, reuse the data. (https://www.cambridgecyberinternational.com/en/insights/lab/) Precedent: adding security opcodes to a general-purpose core Extending a general-purpose instruction set with dedicated security opcodes is not a novel idea this course invents; Intel's Advanced Encryption Standard (AES) New Instructions (NI), branded AES-NI and introduced in 2010, added six new instructions that perform Advanced Encryption Standard round operations directly in hardware, specifically so that a cipher's correctness and timing behaviour would not depend on how carefully a software library implemented it. Intel's Software Guard Extensions (SGX), introduced in 2015, went further still, adding a family of opcodes that create and manage an isolated enclave whose memory the operating system itself cannot read, a security guarantee no purely architectural instruction set could offer without new hardware-enforced opcodes. Both precedents share the same shape this module's exercise follows: reserved opcode space in the encoding, a precise specification of what the new instruction must do to architectural state, and a decoder change that recognises the new bit pattern and routes it to new control logic rather than to the existing arithmetic or memory-access paths. Getting the decoder change wrong in exactly the way the module's simulated fault demonstrates, an opcode that decodes correctly but drives no new datapath logic, is a realistic failure mode, not a contrived one; it is functionally identical to shipping a security feature that appears to exist in the instruction manual but does nothing when executed. The broader lesson AES-NI and SGX both teach is that a hardware-implemented security operation can be stronger than a software equivalent precisely because it removes an entire class of software-level bugs, timing side channels from data-dependent branches, cache-timing leaks from table lookups, that a compiler and operating system can otherwise introduce even when the underlying algorithm is correct. Gateware cipher datapaths. Building a cipher as a hardware datapath and clocking test vectors through it.. Describe a cipher round's structure, then build it as a hardware datapath.. Clock test vectors through the datapath.. Verify the output against known-answer test vectors.. A cipher as a datapath, Rounds and state, Clocking test vectors, Known-answer verification Gateware cipher datapaths A block cipher is usually met first as a software function. This module rebuilds one as gateware: logic that performs substitution, permutation and key mixing directly in hardware, clocked one round per cycle (or unrolled across combinational logic), so confidentiality is rooted in silicon rather than a call into a library that a compromised operating system could intercept or replace. A cipher as a datapath Implementing a cipher as a hardware datapath means wiring its defined transformations, substitution boxes, bit permutations, and modular mixing, as combinational logic (computing a function of current inputs) interleaved with sequential logic (registers holding state between rounds). Each transformation the specification describes as a mathematical step over bytes or bits becomes a concrete piece of circuitry: an S-box becomes a lookup implemented in gates, a permutation becomes fixed wiring that reorders bits, and mixing becomes an arithmetic or eXclusive OR (XOR) network. Rounds and state Most block ciphers iterate a round function multiple times. In gateware, a state register holds the current intermediate value; each clock cycle applies one round's transformation and writes the result back into that register, until the specified round count is reached, at which point the state register holds the final ciphertext (or plaintext, for decryption). A key schedule, itself a small datapath, derives a distinct per-round key from the master key and feeds it into each round's mixing step; getting the round count or the key schedule wrong is one of the most common implementation bugs. Clocking test vectors A test vector is a fixed input (plaintext and key) paired with its correct, published output (ciphertext), taken from the cipher's official specification. Clocking a vector through the datapath means loading the input and key into the appropriate registers, then advancing the clock through every round, and finally reading the output register once processing completes. This is a deterministic, repeatable procedure: given the same input and key, a correct datapath produces the same output every time. Known-answer verification Known-answer testing compares the datapath's output against the specification's published vectors: the implementation passes only when the two match exactly. This is the standard, objective check for cryptographic hardware because it is reproducible and does not depend on trusting the implementer's own reasoning. When a vector fails, the disciplined response is to inspect the state register across cycles to localise which round or transformation first diverged from the expected value (a wrong constant, a misordered round, an off-by-one in round count), fix that specific fault, and re-run every vector, since a fix for one input must not silently break another. Related CCI capabilities Computer Architecture (Course): (https://www.cambridgecyberinternational.com/en/insights/academy/computer-architecture/). CCI Lab: Run it, build with it, read the thinking, reuse the data. (https://www.cambridgecyberinternational.com/en/insights/lab/) The Advanced Encryption Standard as a hardware target The cipher this module's datapath implements follows the shape of the Advanced Encryption Standard, which the National Institute of Standards and Technology selected in 2001 as Federal Information Processing Standard 197 after an open, multi-year public competition among fifteen candidate ciphers submitted by cryptographers worldwide. NIST published known-answer test vectors alongside the standard itself specifically so that any implementation, whether in software or, as this module builds, directly in gateware, could be checked against a fixed set of input-key-output triples without needing to trust the implementer's own test suite. A round-based cipher datapath's state register exists because the standard itself is defined as a fixed number of structurally identical rounds, each applying the same sequence of byte-substitution, row-shifting, column-mixing and key-addition operations to the state that the previous round produced; building the datapath to clock a fresh round each cycle, rather than unrolling all rounds into combinational logic, is a direct hardware expression of that round structure. Verifying the datapath against the standard's own known-answer vectors, rather than only checking that the circuit "looks right," is exactly the discipline that caught the historically real category of implementation bugs (an off-by-one round count, a mis-ordered key schedule) that plagued early software AES implementations before hardware acceleration became standard. Intel's AES-NI extension, introduced in 2010 (see Module 02's Advanced Encryption Standard (AES) New Instructions (NI) discussion), later moved this same round structure directly into general-purpose silicon, which is the strongest possible confirmation that a hardware AES datapath is not an academic exercise: it is the production design pattern the wider industry converged on for exactly the performance and side-channel reasons this module's lab lets you observe directly. Bus protection: encryption and integrity tagging. Protecting data on the bus with encryption and integrity tags, and the cost of doing so.. Explain the effect of toggling bus encryption, then toggle it and observe that effect.. Build integrity tagging into the bus and detect a tampered transfer.. Reason about the cost of bus protection.. Data on the bus, Bus encryption, Integrity tagging, The cost of protection Bus protection: encryption and integrity tagging Module 03 built a cipher datapath; this module puts it to work protecting the bus itself, the shared wires connecting the core to memory and peripherals, which is exactly where a probe, a malicious peripheral, or an attacker with physical access can observe or tamper with data in transit. Data on the bus A bus is shared by construction, and anything with electrical or logical access to it can potentially observe every transfer that crosses it. Data sent in plaintext across a bus to Dynamic Random-Access Memory (DRAM) or a peripheral can be read by a bus probe or a compromised component sharing that bus, and can be modified in transit; neither the sender nor the ordinary receiver logic detects this unless protection is explicitly added. Bus encryption Bus encryption applies a cipher, such as the one built in Module 03, to data as it crosses the bus, so an observer with access to the wires sees only ciphertext and cannot recover the underlying value. A memory-encryption engine sitting between the core and DRAM is a concrete instance: it encrypts data on the way out and decrypts it on the way back, so physical access to the memory bus or the DRAM chips themselves does not, by itself, reveal secrets. Integrity tagging Encryption alone protects confidentiality but not integrity: an attacker who cannot read the plaintext can often still flip bits in the ciphertext, producing an incorrect but plausible-looking decrypted value, undetected. Integrity tagging closes this gap by attaching a message authentication code (MAC) to each transfer; the receiver recomputes the expected tag and rejects the transfer if it does not match. Freshness, typically a counter or nonce folded into the tag, additionally prevents an attacker from replaying a previously valid, correctly tagged transfer at a later time. The cost of protection None of this is free. Encryption and tagging add latency (cycles spent computing the cipher and MAC before data can be used), area (the cipher and MAC logic occupy silicon), and energy, all of which must be weighed against the threat being addressed; not every bus, in every system, justifies full protection. The lab lets you toggle protection on and off and observe directly: with it off, an on-bus observer reads plaintext and an injected bit-flip goes silently through; with encryption alone, the plaintext is hidden but a tamper can still corrupt data undetected; only encryption plus integrity tagging (and freshness) gives you confidentiality, tamper detection, and replay resistance together, at a cost you can now reason about concretely rather than assume away. Related CCI capabilities Computer Architecture (Course): (https://www.cambridgecyberinternational.com/en/insights/academy/computer-architecture/). CCI Lab: Run it, build with it, read the thinking, reuse the data. (https://www.cambridgecyberinternational.com/en/insights/lab/) Bus and memory encryption in production silicon The threat this module's lab demonstrates, plaintext data readable by anyone who can physically probe a bus or DRAM chip, is not hypothetical: Advanced Micro Devices (AMD)'s Secure Memory Encryption feature, introduced in 2016, and Intel's Total Memory Encryption feature, introduced in 2018, both exist specifically because a physical attacker with access to the memory bus or the DRAM modules themselves can otherwise read a running system's entire memory contents regardless of any software-level access control. Both features encrypt data as it crosses the memory bus and decrypt it only inside the processor package, which is architecturally the same toggle this module's simulated bus protection control represents. Encryption alone answers confidentiality but not integrity: a bit flipped in transit on an encrypted bus still decrypts to something, just not the correct plaintext, which is why production memory-encryption engines add an integrity tag, typically a cryptographic message authentication code computed over each cache line, so a tampered transfer is detected rather than silently corrupting a computation. Freshness protection, a per-transfer counter or nonce folded into the tag computation, closes the remaining gap: without it, an attacker who has recorded a previous, validly-tagged transfer can replay it later, and the receiver's integrity check alone cannot distinguish a replay from a fresh, legitimate write. The cost of this protection is real and is exactly why the toggle in this module's lab is worth building rather than only describing: every bus transfer now carries additional encryption and authentication-tag overhead, and detecting a tampered transfer requires the receiver to recompute and compare the tag on every access, a cost production designs like AMD's and Intel's have judged worth paying given the alternative. Roots of trust and secure boot. The hardware root of trust, measured and secure boot, and the chain of trust.. Explain the hardware root of trust.. Distinguish measured boot from secure boot.. Implement a measurement extension and gate boot on it.. The hardware root of trust, Measured boot, Secure boot, The chain of trust Roots of trust and secure boot Every security argument has to stop somewhere: some component must be trusted without itself being verified by something else, or the reasoning regresses forever. This module studies that stopping point, the hardware root of trust, and the two complementary strategies (measuring and verifying) built on top of it during boot. The hardware root of trust A hardware root of trust is a small, trustworthy hardware component, immutable boot code, a protected key store, or a dedicated measurement register, that anchors the security of everything built above it. It must be small enough to analyse exhaustively, tamper-resistant against physical attack, and immutable or very strongly protected against modification, precisely because if the root itself is compromised, every guarantee resting on it is worthless: there is nothing further down to fall back on. This is why real roots of trust (the security opcode of Module 02 is exactly this kind of primitive) favour minimality over features. Measured boot Measured boot works by hashing each component, bootloader, firmware, kernel, into a protected measurement register before executing it, extending (folding new measurements into old, rather than overwriting) so the register accumulates an unforgeable record of everything that ran. A Trusted Platform Module (TPM) typically supplies these protected registers along with key storage and cryptographic primitives. Measured boot does not stop a compromised component from running; it records that it ran, so a later remote attestation can reveal the compromise even though the boot itself proceeded. Secure boot Secure boot takes the stronger stance: it verifies each component's cryptographic signature against a trusted key before running it, and refuses to execute anything that fails verification. Where measured boot produces an after-the-fact record, secure boot actively gates execution, at the cost of needing a signing and key-management infrastructure the platform can trust. The chain of trust The chain of trust is the discipline of each stage measuring or verifying the next before handing off control, so that trust extends outward from the root rather than being assumed everywhere at once; a break anywhere in the chain becomes detectable rather than silently propagating. Practically, this requires the measurement register itself to be extend-only, so a compromised later stage cannot rewrite history to hide itself, and it requires that measurements are eventually acted on: a policy that checks measurements or signatures and enforces a decision, not merely a log nobody reads. NIST Special Publication (SP) 800-193 addresses exactly this discipline for platform firmware: protecting, detecting corruption of, and recovering it, a direct real-world application of hardware-rooted trust. Related CCI capabilities Computer Architecture (Course): (https://www.cambridgecyberinternational.com/en/insights/academy/computer-architecture/). CCI Lab: Run it, build with it, read the thinking, reuse the data. (https://www.cambridgecyberinternational.com/en/insights/lab/) From TPM to UEFI Secure Boot The Trusted Computing Group published its Trusted Platform Module 1.2 specification in 2003, giving the industry a standardised, low-cost hardware root of trust capable of storing measurements in tamper-resistant platform configuration registers rather than in ordinary, attacker-modifiable memory. The Unified Extensible Firmware Interface (UEFI) consortium standardised Secure Boot as part of the UEFI 2.3.1 specification in 2011, giving firmware a standard mechanism to verify a cryptographic signature on each stage of the boot chain before executing it, which is the secure-boot half of the measured-boot-versus-secure-boot distinction this module draws. The two mechanisms answer different questions and are frequently confused: measured boot records what ran, extending a chain of hashes into the TPM's platform configuration registers so a later party can verify what actually executed, while secure boot prevents what runs, refusing to execute a stage whose signature does not verify against a trusted key. A platform can implement either, both, or, as this module's simulated gap illustrates, measured boot alone without ever checking the resulting measurements against a policy, which records an accurate history of a compromise without ever stopping it. NIST Special Publication 800-193, Platform Firmware Resiliency Guidelines, addresses exactly this discipline for platform firmware, organising the problem into protecting firmware from unauthorised change, detecting when protection has failed, and recovering to a known-good state, a direct, real-world elaboration of the chain-of-trust reasoning this module's lab exercises in miniature. Hardware attacks. Side channels, fault injection, and memory-disturbance effects, modelled in simulation, and the defences that close them.. Explain a side channel and how it leaks a secret.. Describe fault injection and memory-disturbance attacks.. Model an attack and observe the defence that closes it.. Side channels (timing and power), Fault injection, Memory-disturbance (Rowhammer), Speculative-execution side channels Hardware attacks Every mechanism built so far, the security opcode, the cipher datapath, bus protection, the root of trust, assumes the hardware behaves purely according to its logical specification. Real hardware also has a physical existence: it takes time, draws power, emits electromagnetic radiation, and shares physical resources like Dynamic Random-Access Memory (DRAM) rows. This module studies attacks that exploit that physical existence, modelled safely in simulation, and the defences that close each one. Side channels (timing and power) A side channel leaks a secret through a physical or timing observable that correlates with it, rather than through the intended output. A timing side channel arises when execution time depends on secret data, for example a comparison that returns as soon as a byte mismatches, letting an attacker infer how many leading bytes were correct from response time alone; the standard defence is constant-time implementation, whose timing never depends on the secret. Differential Power Analysis (Kocher, Jaffe and Jun, 1999) is the classic power-based instance: statistically analysing a device's power consumption across many operations recovers key bits that never appear in any output. Fault injection Fault-injection attacks (Boneh, DeMillo and Lipton, 1997) deliberately induce a computation error, via voltage glitches, clock glitches, or laser pulses, and exploit the resulting faulty output, which can leak far more about a secret key than a correct output would. The defence is to verify computations, for example by recomputing and comparing, so a faulted result is detected and never released rather than trusted. Memory-disturbance (Rowhammer) Rowhammer (Kim et al., 2014) flips bits in DRAM without ever addressing the flipped row directly: rapidly and repeatedly accessing (hammering) adjacent rows causes electrical disturbance that corrupts neighbouring cells. Defences include refreshing rows more often, error-correcting codes, and hardware counters that detect and mitigate hammering patterns before they cause a flip. Speculative-execution side channels Spectre (Kocher et al., 2019) exploits speculative execution: a performance optimisation where the core executes instructions ahead of knowing whether they should, based on a predicted branch outcome. Even when a misprediction is rolled back architecturally, the speculative access leaves a microarchitectural trace, commonly in the cache, that a subsequent timing side channel can read, leaking data that was never supposed to be architecturally visible at all. These attacks are studied here in a contained simulator specifically so you can recognise, model and defend against them, rather than to mount them on real devices: the pass condition throughout is demonstrating that a stated defence closes the modelled leak, visible directly in the signals or timing you observe. Related CCI capabilities Computer Architecture (Course): (https://www.cambridgecyberinternational.com/en/insights/academy/computer-architecture/). CCI Lab: Run it, build with it, read the thinking, reuse the data. (https://www.cambridgecyberinternational.com/en/insights/lab/) Landmark hardware attacks, briefly dated Differential power analysis, published by Paul Kocher, Joshua Jaffe and Benjamin Jun in 1999, showed that a cipher implementation's power-consumption trace over many operations could leak its secret key even when the algorithm itself was mathematically sound, establishing side-channel leakage as a hardware concern distinct from algorithmic correctness. Fault-injection attacks, formalised by Dan Boneh, Richard DeMillo and Richard Lipton in 1997, showed that deliberately inducing a hardware error, historically through voltage glitching or, in the Rowhammer line of research Yoongu Kim and colleagues published in 2014, through repeated DRAM row activation, could recover secrets or corrupt memory that no purely logical attack could reach. Spectre, published by Paul Kocher and a large multi-institution team in 2019 (with an earlier public disclosure in January 2018), and the closely related Meltdown attack published by Moritz Lipp and colleagues in 2018, showed that speculative execution, a performance optimisation present in essentially every modern high-performance processor, could be coerced into leaking data across privilege and isolation boundaries through cache-timing side effects, a class of hardware attack this course's earlier modules on secure boot and trusted execution both had to account for directly. These four attacks are taught together in this module because they span the range a hardware-security engineer needs to reason about: power and timing side channels leak information passively, fault injection actively corrupts state, and speculative-execution attacks exploit a performance feature that was never designed with security isolation in mind, and a defence adequate against one category, constant-time coding against timing leaks, say, does nothing against another, such as a voltage-glitching fault attack. Trusted execution and memory protection. Isolated execution environments, memory encryption and integrity, and their limits.. Explain a trusted execution environment.. Configure protection on a region so an ordinary access is denied.. Reason about the limits of hardware isolation.. Trusted execution environments, Memory encryption and integrity, Attestation, The limits of isolation Trusted execution and memory protection This module assembles several ANVIL mechanisms, the security opcode, the cipher datapath, bus and memory protection, into a single composite guarantee: a trusted execution environment (TEE), an isolated place to run code and hold data even when the rest of the system, including privileged software like the operating system, is untrusted or compromised. Trusted execution environments A TEE is a hardware-isolated environment where code and data are protected from the rest of the system. Isolation here is enforced by hardware access control: the memory management logic itself refuses ordinary, non-enclave accesses to enclave pages, so the guarantee does not depend on the operating system's cooperation or correctness. This is a stronger claim than software sandboxing, because even a fully privileged, malicious kernel is included among the parties the TEE excludes. Memory encryption and integrity Access control on its own does not resist a physical attacker who can probe or replay memory directly. TEEs therefore combine access control with memory encryption (so data at rest or in transit to Dynamic Random-Access Memory (DRAM) is unreadable outside the enclave) and memory integrity (so tampered or replayed encrypted memory is detected rather than silently accepted). Integrity is not optional: encryption alone still lets a physically-present attacker flip ciphertext bits or replay an old, validly encrypted block, producing an undetected, incorrect result inside the enclave. Attestation Attestation lets a TEE prove to a remote party exactly what code is loaded and running inside it, typically by producing a signed measurement rooted in the same hardware root-of-trust machinery studied in Module 05. This lets a remote party decide whether to trust the enclave, and release a secret to it, before any secret is sent, closing the loop between measurement and actual deployment decisions. The limits of isolation Hardware isolation reduces risk; it does not eliminate it. Real research demonstrates that TEEs can still leak through microarchitectural side channels, including the speculative-execution attacks studied in Module 06, despite architecturally correct isolation, because the isolation boundary was never designed to account for shared microarchitectural state like caches. The trusted computing base of a TEE should therefore be kept as small as possible, so it can actually be analysed, and code running inside an enclave still needs its own defences, constant-time implementation among them, rather than assuming the enclave boundary makes every internal leak irrelevant. The lab makes both halves concrete: an ordinary access to a protected region is denied by the hardware, demonstrating the guarantee, while the surrounding discussion keeps the limits equally honest. Related CCI capabilities Computer Architecture (Course): (https://www.cambridgecyberinternational.com/en/insights/academy/computer-architecture/). CCI Lab: Run it, build with it, read the thinking, reuse the data. (https://www.cambridgecyberinternational.com/en/insights/lab/) Trusted execution environments in production hardware Advanced Reduced Instruction Set Computer (RISC) Machines (ARM) introduced TrustZone in 2004 as a set of hardware extensions that partition a processor into a "normal world" running the main operating system and a "secure world" running trusted code, with hardware-enforced boundaries preventing the normal world from reading secure-world memory even with full kernel privileges. Intel's Software Guard Extensions (SGX), introduced in 2015, took a different architectural approach, carving out enclaves within an otherwise normal process's address space rather than partitioning the whole system, but the underlying guarantee, that an operating system compromise should not automatically expose the isolated region's secrets, is the same one this module's lab demonstrates by denying an ordinary access to a protected region. Both TrustZone and SGX also illustrate this module's second theme, the limits of hardware isolation, directly: speculative-execution research following the Spectre disclosures (Kocher et al., 2019) showed that even code running inside a hardware-isolated enclave can leak secrets through a shared microarchitectural side channel, such as a cache-timing pattern, that the isolation boundary was never designed to close, since the boundary protects architectural state, not every observable timing effect of executing on shared hardware. This is why a trusted execution environment's guarantees are best stated precisely rather than absolutely: isolation denies an ordinary memory access, as this module's lab confirms directly, but it does not by itself guarantee constant-time execution, and code written to run inside an enclave without that discipline can still leak through the channels isolation was never designed to close. Specifying and verifying a hardware security property. Stating a security property over the simulated hardware and model-checking it, connecting ANVIL to AXIOM.. State a security property over simulated hardware.. Verify it with the model checker.. Read a counterexample waveform when it fails.. Properties over hardware, The model checker, Verifying the property, Reading a counterexample Specifying and verifying a hardware security property Every mechanism built across ANVIL so far, the security opcode, bus tagging, the measurement register, enclave isolation, has been checked by observation: single-stepping, reading waveforms, running known-answer vectors. This module raises the bar from observing correct behaviour on chosen inputs to proving a property holds across every reachable state of the simulated design, using the same model-checking core taught in AXIOM (Formal Methods). Properties over hardware A hardware security property is a precise statement that must hold over the design's behaviour, for example 'a non-enclave access never reads enclave memory' or 'the measurement register is extend-only'. Precision is not optional: a vague property cannot be checked, because a model checker needs an exact statement over the design's actual signals and states, not an informal description of intent. The model checker Model-checking a hardware property means exhaustively exploring the simulated design's reachable states (not sampling some of them, as testing does) and confirming the property holds in every one, or producing a concrete counterexample the moment it finds a state where the property fails. This is the same checking discipline AXIOM applies to protocols and algorithms; here the model being checked is the hardware design itself, so a verified property is a claim about the artefact closest to what would actually be fabricated, narrowing, though never fully closing, the gap between model and implementation. Verifying the property Verifying the property means running the checker over the design as specified and interpreting its result. If the checker returns no counterexample within the modelled bounds, the property holds over the simulated design within those bounds: a real, but explicitly bounded, form of assurance, not a claim about every physical chip that could ever be fabricated from the design. This distinction between 'checked' and 'true forever, unconditionally' is essential to state honestly. Reading a counterexample When the checker fails the property, it returns a counterexample: a concrete execution, rendered here as a waveform, that violates the property and shows exactly how, down to the cycle and the signals involved. This is far more actionable than a bare pass/fail result, because it localises the fault directly rather than requiring you to search for it. A property that is genuinely true of the design but not provable as stated often needs strengthening with auxiliary conditions until it becomes inductive, the same technique AXIOM teaches, after which it is re-checked. A speculative read appearing in a counterexample for 'enclave memory is never read externally', for instance, is not a checker error: it is the property doing its job by exposing a real microarchitectural leak that needs fixing. Related CCI capabilities Computer Architecture (Course): (https://www.cambridgecyberinternational.com/en/insights/academy/computer-architecture/). CCI Lab: Run it, build with it, read the thinking, reuse the data. (https://www.cambridgecyberinternational.com/en/insights/lab/) Model checking as a verification discipline Symbolic model checking, the technique this module's checker applies, traces to Kenneth McMillan's 1992 Symbolic Model Verifier (SMV) model checker, developed at Carnegie Mellon University, which showed that a finite-state hardware design's properties could be verified exhaustively against every reachable state rather than only against the specific test vectors an engineer thought to write. This distinction, exhaustive verification against a stated property versus testing against a finite sample of inputs, is exactly why this module frames model checking as a complement to, not a replacement for, the known-answer testing Module 03 practised. A model checker that returns no counterexample within the bounds it explored licenses a bounded claim, not an unconditional one: the property held for every state the checker actually reached, which is a strong result but not automatically a proof about states outside the modelled bounds, an honesty this module insists on carrying into how a result is reported. When a counterexample is returned, the waveform it produces is not a failure message alone; it is a concrete, reproducible trace showing exactly which sequence of inputs drives the design into the state that violates the stated property, which is what makes a counterexample far more actionable than a test suite's simple pass or fail result. The seL4 microkernel's formal verification, published by Klein et al. in 2009, remains the field's clearest demonstration that this discipline scales beyond toy examples: seL4's functional correctness was proved down to the executable binary, not merely the source design, which is the same precise-specification-first discipline this module's lab exercises in miniature against a single stated hardware security property. Capstone: implement and verify a security property in silicon. Implement a stated security property in the simulated hardware and prove it with the checker, then defend the result.. Implement a stated security property in simulated hardware.. Verify it with the model checker.. Explain and defend the verified result and its scope.. Scoping the property, Implementing it in hardware, Verifying it, Defending the result Capstone: implement and verify a security property in silicon The capstone draws on every layer of this course: the datapath and Instruction Set Architecture (ISA) understanding of Modules 00 to 02, a hardware security mechanism from Modules 03 to 07, and the specification and verification discipline of Module 08, requiring you to implement a stated security property in the simulated hardware and then prove, not merely claim, that it holds using the model checker. Scoping the property Scoping well means stating the property precisely over the design's actual signals and states, not vaguely, so it is checkable at all; you must choose a property whose truth genuinely depends on the mechanism you intend to build, such as an access check, an integrity tag, or an extend-only register, rather than one that is trivially true or unrelated to your implementation. A well-scoped property is also honest about its boundary: what part of the design it covers, and what it deliberately leaves out. Implementing it in hardware Implementing the property is not documentation; it means adding or wiring the actual hardware that enforces it, an access-control check gating a memory region, a Message Authentication Code (MAC)-based integrity tag on a bus transfer, or a measurement register wired to extend rather than overwrite, using the same datapath and control-signal techniques used to add the security opcode in Module 02. The mechanism must be built into the datapath, not asserted in prose alongside it. Verifying it Once implemented, the property must actually be run through the model checker over the simulated design. The capstone's pass condition is specifically that the stated property holds under the checker (or that a returned counterexample is correctly read and resolved by fixing the design and re-verifying), not a good write-up, a fast clock, or a long manual. A capstone that implements the mechanism convincingly but never runs the checker has not met the proof-of-work requirement: an assertion of security is not the same as a verified one. Defending the result Defending the result means stating its scope honestly: the property holds over the simulated model within the bounds the checker actually explored, not on every chip ever fabricated forever, and a passing check does not rule out effects outside the model, an unmodelled side channel, a fabrication defect, or an attack class the property was never scoped to cover. This connects directly back to AXIOM: hardware verification is not decorative or software-only, it is applicable to concrete designs precisely because the verified model here is very close to the artefact that would be built, but the residual model-to-implementation gap, and any unmodelled attacks, must be named rather than hidden behind a claim of 'unbreakable' security. Related CCI capabilities Computer Architecture (Course): (https://www.cambridgecyberinternational.com/en/insights/academy/computer-architecture/). CCI Lab: Run it, build with it, read the thinking, reuse the data. (https://www.cambridgecyberinternational.com/en/insights/lab/) Verified security properties beyond the classroom The Capability Hardware Enhanced Reduced Instruction Set Computer (RISC) Instructions (CHERI) project, first published by Robert Watson and collaborators at the University of Cambridge in 2014, extended a conventional instruction set with hardware-enforced memory capabilities, showing that a precisely scoped hardware security property, in CHERI's case, memory-safety guarantees enforced by the datapath itself rather than by software convention, can be specified, implemented and verified using exactly the discipline this capstone exercises: state the property precisely, implement it in the datapath, and prove rather than merely assert that it holds. The seL4 microkernel's 2009 formal verification remains the field's benchmark for what "prove, not merely claim" looks like in practice, since seL4's authors verified functional correctness all the way down to the compiled binary rather than stopping at the design specification. Both precedents share this capstone's central discipline: a property that is true of a design but stated too loosely to be checked automatically is not yet a verified property, and scoping a property precisely, naming exactly the states and transitions it must hold over, is usually harder than implementing the mechanism that satisfies it. A capstone that implements the mechanism correctly but never runs the checker against it has completed half the exercise; the honest phrasing this module insists on, that a passing check rules out every counterexample the checker's bounded search actually explored rather than ruling out every conceivable attack, is the same caveat CHERI's and seL4's own published results are careful to state. Connecting explicitly back to AXIOM, verification in the sense this capstone and its two precedents share is not a synonym for confidence; it is a specific, falsifiable claim about a specific, precisely stated property, checked against a specific, bounded model, and any claim stronger than that, unbreakable hardware security, chief among them, is precisely the kind of overclaim this course has trained you to recognise and rephrase.