Project

General

Profile

2nd Google Summer of Code 2012 project was merged to master

"Formalization of Correct Usage of Kernel Core API" project developed during Google Summer of Code 2012 was merged to master of the Linux Driver Verification project.
Added by Evgeny Novikov about 12 years ago

In Google Summer of Code 2012 Ph.D. student Mikhail Mandrykin managed by mentor Alexey Khoroshilov has successfully developed a project titled Formalization of Correct Usage of Kernel Core API for The Linux Foundation. A corresponding branch was merged to the master branch of the Linux Driver Verification project in 5ee5b4e.

Mikhail implemented 5 formal models for safety rules that help him to find a lot of bugs in Linux kernel drivers:
  1. Possible TTY NULL dereference (commits 1, 2)
  2. The gadget driver (de)registration (commits 1, 2, 3, 4, 5)
  3. Refcounting with usb_get_dev()/usb_put_dev() (24 suspicious drivers)
  4. Don't call kfree_skb twice (no actual problems were found)
  5. Error handling in probe() (commits 1 and 5 suspicious drivers)

Comments