A Case Study in Language-Based Security: Building an I/O Library for Wyvern
summary
Builds a small standard I/O library for Wyvern that combines object capabilities, an effect system, and language extensions to reduce misuse. Demonstrates runtime capability enforcement that prevents an untrusted module from opening a password file, compile-time effect checks that reject a save that unexpectedly gains a network effect, and read‑only wrapper patterns for fine-grained least‑privilege. Implements a bounded‑abstract‑effects mechanism motivated by the case study and uses typed format‑string extensions to eliminate format‑string injection; the prototypes compile and catch the shown failures.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 3:12Case study goals and Wyvern
- 7:25Capability-based security
- 10:15Live demo: capability enforcement
- 12:00Building with capabilities
- 15:07Effect systems for I/O
- 17:16Demo: effect change detection
- 19:44Bounded abstract effects
- 20:47Language extensions for injection
- 23:15Demo: safe format strings
- 24:37Key takeaways
- 25:19Q&A
related talks
16mA Case Study in Language-Based Security: Building an I/O Library for Wyvern
01h 02mT1: Secure Programming For Embedded Systems
49mBreaching LLM-Powered Applications: Overcoming Security and Privacy Challenges
13mOwlC: Compiling Security Protocols to Verified, Secure...
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice
38mBuilding Secure Systems in Haskell
50mSecuring LLM-Powered Applications: Overcoming Security and Privacy Challenges
01h 06mSecurity Beyond Memory Safety - Using Modern C++ to Avoid Vulnerabilities by Design