EBA is a prototype tool to find non-trivial resource manipulation bugs in C programs, at compile-time, and super-fast.
In its few months of existence, EBA has found several double-lock bugs in Linux 4.7–4.10 releases (i.e. in code that has passed code reviews). All the following bugs are caught by EBA in a matter of seconds:
- HSI: cmt_speech: Fix double spin_lock
- usb: gadget: pch_udc: reorder spin_[un]lock to avoid deadlock
- ath10k: fix deadlock while processing rx_in_ord_ind 
- net: ethernet: ti: cpdma: fix lockup in cpdma_ctlr_destroy() 
- libceph: ceph_build_auth() doesn’t need ceph_auth_build_hello()
- [PATCH] Fix: scsi: megaraid: reduce the scope of pending-list lock to avoid double lock
- iommu/vt-d: Fix dead-locks in disable_dmar_iommu() path 
- Re: Potential double-lock BUG in drivers/tty/serial/sh-sci.c (Linux 4.9)
- Potential deadlock BUG in drivers/net/wireless/st/cw1200/sta.c (Linux 4.9) 
- Potential deadlock BUG in Linux 4.9 drivers/dma/coh901318.c 
- [PATCH] [media] pctv452e: fix double lock bug 
- Potential double-lock BUG in drivers/infiniband/core/umem_odp.c (Linux 4.9-rc7) 
- dmaengine: pl330: fix double lock
 I reported this bug in private email communication with Kalle Valo, but I was slow and the bug had been found and fixed already.
 For some reason I was not credited, but I reported this bug!
 To be confirmed.
EBA is open source: https://github.com/iagoabal/eba
(There are installation instructions in the README.md file.)
EBA first uses side-effect analysis to build a program abstraction. This abstraction is later model checked in search of bug patterns.
- A short 2-page paper about EBA (the evaluation results are outdated)
- A research paper to appear in VMCAI 2017
- EBA’s inference system for CIL
EBA is a tool by Iago Abal.
This project was originally part of my PhD at IT University of Copenhagen.