STORM: Refinement Types for Secure Web Applications
Talkat 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI '21) · 2021-07-14..07-16·
summary
Storm is a web framework that enforces data-dependent security policies at compile time via a Security Typed ORM that refines MVC types with logical assertions. It uses Liquid Haskell for decidable refinements and a formally verified reference of the enforcement using LIO IFC. Evaluation builds two end-to-end apps (Disco, Voltron), shows trusted code under 1% of the server, annotation burden about one line per 19 LOC, and reports static enforcement with no runtime overhead.
AI-written summary · about
chapters (11)
- 0:00Start
- 0:29Security checks mixed into business logic
- 1:33Existing IFC Frameworks
- 1:55Our solution: STORM
- 7:36Compositional IFC
- 8:28Sets as Predicates
- 11:20Expressiveness
- 12:04Typing Annotations
- 12:28Evaluation
- 13:54Disco and Voltron Architecture
- 14:04Auditability
related talks
38mBuilding Secure Systems in Haskell
01h 04mThe Storm and the Compass [KEYNOTE]
54mSecuring Software by Construction
36mQuickstrom: Specifying and Testing Web Applications
46mSecure Web Applications with Clojure
50mSecure and Privacy by Design Converge with Threat Modeling
40mTempesta FW: FrameWork and FireWall for WAF and DDoS mitigation
40mTempesta FW: FrameWork and FireWall for WAF and DDoS Mitigation