How to read a PL-security paper
summary
Provides a concrete checklist: verify the threat model (who the attacker is, where they sit, what they can observe), insist on a clear, semantic policy and whether it’s a hyperproperty, and check the policy–mechanism–assurance separation and actual proofs or tools. Gives concrete examples: timing attacks become practical in cloud racks, a DNA sequencer can trigger a buffer overflow, and a scheduler batching bug in a toy language "troop" flips observable outputs — found with property‑based testing. Emphasizes the security/expressivity/performance tradeoffs.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:41Understanding threat models
- 6:13Evaluating security papers
- 12:40Subtleties in security models
- 16:08Policy, mechanism, assurance
- 21:54Design principles
- 25:47Privacy vs. security
- 29:26Practical implementation bugs
- 34:49Conclusion and takeaways
related talks
49mPragmatic Approaches To Building Secure Software
27mSecurity: The Thing That Everyone...
43mThreat modeling
44mSecurity Lessons for Early Adopters
17mPreview: Security and Privacy
50mSecure and Privacy by Design Converge with Threat Modeling
57mWhat Could Possibly Go Wrong? Plain Language Threat Modeling in DevSecOps
57mShift Left Security with the Security Test Pyramid