Security & Privacy

Phase 9 asked whether a system behaves correctly under normal operation, using formal methods to pin down precise specifications and check designs against them. This phase asks the harder version of that question: does the system stay correct when an adversary is deliberately trying to break it? Lee and Seshia’s chapter on security and privacy makes the case that embedded and cyber-physical systems face this question with unusual urgency, since the same physical processes those systems control (medical devices, vehicles, traffic infrastructure) turn a software bug into a safety incident the moment someone exploits it on purpose.

Threat Models and the Four Core Properties

The chapter opens with a blunt framing point worth internalizing before any cryptography: security is never absolute. Any security claim only means something relative to a specific threat model, that is, what capabilities and access the attacker is assumed to have, and a specific set of properties being defended. “Completely secure” is a red flag phrase, not a real claim, and it’s the security-domain analog of Phase 9‘s insistence on precise formal specification: an informal, unstated threat model is exactly as dangerous as an informal, ambiguous requirement.

Four properties are worth keeping distinct, since different attacks and defenses target them differently. Confidentiality means secret data stays secret from the attacker; integrity means data isn’t modified by the attacker; authenticity means you actually know who you’re talking to; availability means the system keeps working despite the attacker, with denial-of-service being the canonical availability attack. A given defense mechanism often protects only one or two of these: encryption alone gives confidentiality but not integrity or authenticity, which is exactly why MACs and digital signatures exist as separate primitives.

Cryptographic Primitives

Symmetric-key cryptography starts from one shared secret key that both parties know. The one-time pad, which XORs the plaintext with a truly random, single-use key, is information-theoretically perfect: Lee and Seshia prove this cleanly by showing that every ciphertext is equally consistent with every possible plaintext under some key, so an observer with no key knowledge learns nothing at all.

$$C = M \oplus K, \qquad M = C \oplus K$$

That perfection has a strict condition attached, though: the key can never be reused. Reusing it leaks the XOR of the two plaintexts through the XOR of the two ciphertexts, an immediate consequence of XOR’s algebra:

$$\text{if } K \text{ reused: } C_1 \oplus C_2 = (M_1\oplus K) \oplus (M_2 \oplus K) = M_1 \oplus M_2$$

Real systems trade that perfect secrecy for practical reusability by using block ciphers instead of true one-time pads: DES historically, and now AES, the modern standard, which operates on 128-bit blocks with 128, 192, or 256-bit keys and is currently considered infeasible to brute-force even at supercomputer scale.

Kerckhoffs’s principle is worth internalizing as a design discipline rather than filing away as a historical footnote: a cryptosystem must remain secure even if everything except the key is public knowledge. Security through obscurity, hiding the algorithm itself, is not real security; only the key’s secrecy should matter. It’s the crypto-specific instance of a broader lesson that recurs across this whole series: never design a system whose safety depends on an attacker’s ignorance of how it works.

Public-key, or asymmetric, cryptography solves symmetric crypto’s bootstrapping problem: how do you share a key in the first place, if the channel itself isn’t secure? A public/private key pair does it: encrypt with the public key, and only the matching private key decrypts. RSA’s security rests on the practical difficulty of factoring the product of two large primes:

$$n = pq,\quad ed \equiv 1 \pmod{\varphi(n)}, \qquad C = M^e \bmod n, \qquad M = C^d \bmod n$$

where $(n,e)$ is the public key, $d$ is the private key, and $\varphi(n)=(p-1)(q-1)$ is Euler’s totient of the product of the two large primes $p$ and $q$. The encryption function here is a genuine one-way function: easy to compute, computationally infeasible to invert without the private key. It’s also expensive, since public-key operations mean modular exponentiation on large numbers, which is exactly why embedded systems mostly use it only to bootstrap a symmetric session key and then switch to cheap symmetric crypto for the actual data, a pattern reused everywhere from TLS down to embedded protocols.

Confidentiality, integrity, and authenticity need mechanism-by-mechanism separation, because encryption alone only buys the first. Secure hash functions map an arbitrary-length message to a fixed-length digest, and three properties, pre-image resistance, second-pre-image resistance, and collision resistance, make forgery computationally infeasible, which is what gives you integrity-checking. Digital signatures (sign with your private key, anyone verifies with your public key) give authenticity and integrity together, but naive signing has real, non-obvious flaws. Lee and Seshia’s example: RSA signatures on a raw message are multiplicatively forgeable, since $S_1 \cdot S_2 \pmod n$ is a valid signature for $M_1 \cdot M_2$, which is exactly why you sign a message’s hash rather than the message itself. MACs are the symmetric-key analog of signatures, using a shared key rather than a key pair, and are a good fit for closed systems with pre-shared keys, like ECUs communicating over an automotive CAN bus.

Protocol and Network Security

Diffie-Hellman key exchange lets two parties agree on a shared secret purely by exchanging public values over a channel a passive eavesdropper can fully observe:

$$A = z^a \bmod p,\quad B = z^b \bmod p \qquad \Rightarrow \qquad K = B^a \bmod p = A^b \bmod p = z^{ab}\bmod p$$

with $a$ and $b$ kept secret; an eavesdropper who sees only $p$, $z$, $A$, and $B$ cannot feasibly recover $a$, $b$, or $K$. The security rests on the discrete logarithm problem (computing $x$ from $z^x \bmod p$ is hard) being a one-way function, mirroring RSA’s factoring-hardness assumption. It’s elegant, but the large-prime modular exponentiation involved is often too expensive for energy- and real-time-constrained embedded platforms, which motivates cheaper, embedded-specific alternatives.

Timed release of keys, as in the μTESLA protocol, is one such alternative, and a clever one: it trades a hard cryptography problem for a timing and synchronization problem instead. The sender attaches a MAC computed with a not-yet-revealed key, then broadcasts the key later on a fixed schedule; receivers with synchronized clocks can verify that a received MAC’s key genuinely hadn’t been disclosed yet, proving the message is fresh rather than a replay, then validate it once the key is published. It’s a nice example of an embedded system’s native strength, precise timing achievable via GPS or PTP, being turned into a security asset rather than just a real-time-correctness one.

Protocol-level bugs can break otherwise-perfect cryptography, and Lee and Seshia’s replay-attack example is the cleanest illustration in the whole chapter. Every individual cryptographic step can be sound, yet an attacker who simply records and rebroadcasts an old encrypted message can drain a sensor node’s battery, a denial-of-service attack, purely because the protocol had no way to detect that a message wasn’t fresh. The fix, a nonce or timestamp attached to each message, is cheap, but the lesson is expensive to relearn if missed: security is a property of the whole protocol’s behavior over time, not just of the cryptographic primitives used inside it. That’s the same lesson Phase 6 draws about scheduling: correct components can still compose into an incorrect system, whether that shows up as a deadlock or as a replay vulnerability. It also underscores why the network channels covered back in Phase 8 deserve to be treated as an attack surface from the outset, not an afterthought once the protocol already works.

Reverse-engineering real deployed systems keeps surfacing the same root cause. Lee and Seshia cite published attacks on implantable medical devices, automotive OBD-II and CAN networks, and traffic light controllers, and in each case the vulnerability existed because security wasn’t a first-order design concern when the system was originally built, not because the underlying cryptography was broken. It’s a blunt, well-supported argument for treating security as a requirement from the very start of a design, not a bolt-on applied after the fact.

Software Security: Buffer Overflows

Buffer overflow is the chapter’s deep-dive example, and it’s worth understanding structurally rather than dismissing as just another C bug. C performs no automatic bounds-checking on array or pointer access, so writing past the end of an array silently corrupts whatever memory happens to sit next to it. Lee and Seshia’s worked examples make this concrete in two ways: a global secret_key variable declared right after a fixed-size buffer, where an attacker-controlled overflow overwrites the key directly, and a stack-allocated buffer whose overflow can overwrite the function’s own return address, known as stack smashing, redirecting execution to attacker-chosen code. That second case, a code injection attack, is the most severe outcome, since it can hand the attacker arbitrary control over the program.

This bites embedded systems specifically harder than general-purpose software, because embedded C code often runs bare metal with no OS-level memory protection or bounds-checking layer to catch the error before it does damage. That connects directly back to Phase 3‘s memory-protection-unit material: an MPU or MMU is one of the few hardware backstops against exactly this class of bug, and its absence, common on cost- and power-constrained microcontrollers, removes that backstop entirely. Defenses exist on both ends of the spectrum: explicit bounds checks are cheap and easy but have to be applied consistently everywhere, which makes this a discipline problem rather than a technical one, while memory-safe higher-level languages make the whole bug class structurally impossible rather than relying on programmer discipline to catch every instance.

Secure Information Flow

Secure information flow reframes the whole question from “is this encrypted” to “where is data allowed to go.” Confidentiality means secret data must never flow to an attacker-readable channel; integrity means untrusted, attacker-controlled data must never flow to a trusted channel unchecked. Lee and Seshia’s glucose-meter example works through this as a clean progressive case. A first version leaks the reading in the clear, an illegal information flow from a secret variable straight to a public network channel. A second version encrypts the reading using a declassifier, a function that legitimately launders secret data into a form safe to release, but still leaks the patient ID unencrypted: metadata leakage that’s easy to overlook when you’re focused on the “obviously sensitive” value. A third version adds a password check but leaks one bit, whether the password was right or wrong. That leak is acceptable, given the exponential cost of brute-forcing it, and it’s the chapter’s concrete instance of quantitative information flow: not all leaks are equally bad, and sometimes a small, bounded leak is a legitimate engineering trade-off rather than a bug to eliminate at any cost.

Formalizing “the attacker’s observable view doesn’t depend on the secret” turns out to require comparing multiple execution traces at once: does the low, public part of the trace stay identical across different high, secret inputs? That’s provably not expressible as an ordinary single-trace property; the LTL machinery from Phase 9 can’t state it, which is exactly why it needs the more general notion of a hyperproperty, a property of sets of traces rather than of one trace at a time. Non-interference is a genuine example of a real, practically important property class that sits outside the verification machinery covered in Phase 9, and it needs genuinely different tools, namely relational verification, rather than just a more complicated LTL formula.

Taint analysis, labeling data as it flows through the program, either statically or at runtime, and flagging illegal flows, is the practical, if imprecise, engineering tool for catching confidentiality and integrity violations like the glucose-meter example. It’s cheaper and easier to apply than full formal verification of non-interference, at the cost of false alarms in the static case or runtime overhead in the dynamic one.

Sensor Attacks and Side Channels

Some of the most distinctly cyber-physical attacks in the chapter never touch the digital system at all. Real, published attacks spoof or disrupt analog sensor readings, implantable cardiac devices and automotive wheel-speed sensors among them, purely through electromagnetic interference, exploiting the analog physical layer itself, below where any software-level defense can even see the problem. This has no analog in traditional, non-embedded software security: the attacker is exploiting the sensor’s role as the boundary between the physical and cyber worlds covered in Phase 4, not a software bug.

Side-channel attacks are the other broad category, and they leak information through a physical channel the system designer never intended as a communication channel at all: timing, power draw, memory access patterns, acoustic emissions, even fault-injection behavior. Lee and Seshia’s own modular exponentiation timing attack is a genuinely striking, full-circle example, because it reuses the exact modexp function from the WCET running example covered under Phase 9. It shows empirically that execution time clusters by the number of 1-bits in the secret exponent, leaking key information purely from timing measurements.

That means a WCET-style timing measurement, the very quantity that earlier verification work teaches you to analyze for real-time correctness, can also leak a cryptographic key: the same execution-time analysis is a correctness tool in one context and an attack tool in another. Differential power analysis and cache-timing attacks (Tromer et al.’s real break of AES, achieved by inducing and measuring cache hits and misses from a co-resident process) extend the same principle to other physical and microarchitectural side channels, directly reusing the cache-conflict mechanics from Phase 3, now as an attack primitive rather than a performance concern.

The chapter’s closing lesson is worth carrying forward as the single most important idea from this whole phase: security compromises are often achieved by breaking assumptions made by system designers. Nearly every attack surveyed here, replay attacks, buffer overflows, EMI spoofing, timing side-channels, succeeds not by defeating strong cryptography head-on, but by exploiting something the designer never thought to model as part of the threat surface at all.

Where This Leaves Us

This phase extends Phase 9‘s “does it behave correctly” question into “does it stay correct under a deliberately adversarial environment,” and the chapter’s framing, that no security claim means anything without a precise threat model and a precise property, whether confidentiality, integrity, authenticity, or availability, is the load-bearing idea underneath everything else. Cryptographic primitives (symmetric one-time-pad and block-cipher encryption, RSA public-key crypto, secure hashes, digital signatures, MACs, Diffie-Hellman key exchange) supply the mathematical building blocks, but the recurring lesson is that these primitives are necessary and nowhere near sufficient. Every real breach surveyed here, a replay attack that drains a sensor’s battery despite flawless encryption, buffer overflows enabling stack-smashing code injection, EMI attacks spoofing analog sensors below the software layer entirely, a timing side-channel leaking a secret key from the exact WCET example used earlier in the series, succeeds by exploiting an assumption the designer never thought to defend, not by breaking cryptography head-on. Secure information flow supplies the formal vocabulary for reasoning about where sensitive data is allowed to go, and shows that this reasoning genuinely needs new machinery, hyperproperties, beyond the single-trace tools built up in Phase 9.

With security’s adversarial lens now added to verification’s correctness lens, the series turns to its final phase. Phase 11, the last in the series, pulls modeling, processors, software, scheduling, networking, verification, and security back together into a single design methodology, asking how a real embedded system gets built, and validated, end to end.