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

• Type: Article in International Conference Proceedings Book
• Date: 2017

Authors

Ferreira, JF (Author) Other; Johnson, SA (Author) Other; Mendes, A (Author) Other; Brooke, PJ (Author) Other

Conference proceedings International

Title: Integrated Formal Methods - 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings

Pages: 407-421

13th International Conference on Integrated Formal Methods, IFM 2017

20 September 2017 through 22 September 2017

Indexing

Scopus - 3 Citations

Other information

Authenticus ID: P-00N-PGS

DOI: 10.1007/978-3-319-66845-1_27

Abstract (EN): 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. © Springer International Publishing AG 2017.

Language: English

Type (Professor's evaluation): Scientific