Description
This thesis examines formal verification of device drivers using model checking, deductive
verification, and synthesis techniques, crucial for preventing system crashes
and security vulnerabilities. It evaluates 15 verification tools based on preparation
effort, processing effort, correctness guarantees, and limitations. Kani, Pancake, and
CPAchecker are identified as the most promising, with Kani particularly suited for
verifying Rust-based drivers. CPAchecker excels in automated verification but is limited
to C, while Pancake offers strong correctness guarantees but requires high manual effort.
An experimental verification of 4 functions from the ixy.rs driver demonstrates Kani’s
effectiveness in ensuring safety and correctness. The findings suggest Kani balances
verification effort, automation, and correctness, making it ideal for Rust driver verification,
especially unsafe code. Pancake and CPAchecker remain strong alternatives, with
potential for further research. The verification approach presented in this work could
potentially be applied to larger projects like Rust-for-Linux.
|
Thesis topic in co-operation with the Fraunhofer Institute for Applied and Integrated Security AISEC, Garching