Certified Password Quality: A Case Study Using Coq and Linux Pluggable Authentication Modules

Joao Ferreira, Saul Johnson, Alexandra Mendes, Phillip Brooke

    Research output: Contribution to conferencePaper

    101 Downloads (Pure)

    Abstract

    We propose the use of modern proof assistants to specify, implement, and verify password quality checkers. We use the proof assistant Coq, focusing on Linux PAM, a widely-used implementation of pluggable authentication modules for Linux. We show how password quality policies can be expressed in Coq and how to use Coq's code extraction features to automatically encode these policies as PAM modules that can readily be used by any Linux system. We implemented the default password quality policy shared by two widely-used PAM modules: pam_cracklib and pam_pwquality. We then compared our implementation with the original modules by running them against a random sample of 100,000 leaked passwords obtained from a publicly available database. In doing this, we demonstrated a potentially serious bug in the original modules. The bug was reported to the maintainers of Linux PAM and is now fixed.
    Original languageEnglish
    Pages407-421
    Number of pages15
    Publication statusPublished - 2017
    Event13th International Conference on Integrated Formal Methods - University of Torino, Turin, Italy
    Duration: 18 Sep 201722 Sep 2017
    Conference number: 13

    Conference

    Conference13th International Conference on Integrated Formal Methods
    Abbreviated titleiFM 2017
    CountryItaly
    CityTurin
    Period18/09/1722/09/17

    Fingerprint Dive into the research topics of 'Certified Password Quality: A Case Study Using Coq and Linux Pluggable Authentication Modules'. Together they form a unique fingerprint.

  • Cite this

    Ferreira, J., Johnson, S., Mendes, A., & Brooke, P. (2017). Certified Password Quality: A Case Study Using Coq and Linux Pluggable Authentication Modules. 407-421. Paper presented at 13th International Conference on Integrated Formal Methods, Turin, Italy.