Verified programs can party
Hsuan-Chi Kuo, Kai-Hsun Chen, Yicheng Lu, Dan Williams, Sibin Mohan, Tianyin Xu
Abstract
Operating system (OS) extensions are more popular than ever. For example, Linux BPF is marketed as a "superpower" that allows user programs to be downloaded into the kernel, verified to be safe and executed at kernel hook points. So, BPF extensions have high performance and are often placed at performance-critical paths for tracing and filtering.
Topics & Concepts
Computer scienceOperating systemKernel (algebra)SuperpowerHookTracingSystem callLinux kernelComputer securityEngineeringChinaStructural engineeringCombinatoricsLawPolitical scienceMathematicsSecurity and Verification in ComputingAdvanced Malware Detection TechniquesNetwork Security and Intrusion Detection