Skip to main content

Security Architecture and Lightweight Formal Reasoning

Competency Contract​

  • Primary competency: SE-ENGINEERING-001
  • Mastery: explain, apply, develop, and evaluate as required by the semester assessment
  • Status: required evidence extension; budgeted at 35–45 hours in the reconciled semester workload

Required Work​

Add architectural threat modelling and privacy design; state invariants and state transitions; use a lightweight specification or model-based test; automate a security fitness function.

Evidence Contract​

  • trust-boundary diagram
  • privacy ADR
  • invariant/state model
  • model-based test
  • security fitness-function result.

Assessment Integration​

  • Project: produce the evidence in the semester repository rather than as detached prose.
  • Checkpoint: show the evidence exists and identify its highest-risk gap.
  • Cumulative review: connect the work to current, previous, and two-semesters-back knowledge.
  • Exam: evaluate a new case and reject an attractive but unsafe or unsupported alternative.
  • Rubric: every required evidence category must pass; strengths cannot average away a missing category.
  • Answer key: calibrate the shape of evidence without prescribing one implementation.

Oral Defense​

Defend one invariant violation, one rejected architecture, and how the automated check prevents regression.

AI-Use Declaration​

Record tools and models used, material output accepted, rejected suggestions, and independent verification. Undeclared generated evidence fails the integrity gate.

Reading Route​

Start with the linked semester concepts and labs. Use local books selectively for conceptual depth and current official standards for normative requirements. Stop reading when you can produce and defend the required evidence.

Operational work and evidence: S1–S5​

Use the same synthetic two-tenant reservation/document service as the semester project. Include an API, an authorization decision, a cache or projection, persistent state and a worker. Preserve the original five evidence categories; each independently requires level 2 under the progression contract.

S1 — Trust-boundary diagram and threat scenarios (6–8 hours)​

Draw caller, API, authorization component, cache, database, worker and external partner. Mark data flows, principals, credential propagation, owners and where trust changes. A network line is not automatically a trust boundary, and two components in one process can have different authority.

For at least five concrete scenarios, record asset, actor capability, entry point, violated property and detection/mitigation evidence. Include a valid user reading another tenant's record, a revoked user reading a warmed cache, a worker receiving a stale message, an unavailable authorization dependency and an overprivileged diagnostic path. State assumptions rather than asserting that “internal” traffic is trusted. Rank by plausible impact and evidence; do not invent probability precision.

S2 — Privacy ADR with observable consequences (6–8 hours)​

Inventory identifiers and derived data across storage, caches, logs, exports and backups. Record purpose, access, retention and deletion/completion meaning. Write a privacy ADR comparing three viable ways to meet the same need while collecting or retaining less data. Name residual exposure and who owns it.

Use synthetic records to demonstrate one denied access and one retention/deletion path, including cached copies and restore behavior inherited from Semester 06. Distinguish logical unavailability from physical media erasure. Do not claim legal compliance from this exercise. An audit log needed for deletion/replay protection can itself contain identifiers; justify minimal retained metadata and access controls.

S3 — Explicit invariant and state model (7–9 hours)​

Define a bounded model with two tenants, two principals, two records, a permission revision and a cache that can contain stale entries. Include grant, revoke, read, warm-cache, delete and dependency-unavailable transitions. Define the linearization/observation boundary of each operation: the required property concerns reads beginning after revocation/deletion completion; concurrent in-flight reads need a separately declared policy.

Invariant: every successful read belongs to the requesting tenant, is authorized at the promised policy boundary and does not expose a record whose deletion completed before that read began. Model the principal/tenant identity as authenticated input, not a caller-controlled label assumed trustworthy. If the model assumes authentication correctness, record that abstraction explicitly.

Specify what happens when current policy cannot be obtained. For this exercise, deny or return an unavailable outcome rather than serve content under an unverified permission. This is a chosen confidentiality requirement, not a universal availability policy. Separate content absence from authorization denial in internal evidence without leaking record existence through public errors.

S4 — Model-based test and implementation comparison (8–10 hours)​

Enumerate bounded action sequences to a declared depth or use a seeded state-machine generator; publish state/action counts, seed, bounds and omitted behaviors. Inject a cache-only authorization defect. Preserve the shortest failing trace you can minimize: grant, warm, revoke, read is a starting candidate. Add tenant confusion and delete/replay traces.

Repair the transition model, then replay equivalent requests against the implemented service. Maintain a mapping from abstract actions to actual endpoint/state observations. Model success alone does not establish implementation conformance. Keep both traces and explain any mismatch. Test dependency-unavailable behavior explicitly. Finite exploration is evidence within declared bounds, not proof for arbitrary concurrency or every deployment.

S5 — Security fitness function with failure evidence (8–10 hours)​

Automate a service-level regression for at least cross-tenant reads, revoked access, deleted cached data and unavailable authorization. Include positive authorized reads so an implementation that denies everything cannot pass. Keep synthetic credentials/data local. Fail visibly on unavailable test setup or missing observations; a skipped collector is not a successful security check.

Run the deliberately unsafe variant and retain its failure, then run the repaired variant. Identify the owner, response to failure, environment and revision. Add one source-boundary or least-privilege configuration check where it supports the architecture; explain why it cannot replace runtime authorization tests. Reopen evidence when identity propagation, cache serialization, policy semantics or deployment boundaries change.

Calibration and defense​

A cache keyed by tenant and record can still return data to a revoked principal. Key separation is not complete authorization. A denial-only implementation satisfies a narrow “no unauthorized success” assertion but violates the required legitimate-read behavior. A successful direct database deletion test leaves warmed caches untested. A model that omits revocation cannot support a claim about revocation safety.

Every S category uses 0 absent/incorrect, 1 prompted/incomplete, 2 independent correct evidence with limits, 3 fresh transfer. In defense, change the policy revision or introduce an unavailable dependency; explain which claim survives and which test must change. Record reviewer feedback and AI assistance. No author reference-harness execution should be presented as your own service security test.

Selective source reinforcement​

Use OWASP's Threat Modeling Cheat Sheet to structure system/threat/mitigation/review questions, then revise one scenario and its evidence. Reuse the semester's primary books for architecture tradeoffs and prior semester privacy/replay lessons. Additional tools and paid books are optional; the core work is explicit properties and reproducible service evidence.