Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
Sound Formal Verification of Linux’s USB BP Keyboard Driver
verfasst von : Willem Penninckx, Jan Tobias Mühlberg, Jan Smans, Bart Jacobs, Frank Piessens
Erschienen in: NASA Formal Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Case studies on formal software verification can be divided into two categories: while
(i)
unsound approaches may miss errors or report false-positive alarms due to coarse abstractions,
(ii)
sound approaches typically do not handle certain programming constructs like concurrency and/or suffer from scalability issues. This paper presents a case study on successfully verifying the Linux USB BP keyboard driver. Our verification approach is
(a)
sound,
(b)
takes into account dynamic memory allocation, complex API rules and concurrency, and
(c)
is applied on a real kernel driver which was not written with verification in mind. We employ VeriFast, a software verifier based on separation logic. Besides showing that it is possible to verify this device driver, we identify the parts where the verification went smoothly and the parts where the verification approach requires further research to be carried out.