Automated Learning and Verification of Embedded Security Architectures
summary
Proposes reducing the model/implementation gap by extracting concrete behavioral models with automata learning and checking preservation of robust non‑interference (PRNI) with model checking. The pipeline learns DFA‑style enclave models from black/gray‑box tests, produces witness graphs as counterexamples, and reproduces the published sankos attacks (finds B1,B3–B7; B2 and B5 need extra work). The learned models mirror patched commits, enabling regression tests, but learning time and model size limit scaling to full ISAs.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 2:28Formal models vs implementations
- 7:07Top-down vs bottom-up modeling
- 8:55Automata learning for modeling
- 12:28Attacker and victim specs
- 16:59Testing real security architecture
- 19:51Results and future work
- 20:56Q&A
related talks
01h 08mProviding evidence for the security properties of hardware/software codesigns
45mAutomated Verification meets Differential Privacy
33mApplicable and Achievable Formal Verification
12mLeakage models are a leaky abstraction (...)
47mHarnessing LLMs for Next-Level Security Analysis
14mStateful Behavior Inference and Runtime Enforcement for Vehicle Network Security
20mNegative/Positive Verification for WorldGuard, CHERI and Other RISC-V Security Models-
28mProving Memory Access Violations in Isabelle/HOL