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 language | English |
|---|---|
| Pages | 407-421 |
| Number of pages | 15 |
| Publication status | Published - 2017 |
| Event | 13th International Conference on Integrated Formal Methods - University of Torino, Turin, Italy Duration: 18 Sept 2017 → 22 Sept 2017 Conference number: 13 |
Conference
| Conference | 13th International Conference on Integrated Formal Methods |
|---|---|
| Abbreviated title | iFM 2017 |
| Country/Territory | Italy |
| City | Turin |
| Period | 18/09/17 → 22/09/17 |