Lightweight Runtime Security Policy Verification Using an Embeddable C++ miniKanren
summary
An embeddable C++ miniKanren implements relational search with a small virtual-machine queue, bump-allocation arenas and rational-term unification (no occurs check), targeting constrained devices. The implementation fits in a 64 KiB stack-allocated arena with no heap, runs access-control queries at median 17.0 µs and network-policy queries at 3.6 µs, and produces structured, explainable violation reports. Two case studies—ACL enforcement and IoT network policy verification—are built and evaluated, showing fast on-device verification and audit-ready rule-level violation traces.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 3:37Cybersecurity student collaboration
- 8:38Security policy verification
- 10:07C++ implementation details
- 13:25Architecture and parsing
- 17:16Memory game case study
- 22:59Performance goals and benchmarking
- 26:10Memory management
- 29:03Future directions and Q&A
related talks
46mVerifying code using automated reasoning
24mRuntime Security: Challenges & Solution Space
53mLightweight Resource Leak Verification and Inference
16mAgora: Trust Less and Open More in Verification for Confidential Computing
28mLightweight Hypervisor Verification: Putting the Hardware Burger on a Diet
28mAgent Runtime Security: Enforce, Attest, Decide
14mStateful Behavior Inference and Runtime Enforcement for Vehicle Network Security
30mFinding Imposter Among Us: Container Edition