Modularizing Reasoning about AI Capabilities via Abstract Dijkstra Monads
summary
Position proposes a Bastion OS design that uses Dijkstra monads and secIO in F to enforce capability-based, provable constraints on agent actions. Concrete examples include an AI that silently deletes files when asked to “filter” endangered-species data and an AI that edits timeouts; small F* case studies implement an Mio effect that records syscall traces and proves code only opens listed files and does not delete them. Sandboxing alone proves too coarse. Runtime eBPF-style enforcement is suggested.
AI-written summary · about
chapters (10)
- 0:00Agentic AI introduction and risks
- 3:13Agentic AI systems examples
- 8:09Sandboxing insufficient for safety
- 10:56Capability-based AI security
- 16:13Modular reasoning with capability-safe languages
- 18:40Provably safe AI agent architecture
- 21:12Policies for environmental AI tasks
- 24:42F* implementation case studies
- 28:33Future directions for runtime enforcement
- 30:00Q&A
related talks
50mFrom Prompt Hacking to Architectural Determinism: Engineering Reliable GenAI Systems
23mSecurity Reasoning via Substructural Dependency Tracking
21mDemystifying AI Agents: A New Primitive for Flow Control
34mZero Secrets: Building Secure Infrastructure for AI Agents
56mWhen Unstoppable Frontier Agents Meet Immovable Attack Vectors
30mWhy Prompt-Level Guardrails Fail for AI Agents
32mDLGI: Before Things Go Too Far
26mGating Cognition: How Modern AI Architectures Minimize Runtime Reasoning