Haskell Library for Safer Virtual Machine Introspection (Experience Report)
summary
HaVMI is a Haskell library that wraps LibVMI and uses Template Haskell meta-functions like generate_struct to emit concrete Haskell types, accessors and instance declarations that collapse the typical five-line C sequence (symbol lookup + offset add + typed read) into one expression. It statically rejects the three fatal error classes (wrong C name, wrong address arithmetic, wrong bitwidth), is implemented against Linux DWARF-derived JSON for offsets, and is used on examples including a guest rootkit case study that runs successfully.
AI-written summary · about
chapters (7)
- 0:00Husk library intro
- 2:56Problems with VMI libraries
- 7:24Haskell solution with Husk
- 12:35Husk meta functions
- 19:07Error prevention in Husk
- 23:04Summary
- 23:52Q&A
related talks
23mVenerable Variadic Vulnerabilities Vanquished
18mVMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating(…)
47mLinux Virtualization Based Security
28mProving Memory Access Violations in Isabelle/HOL
14mInside Out: A Paradigm Shift in VM Introspection
17mVeriSMo: A Verified Security Module for Confidential VMs
28mLightweight Hypervisor Verification: Putting the Hardware Burger on a Diet
30mHA-IOV: Applying Hardware-assisted Techniques to IO Virtualization Framework